Step | Hyp | Ref
| Expression |
1 | | 2dvdseven 45935 |
. . . . . . . 8
โข (๐ โ Even โ 2 โฅ
๐) |
2 | 1 | ad2antlr 726 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ 2 โฅ ๐) |
3 | | 2prm 16576 |
. . . . . . . 8
โข 2 โ
โ |
4 | | simpll 766 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ๐ โ โ) |
5 | | pcelnn 16750 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ ((2 pCnt ๐) โ โ โ 2 โฅ ๐)) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2 pCnt ๐) โ โ โ 2
โฅ ๐)) |
7 | 2, 6 | mpbird 257 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 pCnt ๐) โ
โ) |
8 | 7 | nnzd 12534 |
. . . . 5
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 pCnt ๐) โ
โค) |
9 | 8 | peano2zd 12618 |
. . . 4
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2 pCnt ๐) + 1) โ
โค) |
10 | | pcdvds 16744 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ) โ (2โ(2 pCnt ๐)) โฅ ๐) |
11 | 3, 4, 10 | sylancr 588 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2โ(2 pCnt ๐)) โฅ ๐) |
12 | | 2nn 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
13 | 7 | nnnn0d 12481 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 pCnt ๐) โ
โ0) |
14 | | nnexpcl 13989 |
. . . . . . . . . 10
โข ((2
โ โ โง (2 pCnt ๐) โ โ0) โ
(2โ(2 pCnt ๐)) โ
โ) |
15 | 12, 13, 14 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2โ(2 pCnt ๐)) โ
โ) |
16 | | nndivdvds 16153 |
. . . . . . . . 9
โข ((๐ โ โ โง (2โ(2
pCnt ๐)) โ โ)
โ ((2โ(2 pCnt ๐))
โฅ ๐ โ (๐ / (2โ(2 pCnt ๐))) โ
โ)) |
17 | 4, 15, 16 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2โ(2 pCnt ๐)) โฅ ๐ โ (๐ / (2โ(2 pCnt ๐))) โ โ)) |
18 | 11, 17 | mpbid 231 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (๐ / (2โ(2 pCnt ๐))) โ โ) |
19 | 18 | nnzd 12534 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (๐ / (2โ(2 pCnt ๐))) โ โค) |
20 | | pcndvds2 16748 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ) โ ยฌ 2 โฅ (๐ / (2โ(2 pCnt ๐)))) |
21 | 3, 4, 20 | sylancr 588 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ยฌ 2 โฅ (๐ / (2โ(2 pCnt ๐)))) |
22 | | isodd3 45934 |
. . . . . . . 8
โข ((๐ / (2โ(2 pCnt ๐))) โ Odd โ ((๐ / (2โ(2 pCnt ๐))) โ โค โง ยฌ 2
โฅ (๐ / (2โ(2
pCnt ๐))))) |
23 | 19, 21, 22 | sylanbrc 584 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (๐ / (2โ(2 pCnt ๐))) โ Odd ) |
24 | | simpr 486 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (1 ฯ ๐) = (2 ยท ๐)) |
25 | | nncn 12169 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ๐ โ โ) |
27 | 15 | nncnd 12177 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2โ(2 pCnt ๐)) โ
โ) |
28 | 15 | nnne0d 12211 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2โ(2 pCnt ๐)) โ 0) |
29 | 26, 27, 28 | divcan2d 11941 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2โ(2 pCnt ๐)) ยท (๐ / (2โ(2 pCnt ๐)))) = ๐) |
30 | 29 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (1 ฯ ((2โ(2
pCnt ๐)) ยท (๐ / (2โ(2 pCnt ๐))))) = (1 ฯ ๐)) |
31 | 29 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 ยท
((2โ(2 pCnt ๐))
ยท (๐ / (2โ(2
pCnt ๐))))) = (2 ยท
๐)) |
32 | 24, 30, 31 | 3eqtr4d 2783 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (1 ฯ ((2โ(2
pCnt ๐)) ยท (๐ / (2โ(2 pCnt ๐))))) = (2 ยท ((2โ(2
pCnt ๐)) ยท (๐ / (2โ(2 pCnt ๐)))))) |
33 | 7, 18, 23, 32 | perfectALTVlem2 46004 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((๐ / (2โ(2 pCnt ๐))) โ โ โง (๐ / (2โ(2 pCnt ๐))) = ((2โ((2 pCnt ๐) + 1)) โ 1))) |
34 | 33 | simprd 497 |
. . . . 5
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (๐ / (2โ(2 pCnt ๐))) = ((2โ((2 pCnt ๐) + 1)) โ 1)) |
35 | 33 | simpld 496 |
. . . . 5
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (๐ / (2โ(2 pCnt ๐))) โ โ) |
36 | 34, 35 | eqeltrrd 2835 |
. . . 4
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2โ((2 pCnt
๐) + 1)) โ 1) โ
โ) |
37 | 7 | nncnd 12177 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 pCnt ๐) โ
โ) |
38 | | ax-1cn 11117 |
. . . . . . . . 9
โข 1 โ
โ |
39 | | pncan 11415 |
. . . . . . . . 9
โข (((2 pCnt
๐) โ โ โง 1
โ โ) โ (((2 pCnt ๐) + 1) โ 1) = (2 pCnt ๐)) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (((2 pCnt ๐) + 1) โ 1) = (2 pCnt
๐)) |
41 | 40 | eqcomd 2739 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2 pCnt ๐) = (((2 pCnt ๐) + 1) โ 1)) |
42 | 41 | oveq2d 7377 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ (2โ(2 pCnt ๐)) = (2โ(((2 pCnt ๐) + 1) โ
1))) |
43 | 42, 34 | oveq12d 7379 |
. . . . 5
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ((2โ(2 pCnt ๐)) ยท (๐ / (2โ(2 pCnt ๐)))) = ((2โ(((2 pCnt ๐) + 1) โ 1)) ยท ((2โ((2
pCnt ๐) + 1)) โ
1))) |
44 | 29, 43 | eqtr3d 2775 |
. . . 4
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ ๐ = ((2โ(((2 pCnt ๐) + 1) โ 1)) ยท ((2โ((2
pCnt ๐) + 1)) โ
1))) |
45 | | oveq2 7369 |
. . . . . . . 8
โข (๐ = ((2 pCnt ๐) + 1) โ (2โ๐) = (2โ((2 pCnt ๐) + 1))) |
46 | 45 | oveq1d 7376 |
. . . . . . 7
โข (๐ = ((2 pCnt ๐) + 1) โ ((2โ๐) โ 1) = ((2โ((2 pCnt ๐) + 1)) โ
1)) |
47 | 46 | eleq1d 2819 |
. . . . . 6
โข (๐ = ((2 pCnt ๐) + 1) โ (((2โ๐) โ 1) โ โ โ
((2โ((2 pCnt ๐) + 1))
โ 1) โ โ)) |
48 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ = ((2 pCnt ๐) + 1) โ (๐ โ 1) = (((2 pCnt ๐) + 1) โ 1)) |
49 | 48 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = ((2 pCnt ๐) + 1) โ (2โ(๐ โ 1)) = (2โ(((2 pCnt ๐) + 1) โ
1))) |
50 | 49, 46 | oveq12d 7379 |
. . . . . . 7
โข (๐ = ((2 pCnt ๐) + 1) โ ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)) = ((2โ(((2
pCnt ๐) + 1) โ 1))
ยท ((2โ((2 pCnt ๐) + 1)) โ 1))) |
51 | 50 | eqeq2d 2744 |
. . . . . 6
โข (๐ = ((2 pCnt ๐) + 1) โ (๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)) โ ๐ = ((2โ(((2 pCnt ๐) + 1) โ 1)) ยท
((2โ((2 pCnt ๐) + 1))
โ 1)))) |
52 | 47, 51 | anbi12d 632 |
. . . . 5
โข (๐ = ((2 pCnt ๐) + 1) โ ((((2โ๐) โ 1) โ โ โง ๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) โ
(((2โ((2 pCnt ๐) + 1))
โ 1) โ โ โง ๐ = ((2โ(((2 pCnt ๐) + 1) โ 1)) ยท ((2โ((2
pCnt ๐) + 1)) โ
1))))) |
53 | 52 | rspcev 3583 |
. . . 4
โข ((((2
pCnt ๐) + 1) โ โค
โง (((2โ((2 pCnt ๐)
+ 1)) โ 1) โ โ โง ๐ = ((2โ(((2 pCnt ๐) + 1) โ 1)) ยท ((2โ((2
pCnt ๐) + 1)) โ 1))))
โ โ๐ โ
โค (((2โ๐)
โ 1) โ โ โง ๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)))) |
54 | 9, 36, 44, 53 | syl12anc 836 |
. . 3
โข (((๐ โ โ โง ๐ โ Even ) โง (1 ฯ
๐) = (2 ยท ๐)) โ โ๐ โ โค (((2โ๐) โ 1) โ โ
โง ๐ = ((2โ(๐ โ 1)) ยท
((2โ๐) โ
1)))) |
55 | 54 | ex 414 |
. 2
โข ((๐ โ โ โง ๐ โ Even ) โ ((1
ฯ ๐) = (2 ยท
๐) โ โ๐ โ โค (((2โ๐) โ 1) โ โ
โง ๐ = ((2โ(๐ โ 1)) ยท
((2โ๐) โ
1))))) |
56 | | perfect1 26599 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) = ((2โ๐) ยท ((2โ๐) โ 1))) |
57 | | 2cn 12236 |
. . . . . . . . 9
โข 2 โ
โ |
58 | | mersenne 26598 |
. . . . . . . . . 10
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |
59 | | prmnn 16558 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |
61 | | expm1t 14005 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ) โ (2โ๐) = ((2โ(๐ โ 1)) ยท 2)) |
62 | 57, 60, 61 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) = ((2โ(๐ โ 1)) ยท 2)) |
63 | | nnm1nn0 12462 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
64 | 60, 63 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (๐
โ 1) โ โ0) |
65 | | expcl 13994 |
. . . . . . . . . 10
โข ((2
โ โ โง (๐
โ 1) โ โ0) โ (2โ(๐ โ 1)) โ โ) |
66 | 57, 64, 65 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ(๐ โ 1)) โ โ) |
67 | | mulcom 11145 |
. . . . . . . . 9
โข
(((2โ(๐ โ
1)) โ โ โง 2 โ โ) โ ((2โ(๐ โ 1)) ยท 2) = (2 ยท
(2โ(๐ โ
1)))) |
68 | 66, 57, 67 | sylancl 587 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ(๐ โ 1)) ยท 2) = (2 ยท
(2โ(๐ โ
1)))) |
69 | 62, 68 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) = (2 ยท (2โ(๐ โ 1)))) |
70 | 69 | oveq1d 7376 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) ยท ((2โ๐) โ 1)) = ((2 ยท (2โ(๐ โ 1))) ยท
((2โ๐) โ
1))) |
71 | | 2cnd 12239 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 2 โ โ) |
72 | | prmnn 16558 |
. . . . . . . . 9
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ โ) |
73 | 72 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ โ) |
74 | 73 | nncnd 12177 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ โ) |
75 | 71, 66, 74 | mulassd 11186 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2 ยท (2โ(๐ โ 1))) ยท ((2โ๐) โ 1)) = (2 ยท
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)))) |
76 | 56, 70, 75 | 3eqtrd 2777 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 ฯ ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) = (2 ยท
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)))) |
77 | | oveq2 7369 |
. . . . . 6
โข (๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)) โ (1 ฯ
๐) = (1 ฯ
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)))) |
78 | | oveq2 7369 |
. . . . . 6
โข (๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)) โ (2 ยท
๐) = (2 ยท
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)))) |
79 | 77, 78 | eqeq12d 2749 |
. . . . 5
โข (๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1)) โ ((1 ฯ
๐) = (2 ยท ๐) โ (1 ฯ
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1))) = (2 ยท ((2โ(๐ โ 1)) ยท ((2โ๐) โ
1))))) |
80 | 76, 79 | syl5ibrcom 247 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (๐ =
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)) โ (1 ฯ ๐) = (2 ยท ๐))) |
81 | 80 | impr 456 |
. . 3
โข ((๐ โ โค โง
(((2โ๐) โ 1)
โ โ โง ๐ =
((2โ(๐ โ 1))
ยท ((2โ๐)
โ 1)))) โ (1 ฯ ๐) = (2 ยท ๐)) |
82 | 81 | rexlimiva 3141 |
. 2
โข
(โ๐ โ
โค (((2โ๐)
โ 1) โ โ โง ๐ = ((2โ(๐ โ 1)) ยท ((2โ๐) โ 1))) โ (1 ฯ
๐) = (2 ยท ๐)) |
83 | 55, 82 | impbid1 224 |
1
โข ((๐ โ โ โง ๐ โ Even ) โ ((1
ฯ ๐) = (2 ยท
๐) โ โ๐ โ โค (((2โ๐) โ 1) โ โ
โง ๐ = ((2โ(๐ โ 1)) ยท
((2โ๐) โ
1))))) |