Step | Hyp | Ref
| Expression |
1 | | breq1 5152 |
. . . . . . 7
β’ (π = 2 β (π β₯ (FermatNoβπ) β 2 β₯ (FermatNoβπ))) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π = 2 β§ π β β) β (π β₯ (FermatNoβπ) β 2 β₯ (FermatNoβπ))) |
3 | | nnnn0 12479 |
. . . . . . . . 9
β’ (π β β β π β
β0) |
4 | | fmtnoodd 46201 |
. . . . . . . . 9
β’ (π β β0
β Β¬ 2 β₯ (FermatNoβπ)) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β β β Β¬ 2
β₯ (FermatNoβπ)) |
6 | 5 | adantl 483 |
. . . . . . 7
β’ ((π = 2 β§ π β β) β Β¬ 2 β₯
(FermatNoβπ)) |
7 | 6 | pm2.21d 121 |
. . . . . 6
β’ ((π = 2 β§ π β β) β (2 β₯
(FermatNoβπ) β
βπ β β
π = ((π Β· (2β(π + 1))) + 1))) |
8 | 2, 7 | sylbid 239 |
. . . . 5
β’ ((π = 2 β§ π β β) β (π β₯ (FermatNoβπ) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
9 | 8 | a1d 25 |
. . . 4
β’ ((π = 2 β§ π β β) β (π β β β (π β₯ (FermatNoβπ) β βπ β β π = ((π Β· (2β(π + 1))) + 1)))) |
10 | 9 | ex 414 |
. . 3
β’ (π = 2 β (π β β β (π β β β (π β₯ (FermatNoβπ) β βπ β β π = ((π Β· (2β(π + 1))) + 1))))) |
11 | 10 | 3impd 1349 |
. 2
β’ (π = 2 β ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
12 | | simpr1 1195 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β π β β) |
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
β’ ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β (Β¬ π = 2 β π β (β β
{2}))) |
19 | 18 | impcom 409 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β π β (β β
{2})) |
20 | | simpr3 1197 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β π β₯ (FermatNoβπ)) |
21 | | fmtnoprmfac1lem 46232 |
. . . . 5
β’ ((π β β β§ π β (β β {2})
β§ π β₯
(FermatNoβπ)) β
((odβ€βπ)β2) = (2β(π + 1))) |
22 | 12, 19, 20, 21 | syl3anc 1372 |
. . . 4
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β
((odβ€βπ)β2) = (2β(π + 1))) |
23 | | prmnn 16611 |
. . . . . . . 8
β’ (π β β β π β
β) |
24 | 23 | ad2antll 728 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β π β
β) |
25 | | 2z 12594 |
. . . . . . . 8
β’ 2 β
β€ |
26 | 25 | a1i 11 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β 2
β β€) |
27 | 13 | necomd 2997 |
. . . . . . . . 9
β’ (Β¬
π = 2 β 2 β π) |
28 | 27 | adantr 482 |
. . . . . . . 8
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β 2 β
π) |
29 | | 2prm 16629 |
. . . . . . . . . . . 12
β’ 2 β
β |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β) |
31 | 30 | anim1i 616 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (2
β β β§ π
β β)) |
32 | 31 | adantl 483 |
. . . . . . . . 9
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β (2
β β β§ π
β β)) |
33 | | prmrp 16649 |
. . . . . . . . 9
β’ ((2
β β β§ π
β β) β ((2 gcd π) = 1 β 2 β π)) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β ((2 gcd
π) = 1 β 2 β π)) |
35 | 28, 34 | mpbird 257 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β (2 gcd
π) = 1) |
36 | | odzphi 16729 |
. . . . . . 7
β’ ((π β β β§ 2 β
β€ β§ (2 gcd π) =
1) β ((odβ€βπ)β2) β₯ (Οβπ)) |
37 | 24, 26, 35, 36 | syl3anc 1372 |
. . . . . 6
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
((odβ€βπ)β2) β₯ (Οβπ)) |
38 | | phiprm 16710 |
. . . . . . . . 9
β’ (π β β β
(Οβπ) = (π β 1)) |
39 | 38 | ad2antll 728 |
. . . . . . . 8
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(Οβπ) = (π β 1)) |
40 | 39 | breq2d 5161 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(((odβ€βπ)β2) β₯ (Οβπ) β
((odβ€βπ)β2) β₯ (π β 1))) |
41 | | breq1 5152 |
. . . . . . . . . . 11
β’
(((odβ€βπ)β2) = (2β(π + 1)) β
(((odβ€βπ)β2) β₯ (π β 1) β (2β(π + 1)) β₯ (π β 1))) |
42 | 41 | adantl 483 |
. . . . . . . . . 10
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§
((odβ€βπ)β2) = (2β(π + 1))) β
(((odβ€βπ)β2) β₯ (π β 1) β (2β(π + 1)) β₯ (π β 1))) |
43 | | 2nn 12285 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 2 β
β) |
45 | | peano2nn 12224 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π + 1) β
β) |
46 | 45 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β0) |
47 | 44, 46 | nnexpcld 14208 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(2β(π + 1)) β
β) |
48 | 23 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β0) |
49 | | prmuz2 16633 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
(β€β₯β2)) |
50 | | eluzle 12835 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β2) β 2 β€ π) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 2 β€
π) |
52 | | nn0ge2m1nn 12541 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ 2 β€ π) β
(π β 1) β
β) |
53 | 48, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β 1) β
β) |
54 | 47, 53 | anim12i 614 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β
((2β(π + 1)) β
β β§ (π β 1)
β β)) |
55 | 54 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
((2β(π + 1)) β
β β§ (π β 1)
β β)) |
56 | | nndivides 16207 |
. . . . . . . . . . . . 13
β’
(((2β(π + 1))
β β β§ (π
β 1) β β) β ((2β(π + 1)) β₯ (π β 1) β βπ β β (π Β· (2β(π + 1))) = (π β 1))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
((2β(π + 1)) β₯
(π β 1) β
βπ β β
(π Β· (2β(π + 1))) = (π β 1))) |
58 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
β’ ((π Β· (2β(π + 1))) = (π β 1) β (π β 1) = (π Β· (2β(π + 1)))) |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§ π β β) β ((π Β· (2β(π + 1))) = (π β 1) β (π β 1) = (π Β· (2β(π + 1))))) |
60 | 23 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β π β
β) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β β) β π β
β) |
63 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β β) β 1 β
β) |
64 | | nncn 12220 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
65 | 64 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β β) β π β
β) |
66 | | peano2nn0 12512 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (π + 1) β
β0) |
67 | 3, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (π + 1) β
β0) |
68 | 44, 67 | nnexpcld 14208 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
(2β(π + 1)) β
β) |
69 | 68 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β
(2β(π + 1)) β
β) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β
(2β(π + 1)) β
β) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β β) β
(2β(π + 1)) β
β) |
72 | 65, 71 | mulcld 11234 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β β) β (π Β· (2β(π + 1))) β
β) |
73 | 62, 63, 72 | subadd2d 11590 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ π β β) β ((π β 1) = (π Β· (2β(π + 1))) β ((π Β· (2β(π + 1))) + 1) = π)) |
74 | 73 | adantll 713 |
. . . . . . . . . . . . . . 15
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§ π β β) β ((π β 1) = (π Β· (2β(π + 1))) β ((π Β· (2β(π + 1))) + 1) = π)) |
75 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
β’ (((π Β· (2β(π + 1))) + 1) = π β π = ((π Β· (2β(π + 1))) + 1)) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§ π β β) β (((π Β· (2β(π + 1))) + 1) = π β π = ((π Β· (2β(π + 1))) + 1))) |
77 | 59, 74, 76 | 3bitrd 305 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§ π β β) β ((π Β· (2β(π + 1))) = (π β 1) β π = ((π Β· (2β(π + 1))) + 1))) |
78 | 77 | rexbidva 3177 |
. . . . . . . . . . . . 13
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(βπ β β
(π Β· (2β(π + 1))) = (π β 1) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
79 | 78 | biimpd 228 |
. . . . . . . . . . . 12
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(βπ β β
(π Β· (2β(π + 1))) = (π β 1) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
80 | 57, 79 | sylbid 239 |
. . . . . . . . . . 11
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
((2β(π + 1)) β₯
(π β 1) β
βπ β β
π = ((π Β· (2β(π + 1))) + 1))) |
81 | 80 | adantr 482 |
. . . . . . . . . 10
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§
((odβ€βπ)β2) = (2β(π + 1))) β ((2β(π + 1)) β₯ (π β 1) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
82 | 42, 81 | sylbid 239 |
. . . . . . . . 9
β’ (((Β¬
π = 2 β§ (π β β β§ π β β)) β§
((odβ€βπ)β2) = (2β(π + 1))) β
(((odβ€βπ)β2) β₯ (π β 1) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
83 | 82 | ex 414 |
. . . . . . . 8
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(((odβ€βπ)β2) = (2β(π + 1)) β
(((odβ€βπ)β2) β₯ (π β 1) β βπ β β π = ((π Β· (2β(π + 1))) + 1)))) |
84 | 83 | com23 86 |
. . . . . . 7
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(((odβ€βπ)β2) β₯ (π β 1) β
(((odβ€βπ)β2) = (2β(π + 1)) β βπ β β π = ((π Β· (2β(π + 1))) + 1)))) |
85 | 40, 84 | sylbid 239 |
. . . . . 6
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(((odβ€βπ)β2) β₯ (Οβπ) β
(((odβ€βπ)β2) = (2β(π + 1)) β βπ β β π = ((π Β· (2β(π + 1))) + 1)))) |
86 | 37, 85 | mpd 15 |
. . . . 5
β’ ((Β¬
π = 2 β§ (π β β β§ π β β)) β
(((odβ€βπ)β2) = (2β(π + 1)) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
87 | 86 | 3adantr3 1172 |
. . . 4
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β
(((odβ€βπ)β2) = (2β(π + 1)) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
88 | 22, 87 | mpd 15 |
. . 3
β’ ((Β¬
π = 2 β§ (π β β β§ π β β β§ π β₯ (FermatNoβπ))) β βπ β β π = ((π Β· (2β(π + 1))) + 1)) |
89 | 88 | ex 414 |
. 2
β’ (Β¬
π = 2 β ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 1))) + 1))) |
90 | 11, 89 | pm2.61i 182 |
1
β’ ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 1))) + 1)) |