Step | Hyp | Ref
| Expression |
1 | | 2nn 12289 |
. . . 4
โข 2 โ
โ |
2 | | fpprel 46694 |
. . . 4
โข (2 โ
โ โ (๐ โ (
FPPr โ2) โ (๐
โ (โคโฅโ4) โง ๐ โ โ โง ((2โ(๐ โ 1)) mod ๐) = 1))) |
3 | 1, 2 | ax-mp 5 |
. . 3
โข (๐ โ ( FPPr โ2) โ
(๐ โ
(โคโฅโ4) โง ๐ โ โ โง ((2โ(๐ โ 1)) mod ๐) = 1)) |
4 | | eluz4nn 12874 |
. . . . . . 7
โข (๐ โ
(โคโฅโ4) โ ๐ โ โ) |
5 | 4 | adantr 479 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ ๐ โ โ) |
6 | | eluzelz 12836 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ4) โ ๐ โ โค) |
7 | | zeo2ALTV 46637 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ Even โ ยฌ ๐ โ Odd )) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ4) โ (๐ โ Even โ ยฌ ๐ โ Odd )) |
9 | 8 | adantr 479 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (๐ โ Even โ ยฌ ๐ โ Odd )) |
10 | 9 | biimprd 247 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (ยฌ ๐ โ Odd โ ๐ โ Even )) |
11 | | nnennexALTV 46667 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ Even ) โ
โ๐ฆ โ โ
๐ = (2 ยท ๐ฆ)) |
12 | 5, 10, 11 | syl6an 680 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (ยฌ ๐ โ Odd โ โ๐ฆ โ โ ๐ = (2 ยท ๐ฆ))) |
13 | | oveq1 7418 |
. . . . . . . . . . . . . 14
โข (๐ = (2 ยท ๐ฆ) โ (๐ โ 1) = ((2 ยท ๐ฆ) โ 1)) |
14 | 13 | oveq2d 7427 |
. . . . . . . . . . . . 13
โข (๐ = (2 ยท ๐ฆ) โ (2โ(๐ โ 1)) = (2โ((2
ยท ๐ฆ) โ
1))) |
15 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = (2 ยท ๐ฆ) โ ๐ = (2 ยท ๐ฆ)) |
16 | 14, 15 | oveq12d 7429 |
. . . . . . . . . . . 12
โข (๐ = (2 ยท ๐ฆ) โ ((2โ(๐ โ 1)) mod ๐) = ((2โ((2 ยท ๐ฆ) โ 1)) mod (2 ยท
๐ฆ))) |
17 | 16 | eqeq1d 2732 |
. . . . . . . . . . 11
โข (๐ = (2 ยท ๐ฆ) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ ((2โ((2
ยท ๐ฆ) โ 1)) mod
(2 ยท ๐ฆ)) =
1)) |
18 | 17 | adantl 480 |
. . . . . . . . . 10
โข (((๐ โ
(โคโฅโ4) โง ๐ฆ โ โ) โง ๐ = (2 ยท ๐ฆ)) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ ((2โ((2 ยท ๐ฆ) โ 1)) mod (2 ยท
๐ฆ)) = 1)) |
19 | | 2z 12598 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
20 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ 2 โ
โ) |
21 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
22 | 20, 21 | nnmulcld 12269 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ) |
23 | | nnm1nn0 12517 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท ๐ฆ) โ โ
โ ((2 ยท ๐ฆ)
โ 1) โ โ0) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) โ 1)
โ โ0) |
25 | | zexpcl 14046 |
. . . . . . . . . . . . . . 15
โข ((2
โ โค โง ((2 ยท ๐ฆ) โ 1) โ โ0)
โ (2โ((2 ยท ๐ฆ) โ 1)) โ
โค) |
26 | 19, 24, 25 | sylancr 585 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ
(2โ((2 ยท ๐ฆ)
โ 1)) โ โค) |
27 | 22 | nnrpd 13018 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ+) |
28 | | modmuladdim 13883 |
. . . . . . . . . . . . . 14
โข
(((2โ((2 ยท ๐ฆ) โ 1)) โ โค โง (2
ยท ๐ฆ) โ
โ+) โ (((2โ((2 ยท ๐ฆ) โ 1)) mod (2 ยท ๐ฆ)) = 1 โ โ๐ โ โค (2โ((2
ยท ๐ฆ) โ 1)) =
((๐ ยท (2 ยท
๐ฆ)) + 1))) |
29 | 26, 27, 28 | syl2anc 582 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ
(((2โ((2 ยท ๐ฆ)
โ 1)) mod (2 ยท ๐ฆ)) = 1 โ โ๐ โ โค (2โ((2 ยท ๐ฆ) โ 1)) = ((๐ ยท (2 ยท ๐ฆ)) + 1))) |
30 | 24 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((2
ยท ๐ฆ) โ 1)
โ โ0) |
31 | 19, 30, 25 | sylancr 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((2 ยท ๐ฆ)
โ 1)) โ โค) |
32 | 31 | zcnd 12671 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((2 ยท ๐ฆ)
โ 1)) โ โ) |
33 | | zcn 12567 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
34 | 33 | adantl 480 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ โ โค) โ ๐ โ
โ) |
35 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ 2 โ
โ) |
36 | | nncn 12224 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
37 | 36 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ ๐ฆ โ
โ) |
38 | 35, 37 | mulcld 11238 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท ๐ฆ) โ
โ) |
39 | 34, 38 | mulcld 11238 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ โ โค) โ (๐ ยท (2 ยท ๐ฆ)) โ
โ) |
40 | | 1cnd 11213 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ โ โค) โ 1 โ
โ) |
41 | | subadd 11467 |
. . . . . . . . . . . . . . . . 17
โข
(((2โ((2 ยท ๐ฆ) โ 1)) โ โ โง (๐ ยท (2 ยท ๐ฆ)) โ โ โง 1 โ
โ) โ (((2โ((2 ยท ๐ฆ) โ 1)) โ (๐ ยท (2 ยท ๐ฆ))) = 1 โ ((๐ ยท (2 ยท ๐ฆ)) + 1) = (2โ((2 ยท ๐ฆ) โ 1)))) |
42 | | eqcom 2737 |
. . . . . . . . . . . . . . . . 17
โข (((๐ ยท (2 ยท ๐ฆ)) + 1) = (2โ((2 ยท
๐ฆ) โ 1)) โ
(2โ((2 ยท ๐ฆ)
โ 1)) = ((๐ ยท
(2 ยท ๐ฆ)) +
1)) |
43 | 41, 42 | bitrdi 286 |
. . . . . . . . . . . . . . . 16
โข
(((2โ((2 ยท ๐ฆ) โ 1)) โ โ โง (๐ ยท (2 ยท ๐ฆ)) โ โ โง 1 โ
โ) โ (((2โ((2 ยท ๐ฆ) โ 1)) โ (๐ ยท (2 ยท ๐ฆ))) = 1 โ (2โ((2 ยท ๐ฆ) โ 1)) = ((๐ ยท (2 ยท ๐ฆ)) + 1))) |
44 | 32, 39, 40, 43 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(((2โ((2 ยท ๐ฆ)
โ 1)) โ (๐
ยท (2 ยท ๐ฆ))) =
1 โ (2โ((2 ยท ๐ฆ) โ 1)) = ((๐ ยท (2 ยท ๐ฆ)) + 1))) |
45 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ โ โ โ 2 โ
โ) |
46 | 45, 36 | mulcld 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ) |
47 | | 1cnd 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ โ โ 1 โ
โ) |
48 | 46, 47 | subcld 11575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) โ 1)
โ โ) |
49 | 48 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((2
ยท ๐ฆ) โ 1)
โ โ) |
50 | | npcan1 11643 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((2
ยท ๐ฆ) โ 1)
โ โ โ ((((2 ยท ๐ฆ) โ 1) โ 1) + 1) = ((2 ยท
๐ฆ) โ
1)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((((2
ยท ๐ฆ) โ 1)
โ 1) + 1) = ((2 ยท ๐ฆ) โ 1)) |
52 | 51 | eqcomd 2736 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((2
ยท ๐ฆ) โ 1) =
((((2 ยท ๐ฆ) โ
1) โ 1) + 1)) |
53 | 52 | oveq2d 7427 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((2 ยท ๐ฆ)
โ 1)) = (2โ((((2 ยท ๐ฆ) โ 1) โ 1) +
1))) |
54 | | 2t1e2 12379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (2
ยท 1) = 2 |
55 | 54 | eqcomi 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 = (2
ยท 1) |
56 | 55 | oveq2i 7422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((2
ยท ๐ฆ) โ 2) =
((2 ยท ๐ฆ) โ (2
ยท 1)) |
57 | | sub1m1 12468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((2
ยท ๐ฆ) โ โ
โ (((2 ยท ๐ฆ)
โ 1) โ 1) = ((2 ยท ๐ฆ) โ 2)) |
58 | 38, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ โง ๐ โ โค) โ (((2
ยท ๐ฆ) โ 1)
โ 1) = ((2 ยท ๐ฆ) โ 2)) |
59 | 35, 37, 40 | subdid 11674 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท (๐ฆ โ 1)) =
((2 ยท ๐ฆ) โ (2
ยท 1))) |
60 | 56, 58, 59 | 3eqtr4a 2796 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ โ โ โง ๐ โ โค) โ (((2
ยท ๐ฆ) โ 1)
โ 1) = (2 ยท (๐ฆ
โ 1))) |
61 | | 2nn0 12493 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 โ
โ0 |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ โง ๐ โ โค) โ 2 โ
โ0) |
63 | | nnm1nn0 12517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ โ โ (๐ฆ โ 1) โ
โ0) |
64 | 63 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ โง ๐ โ โค) โ (๐ฆ โ 1) โ
โ0) |
65 | 62, 64 | nn0mulcld 12541 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท (๐ฆ โ 1))
โ โ0) |
66 | 60, 65 | eqeltrd 2831 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง ๐ โ โค) โ (((2
ยท ๐ฆ) โ 1)
โ 1) โ โ0) |
67 | 35, 66 | expp1d 14116 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((((2 ยท ๐ฆ)
โ 1) โ 1) + 1)) = ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) ยท
2)) |
68 | 35, 66 | expcld 14115 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ(((2 ยท ๐ฆ)
โ 1) โ 1)) โ โ) |
69 | 68, 35 | mulcomd 11239 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ โ โค) โ
((2โ(((2 ยท ๐ฆ)
โ 1) โ 1)) ยท 2) = (2 ยท (2โ(((2 ยท ๐ฆ) โ 1) โ
1)))) |
70 | 67, 69 | eqtrd 2770 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((((2 ยท ๐ฆ)
โ 1) โ 1) + 1)) = (2 ยท (2โ(((2 ยท ๐ฆ) โ 1) โ
1)))) |
71 | 53, 70 | eqtrd 2770 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ((2 ยท ๐ฆ)
โ 1)) = (2 ยท (2โ(((2 ยท ๐ฆ) โ 1) โ 1)))) |
72 | 34, 35, 37 | mul12d 11427 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ โ โค) โ (๐ ยท (2 ยท ๐ฆ)) = (2 ยท (๐ ยท ๐ฆ))) |
73 | 71, 72 | oveq12d 7429 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ
((2โ((2 ยท ๐ฆ)
โ 1)) โ (๐
ยท (2 ยท ๐ฆ))) =
((2 ยท (2โ(((2 ยท ๐ฆ) โ 1) โ 1))) โ (2 ยท
(๐ ยท ๐ฆ)))) |
74 | 34, 37 | mulcld 11238 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง ๐ โ โค) โ (๐ ยท ๐ฆ) โ โ) |
75 | 35, 68, 74 | subdid 11674 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) = ((2 ยท (2โ(((2 ยท
๐ฆ) โ 1) โ 1)))
โ (2 ยท (๐
ยท ๐ฆ)))) |
76 | 75 | eqcomd 2736 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((2
ยท (2โ(((2 ยท ๐ฆ) โ 1) โ 1))) โ (2 ยท
(๐ ยท ๐ฆ))) = (2 ยท ((2โ(((2
ยท ๐ฆ) โ 1)
โ 1)) โ (๐
ยท ๐ฆ)))) |
77 | 73, 76 | eqtrd 2770 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ โ โค) โ
((2โ((2 ยท ๐ฆ)
โ 1)) โ (๐
ยท (2 ยท ๐ฆ))) =
(2 ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ)))) |
78 | 77 | eqeq1d 2732 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(((2โ((2 ยท ๐ฆ)
โ 1)) โ (๐
ยท (2 ยท ๐ฆ))) =
1 โ (2 ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) = 1)) |
79 | | zexpcl 14046 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
โ โค โง (((2 ยท ๐ฆ) โ 1) โ 1) โ
โ0) โ (2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ
โค) |
80 | 19, 66, 79 | sylancr 585 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(2โ(((2 ยท ๐ฆ)
โ 1) โ 1)) โ โค) |
81 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ โ โค) โ ๐ โ
โค) |
82 | | nnz 12583 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
83 | 82 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ โ โค) โ ๐ฆ โ
โค) |
84 | 81, 83 | zmulcld 12676 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง ๐ โ โค) โ (๐ ยท ๐ฆ) โ โค) |
85 | 80, 84 | zsubcld 12675 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ โ โค) โ
((2โ(((2 ยท ๐ฆ)
โ 1) โ 1)) โ (๐ ยท ๐ฆ)) โ โค) |
86 | | m2even 46620 |
. . . . . . . . . . . . . . . . . . 19
โข
(((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ)) โ โค โ (2 ยท
((2โ(((2 ยท ๐ฆ)
โ 1) โ 1)) โ (๐ ยท ๐ฆ))) โ Even ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) โ Even ) |
88 | | 1oddALTV 46656 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
Odd |
89 | | zneoALTV 46635 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) โ Even โง 1 โ Odd ) โ
(2 ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) โ 1) |
90 | 87, 88, 89 | sylancl 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ โ โค) โ (2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) โ 1) |
91 | | eqneqall 2949 |
. . . . . . . . . . . . . . . . 17
โข ((2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) = 1 โ ((2 ยท ((2โ(((2
ยท ๐ฆ) โ 1)
โ 1)) โ (๐
ยท ๐ฆ))) โ 1 โ
๐ โ Odd
)) |
92 | 90, 91 | syl5com 31 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ โ โค) โ ((2
ยท ((2โ(((2 ยท ๐ฆ) โ 1) โ 1)) โ (๐ ยท ๐ฆ))) = 1 โ ๐ โ Odd )) |
93 | 78, 92 | sylbid 239 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง ๐ โ โค) โ
(((2โ((2 ยท ๐ฆ)
โ 1)) โ (๐
ยท (2 ยท ๐ฆ))) =
1 โ ๐ โ Odd
)) |
94 | 44, 93 | sylbird 259 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ โง ๐ โ โค) โ
((2โ((2 ยท ๐ฆ)
โ 1)) = ((๐ ยท
(2 ยท ๐ฆ)) + 1) โ
๐ โ Odd
)) |
95 | 94 | rexlimdva 3153 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ
(โ๐ โ โค
(2โ((2 ยท ๐ฆ)
โ 1)) = ((๐ ยท
(2 ยท ๐ฆ)) + 1) โ
๐ โ Odd
)) |
96 | 29, 95 | syld 47 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ
(((2โ((2 ยท ๐ฆ)
โ 1)) mod (2 ยท ๐ฆ)) = 1 โ ๐ โ Odd )) |
97 | 96 | adantl 480 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ฆ โ โ) โ (((2โ((2
ยท ๐ฆ) โ 1)) mod
(2 ยท ๐ฆ)) = 1 โ
๐ โ Odd
)) |
98 | 97 | adantr 479 |
. . . . . . . . . 10
โข (((๐ โ
(โคโฅโ4) โง ๐ฆ โ โ) โง ๐ = (2 ยท ๐ฆ)) โ (((2โ((2 ยท ๐ฆ) โ 1)) mod (2 ยท
๐ฆ)) = 1 โ ๐ โ Odd )) |
99 | 18, 98 | sylbid 239 |
. . . . . . . . 9
โข (((๐ โ
(โคโฅโ4) โง ๐ฆ โ โ) โง ๐ = (2 ยท ๐ฆ)) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ ๐ โ Odd )) |
100 | 99 | ex 411 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ4) โง ๐ฆ โ โ) โ (๐ = (2 ยท ๐ฆ) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ ๐ โ Odd ))) |
101 | 100 | rexlimdva 3153 |
. . . . . . 7
โข (๐ โ
(โคโฅโ4) โ (โ๐ฆ โ โ ๐ = (2 ยท ๐ฆ) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ ๐ โ Odd ))) |
102 | 101 | com23 86 |
. . . . . 6
โข (๐ โ
(โคโฅโ4) โ (((2โ(๐ โ 1)) mod ๐) = 1 โ (โ๐ฆ โ โ ๐ = (2 ยท ๐ฆ) โ ๐ โ Odd ))) |
103 | 102 | imp 405 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (โ๐ฆ โ โ ๐ = (2 ยท ๐ฆ) โ ๐ โ Odd )) |
104 | 12, 103 | syld 47 |
. . . 4
โข ((๐ โ
(โคโฅโ4) โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (ยฌ ๐ โ Odd โ ๐ โ Odd )) |
105 | 104 | 3adant2 1129 |
. . 3
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ โง ((2โ(๐ โ 1)) mod ๐) = 1) โ (ยฌ ๐ โ Odd โ ๐ โ Odd )) |
106 | 3, 105 | sylbi 216 |
. 2
โข (๐ โ ( FPPr โ2) โ
(ยฌ ๐ โ Odd โ
๐ โ Odd
)) |
107 | 106 | pm2.18d 127 |
1
โข (๐ โ ( FPPr โ2) โ
๐ โ Odd
) |