Step | Hyp | Ref
| Expression |
1 | | mersenne 26954 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |
2 | | prmnn 16615 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
3 | 1, 2 | syl 17 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |
4 | | 1sgm2ppw 26927 |
. . . 4
โข (๐ โ โ โ (1
ฯ (2โ(๐ โ
1))) = ((2โ๐) โ
1)) |
5 | 3, 4 | syl 17 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ (2โ(๐ โ 1))) = ((2โ๐) โ 1)) |
6 | | 1sgmprm 26926 |
. . . . 5
โข
(((2โ๐) โ
1) โ โ โ (1 ฯ ((2โ๐) โ 1)) = (((2โ๐) โ 1) + 1)) |
7 | 6 | adantl 482 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ๐) โ 1)) = (((2โ๐) โ 1) + 1)) |
8 | | 2nn 12289 |
. . . . . . 7
โข 2 โ
โ |
9 | 3 | nnnn0d 12536 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ0) |
10 | | nnexpcl 14044 |
. . . . . . 7
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
11 | 8, 9, 10 | sylancr 587 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) โ โ) |
12 | 11 | nncnd 12232 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) โ โ) |
13 | | ax-1cn 11170 |
. . . . 5
โข 1 โ
โ |
14 | | npcan 11473 |
. . . . 5
โข
(((2โ๐) โ
โ โง 1 โ โ) โ (((2โ๐) โ 1) + 1) = (2โ๐)) |
15 | 12, 13, 14 | sylancl 586 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) + 1) = (2โ๐)) |
16 | 7, 15 | eqtrd 2772 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ๐) โ 1)) = (2โ๐)) |
17 | 5, 16 | oveq12d 7429 |
. 2
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((1 ฯ (2โ(๐ โ 1))) ยท (1 ฯ
((2โ๐) โ 1))) =
(((2โ๐) โ 1)
ยท (2โ๐))) |
18 | 13 | a1i 11 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 โ โ) |
19 | | nnm1nn0 12517 |
. . . . 5
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
20 | 3, 19 | syl 17 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (๐
โ 1) โ โ0) |
21 | | nnexpcl 14044 |
. . . 4
โข ((2
โ โ โง (๐
โ 1) โ โ0) โ (2โ(๐ โ 1)) โ
โ) |
22 | 8, 20, 21 | sylancr 587 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ(๐ โ 1)) โ
โ) |
23 | | prmnn 16615 |
. . . 4
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ
โ) |
24 | 23 | adantl 482 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
โ) |
25 | 22 | nnzd 12589 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ(๐ โ 1)) โ
โค) |
26 | | prmz 16616 |
. . . . . 6
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ
โค) |
27 | 26 | adantl 482 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
โค) |
28 | 25, 27 | gcdcomd 16459 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ(๐ โ 1)) gcd ((2โ๐) โ 1)) = (((2โ๐) โ 1) gcd (2โ(๐ โ 1)))) |
29 | | iddvds 16217 |
. . . . . . . 8
โข
(((2โ๐) โ
1) โ โค โ ((2โ๐) โ 1) โฅ ((2โ๐) โ 1)) |
30 | 27, 29 | syl 17 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โฅ ((2โ๐) โ 1)) |
31 | | prmuz2 16637 |
. . . . . . . . . 10
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ
(โคโฅโ2)) |
32 | 31 | adantl 482 |
. . . . . . . . 9
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
(โคโฅโ2)) |
33 | | eluz2gt1 12908 |
. . . . . . . . 9
โข
(((2โ๐) โ
1) โ (โคโฅโ2) โ 1 < ((2โ๐) โ 1)) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 < ((2โ๐) โ 1)) |
35 | | ndvdsp1 16358 |
. . . . . . . 8
โข
((((2โ๐)
โ 1) โ โค โง ((2โ๐) โ 1) โ โ โง 1 <
((2โ๐) โ 1))
โ (((2โ๐) โ
1) โฅ ((2โ๐)
โ 1) โ ยฌ ((2โ๐) โ 1) โฅ (((2โ๐) โ 1) +
1))) |
36 | 27, 24, 34, 35 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) โฅ ((2โ๐) โ 1) โ ยฌ
((2โ๐) โ 1)
โฅ (((2โ๐)
โ 1) + 1))) |
37 | 30, 36 | mpd 15 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ยฌ ((2โ๐) โ 1) โฅ (((2โ๐) โ 1) +
1)) |
38 | | 2z 12598 |
. . . . . . . . 9
โข 2 โ
โค |
39 | 38 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 2 โ โค) |
40 | | dvdsmultr1 16243 |
. . . . . . . 8
โข
((((2โ๐)
โ 1) โ โค โง (2โ(๐ โ 1)) โ โค โง 2 โ
โค) โ (((2โ๐) โ 1) โฅ (2โ(๐ โ 1)) โ
((2โ๐) โ 1)
โฅ ((2โ(๐ โ
1)) ยท 2))) |
41 | 27, 25, 39, 40 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) โฅ (2โ(๐ โ 1)) โ
((2โ๐) โ 1)
โฅ ((2โ(๐ โ
1)) ยท 2))) |
42 | | 2cn 12291 |
. . . . . . . . . 10
โข 2 โ
โ |
43 | | expm1t 14060 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ) โ (2โ๐) = ((2โ(๐ โ 1)) ยท 2)) |
44 | 42, 3, 43 | sylancr 587 |
. . . . . . . . 9
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) = ((2โ(๐ โ 1)) ยท 2)) |
45 | 15, 44 | eqtr2d 2773 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ(๐ โ 1)) ยท 2) = (((2โ๐) โ 1) +
1)) |
46 | 45 | breq2d 5160 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) โฅ ((2โ(๐ โ 1)) ยท 2) โ
((2โ๐) โ 1)
โฅ (((2โ๐)
โ 1) + 1))) |
47 | 41, 46 | sylibd 238 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) โฅ (2โ(๐ โ 1)) โ
((2โ๐) โ 1)
โฅ (((2โ๐)
โ 1) + 1))) |
48 | 37, 47 | mtod 197 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ยฌ ((2โ๐) โ 1) โฅ (2โ(๐ โ 1))) |
49 | | simpr 485 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
โ) |
50 | | coprm 16652 |
. . . . . 6
โข
((((2โ๐)
โ 1) โ โ โง (2โ(๐ โ 1)) โ โค) โ (ยฌ
((2โ๐) โ 1)
โฅ (2โ(๐ โ
1)) โ (((2โ๐)
โ 1) gcd (2โ(๐
โ 1))) = 1)) |
51 | 49, 25, 50 | syl2anc 584 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (ยฌ ((2โ๐) โ 1) โฅ (2โ(๐ โ 1)) โ
(((2โ๐) โ 1) gcd
(2โ(๐ โ 1))) =
1)) |
52 | 48, 51 | mpbid 231 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (((2โ๐) โ 1) gcd (2โ(๐ โ 1))) = 1) |
53 | 28, 52 | eqtrd 2772 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ(๐ โ 1)) gcd ((2โ๐) โ 1)) = 1) |
54 | | sgmmul 26928 |
. . 3
โข ((1
โ โ โง ((2โ(๐ โ 1)) โ โ โง
((2โ๐) โ 1)
โ โ โง ((2โ(๐ โ 1)) gcd ((2โ๐) โ 1)) = 1)) โ (1 ฯ
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1))) = ((1 ฯ (2โ(๐ โ 1))) ยท (1 ฯ
((2โ๐) โ
1)))) |
55 | 18, 22, 24, 53, 54 | syl13anc 1372 |
. 2
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) = ((1 ฯ
(2โ(๐ โ 1)))
ยท (1 ฯ ((2โ๐) โ 1)))) |
56 | | subcl 11463 |
. . . 4
โข
(((2โ๐) โ
โ โง 1 โ โ) โ ((2โ๐) โ 1) โ
โ) |
57 | 12, 13, 56 | sylancl 586 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
โ) |
58 | 12, 57 | mulcomd 11239 |
. 2
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) ยท ((2โ๐) โ 1)) = (((2โ๐) โ 1) ยท (2โ๐))) |
59 | 17, 55, 58 | 3eqtr4d 2782 |
1
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) = ((2โ๐) ยท ((2โ๐) โ 1))) |