Step | Hyp | Ref
| Expression |
1 | | 2nn 12233 |
. . 3
โข 2 โ
โ |
2 | | perfectlem.1 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
3 | 2 | nnnn0d 12480 |
. . . 4
โข (๐ โ ๐ด โ
โ0) |
4 | | peano2nn0 12460 |
. . . 4
โข (๐ด โ โ0
โ (๐ด + 1) โ
โ0) |
5 | 3, 4 | syl 17 |
. . 3
โข (๐ โ (๐ด + 1) โ
โ0) |
6 | | nnexpcl 13987 |
. . 3
โข ((2
โ โ โง (๐ด +
1) โ โ0) โ (2โ(๐ด + 1)) โ โ) |
7 | 1, 5, 6 | sylancr 588 |
. 2
โข (๐ โ (2โ(๐ด + 1)) โ โ) |
8 | | 2re 12234 |
. . . 4
โข 2 โ
โ |
9 | 2 | peano2nnd 12177 |
. . . 4
โข (๐ โ (๐ด + 1) โ โ) |
10 | | 1lt2 12331 |
. . . . 5
โข 1 <
2 |
11 | 10 | a1i 11 |
. . . 4
โข (๐ โ 1 < 2) |
12 | | expgt1 14013 |
. . . 4
โข ((2
โ โ โง (๐ด +
1) โ โ โง 1 < 2) โ 1 < (2โ(๐ด + 1))) |
13 | 8, 9, 11, 12 | mp3an2i 1467 |
. . 3
โข (๐ โ 1 < (2โ(๐ด + 1))) |
14 | | 1nn 12171 |
. . . 4
โข 1 โ
โ |
15 | | nnsub 12204 |
. . . 4
โข ((1
โ โ โง (2โ(๐ด + 1)) โ โ) โ (1 <
(2โ(๐ด + 1)) โ
((2โ(๐ด + 1)) โ
1) โ โ)) |
16 | 14, 7, 15 | sylancr 588 |
. . 3
โข (๐ โ (1 < (2โ(๐ด + 1)) โ ((2โ(๐ด + 1)) โ 1) โ
โ)) |
17 | 13, 16 | mpbid 231 |
. 2
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โ) |
18 | 7 | nnzd 12533 |
. . . . . . 7
โข (๐ โ (2โ(๐ด + 1)) โ โค) |
19 | | peano2zm 12553 |
. . . . . . 7
โข
((2โ(๐ด + 1))
โ โค โ ((2โ(๐ด + 1)) โ 1) โ
โค) |
20 | 18, 19 | syl 17 |
. . . . . 6
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โ
โค) |
21 | | 1nn0 12436 |
. . . . . . . 8
โข 1 โ
โ0 |
22 | | perfectlem.2 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
23 | | sgmnncl 26512 |
. . . . . . . 8
โข ((1
โ โ0 โง ๐ต โ โ) โ (1 ฯ ๐ต) โ
โ) |
24 | 21, 22, 23 | sylancr 588 |
. . . . . . 7
โข (๐ โ (1 ฯ ๐ต) โ
โ) |
25 | 24 | nnzd 12533 |
. . . . . 6
โข (๐ โ (1 ฯ ๐ต) โ
โค) |
26 | | dvdsmul1 16167 |
. . . . . 6
โข
((((2โ(๐ด + 1))
โ 1) โ โค โง (1 ฯ ๐ต) โ โค) โ ((2โ(๐ด + 1)) โ 1) โฅ
(((2โ(๐ด + 1)) โ
1) ยท (1 ฯ ๐ต))) |
27 | 20, 25, 26 | syl2anc 585 |
. . . . 5
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โฅ
(((2โ(๐ด + 1)) โ
1) ยท (1 ฯ ๐ต))) |
28 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
29 | | expp1 13981 |
. . . . . . . . 9
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
30 | 28, 3, 29 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (2โ(๐ด + 1)) = ((2โ๐ด) ยท 2)) |
31 | | nnexpcl 13987 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐ด
โ โ0) โ (2โ๐ด) โ โ) |
32 | 1, 3, 31 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (2โ๐ด) โ โ) |
33 | 32 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ (2โ๐ด) โ โ) |
34 | | mulcom 11144 |
. . . . . . . . 9
โข
(((2โ๐ด) โ
โ โง 2 โ โ) โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
35 | 33, 28, 34 | sylancl 587 |
. . . . . . . 8
โข (๐ โ ((2โ๐ด) ยท 2) = (2 ยท (2โ๐ด))) |
36 | 30, 35 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (2โ(๐ด + 1)) = (2 ยท (2โ๐ด))) |
37 | 36 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = ((2 ยท (2โ๐ด)) ยท ๐ต)) |
38 | 28 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
39 | 22 | nncnd 12176 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
40 | 38, 33, 39 | mulassd 11185 |
. . . . . 6
โข (๐ โ ((2 ยท (2โ๐ด)) ยท ๐ต) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
41 | | ax-1cn 11116 |
. . . . . . . . 9
โข 1 โ
โ |
42 | 41 | a1i 11 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
43 | | perfectlem.3 |
. . . . . . . . . 10
โข (๐ โ ยฌ 2 โฅ ๐ต) |
44 | | 2prm 16575 |
. . . . . . . . . . 11
โข 2 โ
โ |
45 | 22 | nnzd 12533 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โค) |
46 | | coprm 16594 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐ต
โ โค) โ (ยฌ 2 โฅ ๐ต โ (2 gcd ๐ต) = 1)) |
47 | 44, 45, 46 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (ยฌ 2 โฅ ๐ต โ (2 gcd ๐ต) = 1)) |
48 | 43, 47 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (2 gcd ๐ต) = 1) |
49 | | 2z 12542 |
. . . . . . . . . 10
โข 2 โ
โค |
50 | | rpexp1i 16606 |
. . . . . . . . . 10
โข ((2
โ โค โง ๐ต
โ โค โง ๐ด
โ โ0) โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
51 | 49, 45, 3, 50 | mp3an2i 1467 |
. . . . . . . . 9
โข (๐ โ ((2 gcd ๐ต) = 1 โ ((2โ๐ด) gcd ๐ต) = 1)) |
52 | 48, 51 | mpd 15 |
. . . . . . . 8
โข (๐ โ ((2โ๐ด) gcd ๐ต) = 1) |
53 | | sgmmul 26565 |
. . . . . . . 8
โข ((1
โ โ โง ((2โ๐ด) โ โ โง ๐ต โ โ โง ((2โ๐ด) gcd ๐ต) = 1)) โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
54 | 42, 32, 22, 52, 53 | syl13anc 1373 |
. . . . . . 7
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต))) |
55 | | perfectlem.4 |
. . . . . . 7
โข (๐ โ (1 ฯ ((2โ๐ด) ยท ๐ต)) = (2 ยท ((2โ๐ด) ยท ๐ต))) |
56 | 2 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
57 | | pncan 11414 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด + 1)
โ 1) = ๐ด) |
58 | 56, 41, 57 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด + 1) โ 1) = ๐ด) |
59 | 58 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ (2โ((๐ด + 1) โ 1)) =
(2โ๐ด)) |
60 | 59 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) = (1 ฯ
(2โ๐ด))) |
61 | | 1sgm2ppw 26564 |
. . . . . . . . . 10
โข ((๐ด + 1) โ โ โ (1
ฯ (2โ((๐ด + 1)
โ 1))) = ((2โ(๐ด
+ 1)) โ 1)) |
62 | 9, 61 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1 ฯ (2โ((๐ด + 1) โ 1))) =
((2โ(๐ด + 1)) โ
1)) |
63 | 60, 62 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ (1 ฯ (2โ๐ด)) = ((2โ(๐ด + 1)) โ 1)) |
64 | 63 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((1 ฯ (2โ๐ด)) ยท (1 ฯ ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1
ฯ ๐ต))) |
65 | 54, 55, 64 | 3eqtr3d 2785 |
. . . . . 6
โข (๐ โ (2 ยท ((2โ๐ด) ยท ๐ต)) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
66 | 37, 40, 65 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((2โ(๐ด + 1)) ยท ๐ต) = (((2โ(๐ด + 1)) โ 1) ยท (1 ฯ ๐ต))) |
67 | 27, 66 | breqtrrd 5138 |
. . . 4
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โฅ
((2โ(๐ด + 1)) ยท
๐ต)) |
68 | 20, 18 | gcdcomd 16401 |
. . . . 5
โข (๐ โ (((2โ(๐ด + 1)) โ 1) gcd
(2โ(๐ด + 1))) =
((2โ(๐ด + 1)) gcd
((2โ(๐ด + 1)) โ
1))) |
69 | | iddvdsexp 16169 |
. . . . . . . . 9
โข ((2
โ โค โง (๐ด +
1) โ โ) โ 2 โฅ (2โ(๐ด + 1))) |
70 | 49, 9, 69 | sylancr 588 |
. . . . . . . 8
โข (๐ โ 2 โฅ (2โ(๐ด + 1))) |
71 | | n2dvds1 16257 |
. . . . . . . . . 10
โข ยฌ 2
โฅ 1 |
72 | 49 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โค) |
73 | | 1zzd 12541 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โค) |
74 | 72, 18, 73 | 3jca 1129 |
. . . . . . . . . . 11
โข (๐ โ (2 โ โค โง
(2โ(๐ด + 1)) โ
โค โง 1 โ โค)) |
75 | | dvdssub2 16190 |
. . . . . . . . . . 11
โข (((2
โ โค โง (2โ(๐ด + 1)) โ โค โง 1 โ
โค) โง 2 โฅ ((2โ(๐ด + 1)) โ 1)) โ (2 โฅ
(2โ(๐ด + 1)) โ 2
โฅ 1)) |
76 | 74, 75 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง 2 โฅ ((2โ(๐ด + 1)) โ 1)) โ (2
โฅ (2โ(๐ด + 1))
โ 2 โฅ 1)) |
77 | 71, 76 | mtbiri 327 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ((2โ(๐ด + 1)) โ 1)) โ ยฌ
2 โฅ (2โ(๐ด +
1))) |
78 | 77 | ex 414 |
. . . . . . . 8
โข (๐ โ (2 โฅ ((2โ(๐ด + 1)) โ 1) โ ยฌ 2
โฅ (2โ(๐ด +
1)))) |
79 | 70, 78 | mt2d 136 |
. . . . . . 7
โข (๐ โ ยฌ 2 โฅ
((2โ(๐ด + 1)) โ
1)) |
80 | | coprm 16594 |
. . . . . . . 8
โข ((2
โ โ โง ((2โ(๐ด + 1)) โ 1) โ โค) โ
(ยฌ 2 โฅ ((2โ(๐ด + 1)) โ 1) โ (2 gcd
((2โ(๐ด + 1)) โ
1)) = 1)) |
81 | 44, 20, 80 | sylancr 588 |
. . . . . . 7
โข (๐ โ (ยฌ 2 โฅ
((2โ(๐ด + 1)) โ
1) โ (2 gcd ((2โ(๐ด + 1)) โ 1)) = 1)) |
82 | 79, 81 | mpbid 231 |
. . . . . 6
โข (๐ โ (2 gcd ((2โ(๐ด + 1)) โ 1)) =
1) |
83 | | rpexp1i 16606 |
. . . . . . 7
โข ((2
โ โค โง ((2โ(๐ด + 1)) โ 1) โ โค โง
(๐ด + 1) โ
โ0) โ ((2 gcd ((2โ(๐ด + 1)) โ 1)) = 1 โ
((2โ(๐ด + 1)) gcd
((2โ(๐ด + 1)) โ
1)) = 1)) |
84 | 49, 20, 5, 83 | mp3an2i 1467 |
. . . . . 6
โข (๐ โ ((2 gcd ((2โ(๐ด + 1)) โ 1)) = 1 โ
((2โ(๐ด + 1)) gcd
((2โ(๐ด + 1)) โ
1)) = 1)) |
85 | 82, 84 | mpd 15 |
. . . . 5
โข (๐ โ ((2โ(๐ด + 1)) gcd ((2โ(๐ด + 1)) โ 1)) =
1) |
86 | 68, 85 | eqtrd 2777 |
. . . 4
โข (๐ โ (((2โ(๐ด + 1)) โ 1) gcd
(2โ(๐ด + 1))) =
1) |
87 | | coprmdvds 16536 |
. . . . 5
โข
((((2โ(๐ด + 1))
โ 1) โ โค โง (2โ(๐ด + 1)) โ โค โง ๐ต โ โค) โ
((((2โ(๐ด + 1)) โ
1) โฅ ((2โ(๐ด +
1)) ยท ๐ต) โง
(((2โ(๐ด + 1)) โ
1) gcd (2โ(๐ด + 1))) =
1) โ ((2โ(๐ด + 1))
โ 1) โฅ ๐ต)) |
88 | 20, 18, 45, 87 | syl3anc 1372 |
. . . 4
โข (๐ โ ((((2โ(๐ด + 1)) โ 1) โฅ
((2โ(๐ด + 1)) ยท
๐ต) โง (((2โ(๐ด + 1)) โ 1) gcd
(2โ(๐ด + 1))) = 1)
โ ((2โ(๐ด + 1))
โ 1) โฅ ๐ต)) |
89 | 67, 86, 88 | mp2and 698 |
. . 3
โข (๐ โ ((2โ(๐ด + 1)) โ 1) โฅ ๐ต) |
90 | | nndivdvds 16152 |
. . . 4
โข ((๐ต โ โ โง
((2โ(๐ด + 1)) โ
1) โ โ) โ (((2โ(๐ด + 1)) โ 1) โฅ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ)) |
91 | 22, 17, 90 | syl2anc 585 |
. . 3
โข (๐ โ (((2โ(๐ด + 1)) โ 1) โฅ ๐ต โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ)) |
92 | 89, 91 | mpbid 231 |
. 2
โข (๐ โ (๐ต / ((2โ(๐ด + 1)) โ 1)) โ
โ) |
93 | 7, 17, 92 | 3jca 1129 |
1
โข (๐ โ ((2โ(๐ด + 1)) โ โ โง
((2โ(๐ด + 1)) โ
1) โ โ โง (๐ต
/ ((2โ(๐ด + 1)) โ
1)) โ โ)) |