Proof of Theorem fmtno5fac
Step | Hyp | Ref
| Expression |
1 | | 4nn0 12252 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
2 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
3 | 1, 2 | deccl 12452 |
. . . . . . . . . 10
⊢ ;42 ∈
ℕ0 |
4 | | 8nn0 12256 |
. . . . . . . . . 10
⊢ 8 ∈
ℕ0 |
5 | 3, 4 | deccl 12452 |
. . . . . . . . 9
⊢ ;;428 ∈ ℕ0 |
6 | 5, 4 | deccl 12452 |
. . . . . . . 8
⊢ ;;;4288
∈ ℕ0 |
7 | 6, 2 | deccl 12452 |
. . . . . . 7
⊢ ;;;;42882 ∈
ℕ0 |
8 | | 6nn0 12254 |
. . . . . . 7
⊢ 6 ∈
ℕ0 |
9 | 7, 8 | deccl 12452 |
. . . . . 6
⊢ ;;;;;428826 ∈ ℕ0 |
10 | 9, 8 | deccl 12452 |
. . . . 5
⊢ ;;;;;;4288266 ∈ ℕ0 |
11 | 10, 4 | deccl 12452 |
. . . 4
⊢ ;;;;;;;42882668 ∈
ℕ0 |
12 | 11, 4 | deccl 12452 |
. . 3
⊢ ;;;;;;;;428826688 ∈
ℕ0 |
13 | | 0nn0 12248 |
. . 3
⊢ 0 ∈
ℕ0 |
14 | | 7nn0 12255 |
. . . . . . . 8
⊢ 7 ∈
ℕ0 |
15 | 8, 14 | deccl 12452 |
. . . . . . 7
⊢ ;67 ∈
ℕ0 |
16 | 15, 13 | deccl 12452 |
. . . . . 6
⊢ ;;670 ∈ ℕ0 |
17 | 16, 13 | deccl 12452 |
. . . . 5
⊢ ;;;6700
∈ ℕ0 |
18 | 17, 1 | deccl 12452 |
. . . 4
⊢ ;;;;67004 ∈
ℕ0 |
19 | | 1nn0 12249 |
. . . 4
⊢ 1 ∈
ℕ0 |
20 | 18, 19 | deccl 12452 |
. . 3
⊢ ;;;;;670041 ∈ ℕ0 |
21 | | fmtno5faclem3 45033 |
. . . 4
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 |
22 | 21 | deceq1i 12444 |
. . 3
⊢ ;(;;;;;;;;402025020 + ;;;;;;;26801668)0 = ;;;;;;;;;4288266880 |
23 | | eqid 2738 |
. . 3
⊢ ;;;;;;6700417 = ;;;;;;6700417 |
24 | | eqid 2738 |
. . . 4
⊢ ;;;;;;;;428826688 = ;;;;;;;;428826688 |
25 | | eqid 2738 |
. . . 4
⊢ ;;;;;670041 = ;;;;;670041 |
26 | | eqid 2738 |
. . . . 5
⊢ ;;;;;;;42882668 = ;;;;;;;42882668 |
27 | | eqid 2738 |
. . . . 5
⊢ ;;;;67004 = ;;;;67004 |
28 | | 9nn0 12257 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ0 |
29 | 3, 28 | deccl 12452 |
. . . . . . . . 9
⊢ ;;429 ∈ ℕ0 |
30 | 29, 1 | deccl 12452 |
. . . . . . . 8
⊢ ;;;4294
∈ ℕ0 |
31 | 30, 28 | deccl 12452 |
. . . . . . 7
⊢ ;;;;42949 ∈
ℕ0 |
32 | 31, 8 | deccl 12452 |
. . . . . 6
⊢ ;;;;;429496 ∈ ℕ0 |
33 | | 6p1e7 12121 |
. . . . . 6
⊢ (6 + 1) =
7 |
34 | | eqid 2738 |
. . . . . . 7
⊢ ;;;;;;4288266 = ;;;;;;4288266 |
35 | | eqid 2738 |
. . . . . . 7
⊢ ;;;6700 =
;;;6700 |
36 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;;;428826 = ;;;;;428826 |
37 | | eqid 2738 |
. . . . . . . 8
⊢ ;;670 = ;;670 |
38 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;;42882 = ;;;;42882 |
39 | | eqid 2738 |
. . . . . . . . 9
⊢ ;67 = ;67 |
40 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;;;4288 =
;;;4288 |
41 | | 8p1e9 12123 |
. . . . . . . . . . 11
⊢ (8 + 1) =
9 |
42 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;;428 = ;;428 |
43 | 3, 4, 41, 42 | decsuc 12468 |
. . . . . . . . . 10
⊢ (;;428 + 1) = ;;429 |
44 | | 8p6e14 12521 |
. . . . . . . . . 10
⊢ (8 + 6) =
;14 |
45 | 5, 4, 8, 40, 43, 1, 44 | decaddci 12498 |
. . . . . . . . 9
⊢ (;;;4288 +
6) = ;;;4294 |
46 | | 7cn 12067 |
. . . . . . . . . 10
⊢ 7 ∈
ℂ |
47 | | 2cn 12048 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
48 | | 7p2e9 12134 |
. . . . . . . . . 10
⊢ (7 + 2) =
9 |
49 | 46, 47, 48 | addcomli 11167 |
. . . . . . . . 9
⊢ (2 + 7) =
9 |
50 | 6, 2, 8, 14, 38, 39, 45, 49 | decadd 12491 |
. . . . . . . 8
⊢ (;;;;42882 + ;67) = ;;;;42949 |
51 | | 6cn 12064 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
52 | 51 | addid1i 11162 |
. . . . . . . 8
⊢ (6 + 0) =
6 |
53 | 7, 8, 15, 13, 36, 37, 50, 52 | decadd 12491 |
. . . . . . 7
⊢ (;;;;;428826 + ;;670) =
;;;;;429496 |
54 | 9, 8, 16, 13, 34, 35, 53, 52 | decadd 12491 |
. . . . . 6
⊢ (;;;;;;4288266 + ;;;6700) = ;;;;;;4294966 |
55 | 32, 8, 33, 54 | decsuc 12468 |
. . . . 5
⊢ ((;;;;;;4288266 + ;;;6700) + 1) = ;;;;;;4294967 |
56 | | 8p4e12 12519 |
. . . . 5
⊢ (8 + 4) =
;12 |
57 | 10, 4, 17, 1, 26, 27, 55, 2, 56 | decaddc 12492 |
. . . 4
⊢ (;;;;;;;42882668 + ;;;;67004) = ;;;;;;;42949672 |
58 | 11, 4, 18, 19, 24, 25, 57, 41 | decadd 12491 |
. . 3
⊢ (;;;;;;;;428826688 + ;;;;;670041) = ;;;;;;;;429496729 |
59 | 46 | addid2i 11163 |
. . 3
⊢ (0 + 7) =
7 |
60 | 12, 13, 20, 14, 22, 23, 58, 59 | decadd 12491 |
. 2
⊢ (;(;;;;;;;;402025020 + ;;;;;;;26801668)0 + ;;;;;;6700417) = ;;;;;;;;;4294967297 |
61 | 8, 1 | deccl 12452 |
. . 3
⊢ ;64 ∈
ℕ0 |
62 | 20, 14 | deccl 12452 |
. . 3
⊢ ;;;;;;6700417 ∈ ℕ0 |
63 | | fmtno5faclem2 45032 |
. . . . . 6
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 |
64 | 63 | eqcomi 2747 |
. . . . 5
⊢ ;;;;;;;40202502 = (;;;;;;6700417 · 6) |
65 | | fmtno5faclem1 45031 |
. . . . . 6
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 |
66 | 65 | eqcomi 2747 |
. . . . 5
⊢ ;;;;;;;26801668 = (;;;;;;6700417 · 4) |
67 | 8, 1, 62, 64, 66 | decmul10add 12506 |
. . . 4
⊢ (;;;;;;6700417 · ;64) = (;;;;;;;;402025020 + ;;;;;;;26801668) |
68 | 67 | eqcomi 2747 |
. . 3
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = (;;;;;;6700417 · ;64) |
69 | 62 | nn0cni 12245 |
. . . . 5
⊢ ;;;;;;6700417 ∈ ℂ |
70 | 69 | mulid1i 10979 |
. . . 4
⊢ (;;;;;;6700417 · 1) = ;;;;;;6700417 |
71 | 70 | eqcomi 2747 |
. . 3
⊢ ;;;;;;6700417 = (;;;;;;6700417 · 1) |
72 | 61, 19, 62, 68, 71 | decmul10add 12506 |
. 2
⊢ (;;;;;;6700417 · ;;641) =
(;(;;;;;;;;402025020 + ;;;;;;;26801668)0 + ;;;;;;6700417) |
73 | | fmtno5 45009 |
. 2
⊢
(FermatNo‘5) = ;;;;;;;;;4294967297 |
74 | 60, 72, 73 | 3eqtr4ri 2777 |
1
⊢
(FermatNo‘5) = (;;;;;;6700417 · ;;641) |