Step | Hyp | Ref
| Expression |
1 | | elnn1uz2 12857 |
. . 3
β’ (π β β β (π = 1 β¨ π β
(β€β₯β2))) |
2 | | 5prm 16988 |
. . . . . . 7
β’ 5 β
β |
3 | | dvdsprime 16570 |
. . . . . . 7
β’ ((5
β β β§ π
β β) β (π
β₯ 5 β (π = 5
β¨ π =
1))) |
4 | 2, 3 | mpan 689 |
. . . . . 6
β’ (π β β β (π β₯ 5 β (π = 5 β¨ π = 1))) |
5 | | 1nn0 12436 |
. . . . . . . . 9
β’ 1 β
β0 |
6 | 5 | a1i 11 |
. . . . . . . 8
β’ (π = 5 β 1 β
β0) |
7 | | simpl 484 |
. . . . . . . . 9
β’ ((π = 5 β§ π = 1) β π = 5) |
8 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π = 1 β (π Β· 4) = (1 Β·
4)) |
9 | 8 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = 1 β ((π Β· 4) + 1) = ((1 Β· 4) +
1)) |
10 | 9 | adantl 483 |
. . . . . . . . 9
β’ ((π = 5 β§ π = 1) β ((π Β· 4) + 1) = ((1 Β· 4) +
1)) |
11 | 7, 10 | eqeq12d 2753 |
. . . . . . . 8
β’ ((π = 5 β§ π = 1) β (π = ((π Β· 4) + 1) β 5 = ((1 Β· 4)
+ 1))) |
12 | | df-5 12226 |
. . . . . . . . . 10
β’ 5 = (4 +
1) |
13 | | 4cn 12245 |
. . . . . . . . . . . . 13
β’ 4 β
β |
14 | 13 | mulid2i 11167 |
. . . . . . . . . . . 12
β’ (1
Β· 4) = 4 |
15 | 14 | eqcomi 2746 |
. . . . . . . . . . 11
β’ 4 = (1
Β· 4) |
16 | 15 | oveq1i 7372 |
. . . . . . . . . 10
β’ (4 + 1) =
((1 Β· 4) + 1) |
17 | 12, 16 | eqtri 2765 |
. . . . . . . . 9
β’ 5 = ((1
Β· 4) + 1) |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ (π = 5 β 5 = ((1 Β· 4)
+ 1)) |
19 | 6, 11, 18 | rspcedvd 3586 |
. . . . . . 7
β’ (π = 5 β βπ β β0
π = ((π Β· 4) + 1)) |
20 | | 0nn0 12435 |
. . . . . . . . 9
β’ 0 β
β0 |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ (π = 1 β 0 β
β0) |
22 | | simpl 484 |
. . . . . . . . 9
β’ ((π = 1 β§ π = 0) β π = 1) |
23 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π = 0 β (π Β· 4) = (0 Β·
4)) |
24 | 23 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = 0 β ((π Β· 4) + 1) = ((0 Β· 4) +
1)) |
25 | 24 | adantl 483 |
. . . . . . . . 9
β’ ((π = 1 β§ π = 0) β ((π Β· 4) + 1) = ((0 Β· 4) +
1)) |
26 | 22, 25 | eqeq12d 2753 |
. . . . . . . 8
β’ ((π = 1 β§ π = 0) β (π = ((π Β· 4) + 1) β 1 = ((0 Β· 4)
+ 1))) |
27 | 13 | mul02i 11351 |
. . . . . . . . . . . 12
β’ (0
Β· 4) = 0 |
28 | 27 | oveq1i 7372 |
. . . . . . . . . . 11
β’ ((0
Β· 4) + 1) = (0 + 1) |
29 | | 0p1e1 12282 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
30 | 28, 29 | eqtri 2765 |
. . . . . . . . . 10
β’ ((0
Β· 4) + 1) = 1 |
31 | 30 | eqcomi 2746 |
. . . . . . . . 9
β’ 1 = ((0
Β· 4) + 1) |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ (π = 1 β 1 = ((0 Β· 4)
+ 1)) |
33 | 21, 26, 32 | rspcedvd 3586 |
. . . . . . 7
β’ (π = 1 β βπ β β0
π = ((π Β· 4) + 1)) |
34 | 19, 33 | jaoi 856 |
. . . . . 6
β’ ((π = 5 β¨ π = 1) β βπ β β0 π = ((π Β· 4) + 1)) |
35 | 4, 34 | syl6bi 253 |
. . . . 5
β’ (π β β β (π β₯ 5 β βπ β β0
π = ((π Β· 4) + 1))) |
36 | | fveq2 6847 |
. . . . . . . 8
β’ (π = 1 β
(FermatNoβπ) =
(FermatNoβ1)) |
37 | | fmtno1 45807 |
. . . . . . . 8
β’
(FermatNoβ1) = 5 |
38 | 36, 37 | eqtrdi 2793 |
. . . . . . 7
β’ (π = 1 β
(FermatNoβπ) =
5) |
39 | 38 | breq2d 5122 |
. . . . . 6
β’ (π = 1 β (π β₯ (FermatNoβπ) β π β₯ 5)) |
40 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π + 1) = (1 + 1)) |
41 | | 1p1e2 12285 |
. . . . . . . . . . . . 13
β’ (1 + 1) =
2 |
42 | 40, 41 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π = 1 β (π + 1) = 2) |
43 | 42 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = 1 β (2β(π + 1)) =
(2β2)) |
44 | | sq2 14108 |
. . . . . . . . . . 11
β’
(2β2) = 4 |
45 | 43, 44 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = 1 β (2β(π + 1)) = 4) |
46 | 45 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = 1 β (π Β· (2β(π + 1))) = (π Β· 4)) |
47 | 46 | oveq1d 7377 |
. . . . . . . 8
β’ (π = 1 β ((π Β· (2β(π + 1))) + 1) = ((π Β· 4) + 1)) |
48 | 47 | eqeq2d 2748 |
. . . . . . 7
β’ (π = 1 β (π = ((π Β· (2β(π + 1))) + 1) β π = ((π Β· 4) + 1))) |
49 | 48 | rexbidv 3176 |
. . . . . 6
β’ (π = 1 β (βπ β β0
π = ((π Β· (2β(π + 1))) + 1) β βπ β β0
π = ((π Β· 4) + 1))) |
50 | 39, 49 | imbi12d 345 |
. . . . 5
β’ (π = 1 β ((π β₯ (FermatNoβπ) β βπ β β0 π = ((π Β· (2β(π + 1))) + 1)) β (π β₯ 5 β βπ β β0 π = ((π Β· 4) + 1)))) |
51 | 35, 50 | syl5ibr 246 |
. . . 4
β’ (π = 1 β (π β β β (π β₯ (FermatNoβπ) β βπ β β0 π = ((π Β· (2β(π + 1))) + 1)))) |
52 | | fmtnofac2 45835 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1)) |
53 | | id 22 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β0) |
54 | | 2nn0 12437 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
55 | 54 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β0
β 2 β β0) |
56 | 53, 55 | nn0mulcld 12485 |
. . . . . . . . . 10
β’ (π β β0
β (π Β· 2)
β β0) |
57 | 56 | adantl 483 |
. . . . . . . . 9
β’ (((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β (π Β· 2) β
β0) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ ((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β (π Β· 2) β
β0) |
59 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β π = ((π Β· (2β(π + 2))) + 1)) |
60 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = (π Β· 2) β (π Β· (2β(π + 1))) = ((π Β· 2) Β· (2β(π + 1)))) |
61 | 60 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = (π Β· 2) β ((π Β· (2β(π + 1))) + 1) = (((π Β· 2) Β· (2β(π + 1))) + 1)) |
62 | 59, 61 | eqeqan12d 2751 |
. . . . . . . 8
β’
(((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β§ π = (π Β· 2)) β (π = ((π Β· (2β(π + 1))) + 1) β ((π Β· (2β(π + 2))) + 1) = (((π Β· 2) Β· (2β(π + 1))) + 1))) |
63 | | eluzge2nn0 12819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β2) β π β
β0) |
64 | 63 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β2) β π β β) |
65 | | add1p1 12411 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((π + 1) + 1) = (π + 2)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β2) β ((π + 1) + 1) = (π + 2)) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β (π + 2) = ((π + 1) + 1)) |
68 | 67 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β2) β (2β(π + 2)) = (2β((π + 1) + 1))) |
69 | | 2cnd 12238 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β 2 β β) |
70 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
β0) |
71 | 63, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β (π + 1) β
β0) |
72 | 69, 71 | expp1d 14059 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β2) β (2β((π + 1) + 1)) = ((2β(π + 1)) Β· 2)) |
73 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β2) β 2 β
β0) |
74 | 73, 71 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β2) β (2β(π + 1)) β
β0) |
75 | 74 | nn0cnd 12482 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β2) β (2β(π + 1)) β β) |
76 | 75, 69 | mulcomd 11183 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β2) β ((2β(π + 1)) Β· 2) = (2 Β·
(2β(π +
1)))) |
77 | 68, 72, 76 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β2) β (2β(π + 2)) = (2 Β· (2β(π + 1)))) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ π β β0) β
(2β(π + 2)) = (2
Β· (2β(π +
1)))) |
79 | 78 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π β β0) β (π Β· (2β(π + 2))) = (π Β· (2 Β· (2β(π + 1))))) |
80 | | nn0cn 12430 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
81 | 80 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ π β β0) β π β
β) |
82 | | 2cnd 12238 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ π β β0) β 2 β
β) |
83 | 75 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ π β β0) β
(2β(π + 1)) β
β) |
84 | 81, 82, 83 | mulassd 11185 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π β β0) β ((π Β· 2) Β·
(2β(π + 1))) = (π Β· (2 Β·
(2β(π +
1))))) |
85 | 79, 84 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β2) β§ π β β0) β (π Β· (2β(π + 2))) = ((π Β· 2) Β· (2β(π + 1)))) |
86 | 85 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β (π Β· (2β(π + 2))) = ((π Β· 2) Β· (2β(π + 1)))) |
87 | 86 | adantr 482 |
. . . . . . . . 9
β’ ((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β (π Β· (2β(π + 2))) = ((π Β· 2) Β· (2β(π + 1)))) |
88 | 87 | oveq1d 7377 |
. . . . . . . 8
β’ ((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β ((π Β· (2β(π + 2))) + 1) = (((π Β· 2) Β· (2β(π + 1))) + 1)) |
89 | 58, 62, 88 | rspcedvd 3586 |
. . . . . . 7
β’ ((((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β§ π β β0) β§ π = ((π Β· (2β(π + 2))) + 1)) β βπ β β0
π = ((π Β· (2β(π + 1))) + 1)) |
90 | 89 | rexlimdva2 3155 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β (βπ β β0 π = ((π Β· (2β(π + 2))) + 1) β βπ β β0
π = ((π Β· (2β(π + 1))) + 1))) |
91 | 52, 90 | mpd 15 |
. . . . 5
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 1))) + 1)) |
92 | 91 | 3exp 1120 |
. . . 4
β’ (π β
(β€β₯β2) β (π β β β (π β₯ (FermatNoβπ) β βπ β β0 π = ((π Β· (2β(π + 1))) + 1)))) |
93 | 51, 92 | jaoi 856 |
. . 3
β’ ((π = 1 β¨ π β (β€β₯β2))
β (π β β
β (π β₯
(FermatNoβπ) β
βπ β
β0 π =
((π Β· (2β(π + 1))) + 1)))) |
94 | 1, 93 | sylbi 216 |
. 2
β’ (π β β β (π β β β (π β₯ (FermatNoβπ) β βπ β β0
π = ((π Β· (2β(π + 1))) + 1)))) |
95 | 94 | 3imp 1112 |
1
β’ ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0
π = ((π Β· (2β(π + 1))) + 1)) |