Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((π β β0
β§ π β β)
β π β
β0) |
2 | | nn0nnaddcl 12451 |
. . . . 5
β’ ((π β β0
β§ π β β)
β (π + π) β
β) |
3 | | nnm1nn0 12461 |
. . . . 5
β’ ((π + π) β β β ((π + π) β 1) β
β0) |
4 | 2, 3 | syl 17 |
. . . 4
β’ ((π β β0
β§ π β β)
β ((π + π) β 1) β
β0) |
5 | | 1red 11163 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β 1 β β) |
6 | | nnre 12167 |
. . . . . . 7
β’ (π β β β π β
β) |
7 | 6 | adantl 483 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β π β
β) |
8 | | nn0re 12429 |
. . . . . . 7
β’ (π β β0
β π β
β) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β π β
β) |
10 | | nnge1 12188 |
. . . . . . 7
β’ (π β β β 1 β€
π) |
11 | 10 | adantl 483 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β 1 β€ π) |
12 | 5, 7, 9, 11 | leadd2dd 11777 |
. . . . 5
β’ ((π β β0
β§ π β β)
β (π + 1) β€ (π + π)) |
13 | | readdcl 11141 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π + π) β β) |
14 | 8, 6, 13 | syl2an 597 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β (π + π) β
β) |
15 | | leaddsub 11638 |
. . . . . 6
β’ ((π β β β§ 1 β
β β§ (π + π) β β) β ((π + 1) β€ (π + π) β π β€ ((π + π) β 1))) |
16 | 9, 5, 14, 15 | syl3anc 1372 |
. . . . 5
β’ ((π β β0
β§ π β β)
β ((π + 1) β€ (π + π) β π β€ ((π + π) β 1))) |
17 | 12, 16 | mpbid 231 |
. . . 4
β’ ((π β β0
β§ π β β)
β π β€ ((π + π) β 1)) |
18 | | elfz2nn0 13539 |
. . . 4
β’ (π β (0...((π + π) β 1)) β (π β β0 β§ ((π + π) β 1) β β0
β§ π β€ ((π + π) β 1))) |
19 | 1, 4, 17, 18 | syl3anbrc 1344 |
. . 3
β’ ((π β β0
β§ π β β)
β π β
(0...((π + π) β 1))) |
20 | | fzfid 13885 |
. . . 4
β’ ((π β β0
β§ π β β)
β (0...((π + π) β 1)) β
Fin) |
21 | | fz0ssnn0 13543 |
. . . . 5
β’
(0...((π + π) β 1)) β
β0 |
22 | 21 | a1i 11 |
. . . 4
β’ ((π β β0
β§ π β β)
β (0...((π + π) β 1)) β
β0) |
23 | | 2nn0 12437 |
. . . . . . . . . 10
β’ 2 β
β0 |
24 | 23 | a1i 11 |
. . . . . . . . 9
β’ (π β β0
β 2 β β0) |
25 | | id 22 |
. . . . . . . . . 10
β’ (π β β0
β π β
β0) |
26 | 24, 25 | nn0expcld 14156 |
. . . . . . . . 9
β’ (π β β0
β (2βπ) β
β0) |
27 | 24, 26 | nn0expcld 14156 |
. . . . . . . 8
β’ (π β β0
β (2β(2βπ))
β β0) |
28 | 27 | nn0zd 12532 |
. . . . . . 7
β’ (π β β0
β (2β(2βπ))
β β€) |
29 | 28 | peano2zd 12617 |
. . . . . 6
β’ (π β β0
β ((2β(2βπ))
+ 1) β β€) |
30 | 29 | adantl 483 |
. . . . 5
β’ (((π β β0
β§ π β β)
β§ π β
β0) β ((2β(2βπ)) + 1) β β€) |
31 | | df-fmtno 45794 |
. . . . 5
β’ FermatNo
= (π β
β0 β¦ ((2β(2βπ)) + 1)) |
32 | 30, 31 | fmptd 7067 |
. . . 4
β’ ((π β β0
β§ π β β)
β FermatNo:β0βΆβ€) |
33 | 20, 22, 32 | fprodfvdvdsd 16223 |
. . 3
β’ ((π β β0
β§ π β β)
β βπ β
(0...((π + π) β
1))(FermatNoβπ)
β₯ βπ β
(0...((π + π) β
1))(FermatNoβπ)) |
34 | | fveq2 6847 |
. . . . 5
β’ (π = π β (FermatNoβπ) = (FermatNoβπ)) |
35 | 34 | breq1d 5120 |
. . . 4
β’ (π = π β ((FermatNoβπ) β₯ βπ β (0...((π + π) β 1))(FermatNoβπ) β (FermatNoβπ) β₯ βπ β (0...((π + π) β 1))(FermatNoβπ))) |
36 | 35 | rspcv 3580 |
. . 3
β’ (π β (0...((π + π) β 1)) β (βπ β (0...((π + π) β 1))(FermatNoβπ) β₯ βπ β (0...((π + π) β 1))(FermatNoβπ) β (FermatNoβπ) β₯ βπ β (0...((π + π) β 1))(FermatNoβπ))) |
37 | 19, 33, 36 | sylc 65 |
. 2
β’ ((π β β0
β§ π β β)
β (FermatNoβπ)
β₯ βπ β
(0...((π + π) β
1))(FermatNoβπ)) |
38 | | elfznn0 13541 |
. . . . . . 7
β’ (π β (0...((π + π) β 1)) β π β β0) |
39 | 38 | adantl 483 |
. . . . . 6
β’ (((π β β0
β§ π β β)
β§ π β (0...((π + π) β 1))) β π β β0) |
40 | | fmtnonn 45797 |
. . . . . 6
β’ (π β β0
β (FermatNoβπ)
β β) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ (((π β β0
β§ π β β)
β§ π β (0...((π + π) β 1))) β (FermatNoβπ) β
β) |
42 | 41 | nncnd 12176 |
. . . 4
β’ (((π β β0
β§ π β β)
β§ π β (0...((π + π) β 1))) β (FermatNoβπ) β
β) |
43 | 20, 42 | fprodcl 15842 |
. . 3
β’ ((π β β0
β§ π β β)
β βπ β
(0...((π + π) β
1))(FermatNoβπ)
β β) |
44 | | 2cnd 12238 |
. . 3
β’ ((π β β0
β§ π β β)
β 2 β β) |
45 | | nn0cn 12430 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
46 | | nncn 12168 |
. . . . . . . 8
β’ (π β β β π β
β) |
47 | | addcl 11140 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π + π) β β) |
48 | 45, 46, 47 | syl2an 597 |
. . . . . . 7
β’ ((π β β0
β§ π β β)
β (π + π) β
β) |
49 | | npcan1 11587 |
. . . . . . 7
β’ ((π + π) β β β (((π + π) β 1) + 1) = (π + π)) |
50 | 48, 49 | syl 17 |
. . . . . 6
β’ ((π β β0
β§ π β β)
β (((π + π) β 1) + 1) = (π + π)) |
51 | 50 | eqcomd 2743 |
. . . . 5
β’ ((π β β0
β§ π β β)
β (π + π) = (((π + π) β 1) + 1)) |
52 | 51 | fveq2d 6851 |
. . . 4
β’ ((π β β0
β§ π β β)
β (FermatNoβ(π +
π)) =
(FermatNoβ(((π +
π) β 1) +
1))) |
53 | | fmtnorec2 45809 |
. . . . 5
β’ (((π + π) β 1) β β0
β (FermatNoβ(((π
+ π) β 1) + 1)) =
(βπ β
(0...((π + π) β
1))(FermatNoβπ) +
2)) |
54 | 4, 53 | syl 17 |
. . . 4
β’ ((π β β0
β§ π β β)
β (FermatNoβ(((π
+ π) β 1) + 1)) =
(βπ β
(0...((π + π) β
1))(FermatNoβπ) +
2)) |
55 | 52, 54 | eqtrd 2777 |
. . 3
β’ ((π β β0
β§ π β β)
β (FermatNoβ(π +
π)) = (βπ β (0...((π + π) β 1))(FermatNoβπ) + 2)) |
56 | 43, 44, 55 | mvrraddd 11574 |
. 2
β’ ((π β β0
β§ π β β)
β ((FermatNoβ(π
+ π)) β 2) =
βπ β
(0...((π + π) β
1))(FermatNoβπ)) |
57 | 37, 56 | breqtrrd 5138 |
1
β’ ((π β β0
β§ π β β)
β (FermatNoβπ)
β₯ ((FermatNoβ(π
+ π)) β
2)) |