Step | Hyp | Ref
| Expression |
1 | | breq1 5152 |
. . . . . . 7
β’ (π = 2 β (π β₯ (FermatNoβπ) β 2 β₯ (FermatNoβπ))) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π = 2 β§ π β (β€β₯β2))
β (π β₯
(FermatNoβπ) β 2
β₯ (FermatNoβπ))) |
3 | | eluzge2nn0 12871 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β π β
β0) |
4 | | fmtnoodd 46201 |
. . . . . . . . 9
β’ (π β β0
β Β¬ 2 β₯ (FermatNoβπ)) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β Β¬ 2 β₯ (FermatNoβπ)) |
6 | 5 | adantl 483 |
. . . . . . 7
β’ ((π = 2 β§ π β (β€β₯β2))
β Β¬ 2 β₯ (FermatNoβπ)) |
7 | 6 | pm2.21d 121 |
. . . . . 6
β’ ((π = 2 β§ π β (β€β₯β2))
β (2 β₯ (FermatNoβπ) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
8 | 2, 7 | sylbid 239 |
. . . . 5
β’ ((π = 2 β§ π β (β€β₯β2))
β (π β₯
(FermatNoβπ) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))) |
9 | 8 | a1d 25 |
. . . 4
β’ ((π = 2 β§ π β (β€β₯β2))
β (π β β
β (π β₯
(FermatNoβπ) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1)))) |
10 | 9 | ex 414 |
. . 3
β’ (π = 2 β (π β (β€β₯β2)
β (π β β
β (π β₯
(FermatNoβπ) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))))) |
11 | 10 | 3impd 1349 |
. 2
β’ (π = 2 β ((π β (β€β₯β2)
β§ π β β
β§ π β₯
(FermatNoβπ)) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))) |
12 | | simpr1 1195 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β π β
(β€β₯β2)) |
13 | | neqne 2949 |
. . . . . . . . . 10
β’ (Β¬
π = 2 β π β 2) |
14 | 13 | anim2i 618 |
. . . . . . . . 9
β’ ((π β β β§ Β¬
π = 2) β (π β β β§ π β 2)) |
15 | | eldifsn 4791 |
. . . . . . . . 9
β’ (π β (β β {2})
β (π β β
β§ π β
2)) |
16 | 14, 15 | sylibr 233 |
. . . . . . . 8
β’ ((π β β β§ Β¬
π = 2) β π β (β β
{2})) |
17 | 16 | ex 414 |
. . . . . . 7
β’ (π β β β (Β¬
π = 2 β π β (β β
{2}))) |
18 | 17 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β (Β¬ π = 2 β π β (β β
{2}))) |
19 | 18 | impcom 409 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β π β (β β
{2})) |
20 | | simpr3 1197 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β π β₯ (FermatNoβπ)) |
21 | | fmtnoprmfac2lem1 46234 |
. . . . 5
β’ ((π β
(β€β₯β2) β§ π β (β β {2}) β§ π β₯ (FermatNoβπ)) β ((2β((π β 1) / 2)) mod π) = 1) |
22 | 12, 19, 20, 21 | syl3anc 1372 |
. . . 4
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β ((2β((π β 1) / 2)) mod π) = 1) |
23 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β β§ Β¬
π = 2) β π β
β) |
24 | | 2nn 12285 |
. . . . . . . . . . . . 13
β’ 2 β
β |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β β§ Β¬
π = 2) β 2 β
β) |
26 | | oddprm 16743 |
. . . . . . . . . . . . . 14
β’ (π β (β β {2})
β ((π β 1) / 2)
β β) |
27 | 16, 26 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β β§ Β¬
π = 2) β ((π β 1) / 2) β
β) |
28 | 27 | nnnn0d 12532 |
. . . . . . . . . . . 12
β’ ((π β β β§ Β¬
π = 2) β ((π β 1) / 2) β
β0) |
29 | 25, 28 | nnexpcld 14208 |
. . . . . . . . . . 11
β’ ((π β β β§ Β¬
π = 2) β
(2β((π β 1) /
2)) β β) |
30 | 29 | nnzd 12585 |
. . . . . . . . . 10
β’ ((π β β β§ Β¬
π = 2) β
(2β((π β 1) /
2)) β β€) |
31 | 23, 30 | jca 513 |
. . . . . . . . 9
β’ ((π β β β§ Β¬
π = 2) β (π β β β§
(2β((π β 1) /
2)) β β€)) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ (π β β β (Β¬
π = 2 β (π β β β§
(2β((π β 1) /
2)) β β€))) |
33 | 32 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β (Β¬ π = 2 β (π β β β§ (2β((π β 1) / 2)) β
β€))) |
34 | 33 | impcom 409 |
. . . . . 6
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β (π β β β§ (2β((π β 1) / 2)) β
β€)) |
35 | | modprm1div 16730 |
. . . . . 6
β’ ((π β β β§
(2β((π β 1) /
2)) β β€) β (((2β((π β 1) / 2)) mod π) = 1 β π β₯ ((2β((π β 1) / 2)) β
1))) |
36 | 34, 35 | syl 17 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β (((2β((π β 1) / 2)) mod π) = 1 β π β₯ ((2β((π β 1) / 2)) β
1))) |
37 | | prmnn 16611 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
38 | 37 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β β§ Β¬
π = 2) β π β
β) |
39 | | 2z 12594 |
. . . . . . . . . . . . 13
β’ 2 β
β€ |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β β§ Β¬
π = 2) β 2 β
β€) |
41 | 13 | necomd 2997 |
. . . . . . . . . . . . . 14
β’ (Β¬
π = 2 β 2 β π) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ Β¬
π = 2) β 2 β π) |
43 | | 2prm 16629 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π = 2 β 2 β
β) |
45 | 44 | anim2i 618 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ Β¬
π = 2) β (π β β β§ 2 β
β)) |
46 | 45 | ancomd 463 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ Β¬
π = 2) β (2 β
β β§ π β
β)) |
47 | | prmrp 16649 |
. . . . . . . . . . . . . 14
β’ ((2
β β β§ π
β β) β ((2 gcd π) = 1 β 2 β π)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β β§ Β¬
π = 2) β ((2 gcd π) = 1 β 2 β π)) |
49 | 42, 48 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β β β§ Β¬
π = 2) β (2 gcd π) = 1) |
50 | 38, 40, 49 | 3jca 1129 |
. . . . . . . . . . 11
β’ ((π β β β§ Β¬
π = 2) β (π β β β§ 2 β
β€ β§ (2 gcd π) =
1)) |
51 | 50, 28 | jca 513 |
. . . . . . . . . 10
β’ ((π β β β§ Β¬
π = 2) β ((π β β β§ 2 β
β€ β§ (2 gcd π) =
1) β§ ((π β 1) /
2) β β0)) |
52 | 51 | ex 414 |
. . . . . . . . 9
β’ (π β β β (Β¬
π = 2 β ((π β β β§ 2 β
β€ β§ (2 gcd π) =
1) β§ ((π β 1) /
2) β β0))) |
53 | 52 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β (Β¬ π = 2 β ((π β β β§ 2 β β€ β§
(2 gcd π) = 1) β§
((π β 1) / 2) β
β0))) |
54 | 53 | impcom 409 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β ((π β β β§ 2 β β€ β§
(2 gcd π) = 1) β§
((π β 1) / 2) β
β0)) |
55 | | odzdvds 16728 |
. . . . . . 7
β’ (((π β β β§ 2 β
β€ β§ (2 gcd π) =
1) β§ ((π β 1) /
2) β β0) β (π β₯ ((2β((π β 1) / 2)) β 1) β
((odβ€βπ)β2) β₯ ((π β 1) / 2))) |
56 | 54, 55 | syl 17 |
. . . . . 6
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β (π β₯ ((2β((π β 1) / 2)) β 1) β
((odβ€βπ)β2) β₯ ((π β 1) / 2))) |
57 | | eluz2nn 12868 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β π β β) |
58 | 57 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β π β β) |
59 | 58 | adantl 483 |
. . . . . . . 8
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β π β β) |
60 | | fmtnoprmfac1lem 46232 |
. . . . . . . 8
β’ ((π β β β§ π β (β β {2})
β§ π β₯
(FermatNoβπ)) β
((odβ€βπ)β2) = (2β(π + 1))) |
61 | 59, 19, 20, 60 | syl3anc 1372 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β
((odβ€βπ)β2) = (2β(π + 1))) |
62 | | breq1 5152 |
. . . . . . . . . 10
β’
(((odβ€βπ)β2) = (2β(π + 1)) β
(((odβ€βπ)β2) β₯ ((π β 1) / 2) β (2β(π + 1)) β₯ ((π β 1) /
2))) |
63 | 62 | adantl 483 |
. . . . . . . . 9
β’ (((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β§ ((odβ€βπ)β2) = (2β(π + 1))) β
(((odβ€βπ)β2) β₯ ((π β 1) / 2) β (2β(π + 1)) β₯ ((π β 1) /
2))) |
64 | 24 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β 2 β β) |
65 | | peano2nn 12224 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π + 1) β
β) |
66 | 57, 65 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β2) β (π + 1) β β) |
67 | 66 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β (π + 1) β
β0) |
68 | 64, 67 | nnexpcld 14208 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β2) β (2β(π + 1)) β β) |
69 | | nndivides 16207 |
. . . . . . . . . . . . . . 15
β’
(((2β(π + 1))
β β β§ ((π
β 1) / 2) β β) β ((2β(π + 1)) β₯ ((π β 1) / 2) β βπ β β (π Β· (2β(π + 1))) = ((π β 1) / 2))) |
70 | 68, 27, 69 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β2) β§ (π β β β§ Β¬ π = 2)) β ((2β(π + 1)) β₯ ((π β 1) / 2) β
βπ β β
(π Β· (2β(π + 1))) = ((π β 1) / 2))) |
71 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π Β· (2β(π + 1))) = ((π β 1) / 2) β ((π β 1) / 2) = (π Β· (2β(π + 1)))) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π Β· (2β(π + 1))) = ((π β 1) / 2) β ((π β 1) / 2) = (π Β· (2β(π + 1))))) |
73 | 37 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β π β
β) |
74 | | peano2cnm 11526 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (π β 1) β
β) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (π β 1) β
β) |
76 | 75 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β
(β€β₯β2) β§ π β β) β (π β 1) β β) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (π β 1) β β) |
78 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β π β β) |
79 | 68 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (2β(π + 1)) β
β) |
80 | 78, 79 | nnmulcld 12265 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (π Β· (2β(π + 1))) β β) |
81 | 80 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (π Β· (2β(π + 1))) β β) |
82 | | 2cnne0 12422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (2 β
β β§ 2 β 0) |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (2 β β
β§ 2 β 0)) |
84 | | divmul3 11877 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β 1) β β β§
(π Β· (2β(π + 1))) β β β§ (2
β β β§ 2 β 0)) β (((π β 1) / 2) = (π Β· (2β(π + 1))) β (π β 1) = ((π Β· (2β(π + 1))) Β· 2))) |
85 | 77, 81, 83, 84 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (((π β 1) / 2) = (π Β· (2β(π + 1))) β (π β 1) = ((π Β· (2β(π + 1))) Β· 2))) |
86 | | nncn 12220 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β π β β) |
88 | 68 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β2) β (2β(π + 1)) β β) |
89 | 88 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (2β(π + 1)) β
β) |
90 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β 2 β
β) |
91 | 87, 89, 90 | mulassd 11237 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π Β· (2β(π + 1))) Β· 2) = (π Β· ((2β(π + 1)) Β· 2))) |
92 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β 2 β
β) |
93 | 65 | nnnn0d 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β (π + 1) β
β0) |
94 | 92, 93 | expp1d 14112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β
(2β((π + 1) + 1)) =
((2β(π + 1)) Β·
2)) |
95 | | nncn 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β
β) |
96 | | add1p1 12463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β ((π + 1) + 1) = (π + 2)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β ((π + 1) + 1) = (π + 2)) |
98 | 97 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β
(2β((π + 1) + 1)) =
(2β(π +
2))) |
99 | 94, 98 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β
((2β(π + 1)) Β·
2) = (2β(π +
2))) |
100 | 57, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β2) β ((2β(π + 1)) Β· 2) = (2β(π + 2))) |
101 | 100 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((2β(π + 1)) Β· 2) =
(2β(π +
2))) |
102 | 101 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (π Β· ((2β(π + 1)) Β· 2)) = (π Β· (2β(π + 2)))) |
103 | 91, 102 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π Β· (2β(π + 1))) Β· 2) = (π Β· (2β(π + 2)))) |
104 | 103 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π β 1) = ((π Β· (2β(π + 1))) Β· 2) β (π β 1) = (π Β· (2β(π + 2))))) |
105 | 73 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β
(β€β₯β2) β§ π β β) β π β β) |
106 | 105 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β π β β) |
107 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β 1 β
β) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β
β) |
109 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β 2 β
β) |
110 | 108, 109 | nnaddcld 12264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β (π + 2) β
β) |
111 | 110 | nnnn0d 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π + 2) β
β0) |
112 | 57, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯β2) β (π + 2) β
β0) |
113 | 64, 112 | nnexpcld 14208 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β2) β (2β(π + 2)) β β) |
114 | 113 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯β2) β (2β(π + 2)) β β) |
115 | 114 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (2β(π + 2)) β
β) |
116 | 87, 115 | mulcld 11234 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (π Β· (2β(π + 2))) β β) |
117 | 106, 107,
116 | subadd2d 11590 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π β 1) = (π Β· (2β(π + 2))) β ((π Β· (2β(π + 2))) + 1) = π)) |
118 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π Β· (2β(π + 2))) + 1) = π β π = ((π Β· (2β(π + 2))) + 1)) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β (((π Β· (2β(π + 2))) + 1) = π β π = ((π Β· (2β(π + 2))) + 1))) |
120 | 104, 117,
119 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π β 1) = ((π Β· (2β(π + 1))) Β· 2) β π = ((π Β· (2β(π + 2))) + 1))) |
121 | 72, 85, 120 | 3bitrd 305 |
. . . . . . . . . . . . . . . . 17
β’ (((π β
(β€β₯β2) β§ π β β) β§ π β β) β ((π Β· (2β(π + 1))) = ((π β 1) / 2) β π = ((π Β· (2β(π + 2))) + 1))) |
122 | 121 | rexbidva 3177 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β2) β§ π β β) β (βπ β β (π Β· (2β(π + 1))) = ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
123 | 122 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β2) β§ π β β) β (βπ β β (π Β· (2β(π + 1))) = ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
124 | 123 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β2) β§ (π β β β§ Β¬ π = 2)) β (βπ β β (π Β· (2β(π + 1))) = ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
125 | 70, 124 | sylbid 239 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ (π β β β§ Β¬ π = 2)) β ((2β(π + 1)) β₯ ((π β 1) / 2) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))) |
126 | 125 | expr 458 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π β β) β (Β¬ π = 2 β ((2β(π + 1)) β₯ ((π β 1) / 2) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1)))) |
127 | 126 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β (Β¬ π = 2 β ((2β(π + 1)) β₯ ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1)))) |
128 | 127 | impcom 409 |
. . . . . . . . . 10
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β ((2β(π + 1)) β₯ ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
129 | 128 | adantr 482 |
. . . . . . . . 9
β’ (((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β§ ((odβ€βπ)β2) = (2β(π + 1))) β ((2β(π + 1)) β₯ ((π β 1) / 2) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))) |
130 | 63, 129 | sylbid 239 |
. . . . . . . 8
β’ (((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β§ ((odβ€βπ)β2) = (2β(π + 1))) β
(((odβ€βπ)β2) β₯ ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
131 | 130 | ex 414 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β
(((odβ€βπ)β2) = (2β(π + 1)) β
(((odβ€βπ)β2) β₯ ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1)))) |
132 | 61, 131 | mpd 15 |
. . . . . 6
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β
(((odβ€βπ)β2) β₯ ((π β 1) / 2) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
133 | 56, 132 | sylbid 239 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β (π β₯ ((2β((π β 1) / 2)) β 1) β
βπ β β
π = ((π Β· (2β(π + 2))) + 1))) |
134 | 36, 133 | sylbid 239 |
. . . 4
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β (((2β((π β 1) / 2)) mod π) = 1 β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
135 | 22, 134 | mpd 15 |
. . 3
β’ ((Β¬
π = 2 β§ (π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ))) β βπ β β π = ((π Β· (2β(π + 2))) + 1)) |
136 | 135 | ex 414 |
. 2
β’ (Β¬
π = 2 β ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 2))) + 1))) |
137 | 11, 136 | pm2.61i 182 |
1
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 2))) + 1)) |