Proof of Theorem fmtno5fac
| Step | Hyp | Ref
| Expression |
| 1 | | 4nn0 12545 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
| 2 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . . . . . . . . 10
⊢ ;42 ∈
ℕ0 |
| 4 | | 8nn0 12549 |
. . . . . . . . . 10
⊢ 8 ∈
ℕ0 |
| 5 | 3, 4 | deccl 12748 |
. . . . . . . . 9
⊢ ;;428 ∈ ℕ0 |
| 6 | 5, 4 | deccl 12748 |
. . . . . . . 8
⊢ ;;;4288
∈ ℕ0 |
| 7 | 6, 2 | deccl 12748 |
. . . . . . 7
⊢ ;;;;42882 ∈
ℕ0 |
| 8 | | 6nn0 12547 |
. . . . . . 7
⊢ 6 ∈
ℕ0 |
| 9 | 7, 8 | deccl 12748 |
. . . . . 6
⊢ ;;;;;428826 ∈ ℕ0 |
| 10 | 9, 8 | deccl 12748 |
. . . . 5
⊢ ;;;;;;4288266 ∈ ℕ0 |
| 11 | 10, 4 | deccl 12748 |
. . . 4
⊢ ;;;;;;;42882668 ∈
ℕ0 |
| 12 | 11, 4 | deccl 12748 |
. . 3
⊢ ;;;;;;;;428826688 ∈
ℕ0 |
| 13 | | 0nn0 12541 |
. . 3
⊢ 0 ∈
ℕ0 |
| 14 | | 7nn0 12548 |
. . . . . . . 8
⊢ 7 ∈
ℕ0 |
| 15 | 8, 14 | deccl 12748 |
. . . . . . 7
⊢ ;67 ∈
ℕ0 |
| 16 | 15, 13 | deccl 12748 |
. . . . . 6
⊢ ;;670 ∈ ℕ0 |
| 17 | 16, 13 | deccl 12748 |
. . . . 5
⊢ ;;;6700
∈ ℕ0 |
| 18 | 17, 1 | deccl 12748 |
. . . 4
⊢ ;;;;67004 ∈
ℕ0 |
| 19 | | 1nn0 12542 |
. . . 4
⊢ 1 ∈
ℕ0 |
| 20 | 18, 19 | deccl 12748 |
. . 3
⊢ ;;;;;670041 ∈ ℕ0 |
| 21 | | fmtno5faclem3 47568 |
. . . 4
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 |
| 22 | 21 | deceq1i 12740 |
. . 3
⊢ ;(;;;;;;;;402025020 + ;;;;;;;26801668)0 = ;;;;;;;;;4288266880 |
| 23 | | eqid 2737 |
. . 3
⊢ ;;;;;;6700417 = ;;;;;;6700417 |
| 24 | | eqid 2737 |
. . . 4
⊢ ;;;;;;;;428826688 = ;;;;;;;;428826688 |
| 25 | | eqid 2737 |
. . . 4
⊢ ;;;;;670041 = ;;;;;670041 |
| 26 | | eqid 2737 |
. . . . 5
⊢ ;;;;;;;42882668 = ;;;;;;;42882668 |
| 27 | | eqid 2737 |
. . . . 5
⊢ ;;;;67004 = ;;;;67004 |
| 28 | | 9nn0 12550 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ0 |
| 29 | 3, 28 | deccl 12748 |
. . . . . . . . 9
⊢ ;;429 ∈ ℕ0 |
| 30 | 29, 1 | deccl 12748 |
. . . . . . . 8
⊢ ;;;4294
∈ ℕ0 |
| 31 | 30, 28 | deccl 12748 |
. . . . . . 7
⊢ ;;;;42949 ∈
ℕ0 |
| 32 | 31, 8 | deccl 12748 |
. . . . . 6
⊢ ;;;;;429496 ∈ ℕ0 |
| 33 | | 6p1e7 12414 |
. . . . . 6
⊢ (6 + 1) =
7 |
| 34 | | eqid 2737 |
. . . . . . 7
⊢ ;;;;;;4288266 = ;;;;;;4288266 |
| 35 | | eqid 2737 |
. . . . . . 7
⊢ ;;;6700 =
;;;6700 |
| 36 | | eqid 2737 |
. . . . . . . 8
⊢ ;;;;;428826 = ;;;;;428826 |
| 37 | | eqid 2737 |
. . . . . . . 8
⊢ ;;670 = ;;670 |
| 38 | | eqid 2737 |
. . . . . . . . 9
⊢ ;;;;42882 = ;;;;42882 |
| 39 | | eqid 2737 |
. . . . . . . . 9
⊢ ;67 = ;67 |
| 40 | | eqid 2737 |
. . . . . . . . . 10
⊢ ;;;4288 =
;;;4288 |
| 41 | | 8p1e9 12416 |
. . . . . . . . . . 11
⊢ (8 + 1) =
9 |
| 42 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;;428 = ;;428 |
| 43 | 3, 4, 41, 42 | decsuc 12764 |
. . . . . . . . . 10
⊢ (;;428 + 1) = ;;429 |
| 44 | | 8p6e14 12817 |
. . . . . . . . . 10
⊢ (8 + 6) =
;14 |
| 45 | 5, 4, 8, 40, 43, 1, 44 | decaddci 12794 |
. . . . . . . . 9
⊢ (;;;4288 +
6) = ;;;4294 |
| 46 | | 7cn 12360 |
. . . . . . . . . 10
⊢ 7 ∈
ℂ |
| 47 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 48 | | 7p2e9 12427 |
. . . . . . . . . 10
⊢ (7 + 2) =
9 |
| 49 | 46, 47, 48 | addcomli 11453 |
. . . . . . . . 9
⊢ (2 + 7) =
9 |
| 50 | 6, 2, 8, 14, 38, 39, 45, 49 | decadd 12787 |
. . . . . . . 8
⊢ (;;;;42882 + ;67) = ;;;;42949 |
| 51 | | 6cn 12357 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
| 52 | 51 | addridi 11448 |
. . . . . . . 8
⊢ (6 + 0) =
6 |
| 53 | 7, 8, 15, 13, 36, 37, 50, 52 | decadd 12787 |
. . . . . . 7
⊢ (;;;;;428826 + ;;670) =
;;;;;429496 |
| 54 | 9, 8, 16, 13, 34, 35, 53, 52 | decadd 12787 |
. . . . . 6
⊢ (;;;;;;4288266 + ;;;6700) = ;;;;;;4294966 |
| 55 | 32, 8, 33, 54 | decsuc 12764 |
. . . . 5
⊢ ((;;;;;;4288266 + ;;;6700) + 1) = ;;;;;;4294967 |
| 56 | | 8p4e12 12815 |
. . . . 5
⊢ (8 + 4) =
;12 |
| 57 | 10, 4, 17, 1, 26, 27, 55, 2, 56 | decaddc 12788 |
. . . 4
⊢ (;;;;;;;42882668 + ;;;;67004) = ;;;;;;;42949672 |
| 58 | 11, 4, 18, 19, 24, 25, 57, 41 | decadd 12787 |
. . 3
⊢ (;;;;;;;;428826688 + ;;;;;670041) = ;;;;;;;;429496729 |
| 59 | 46 | addlidi 11449 |
. . 3
⊢ (0 + 7) =
7 |
| 60 | 12, 13, 20, 14, 22, 23, 58, 59 | decadd 12787 |
. 2
⊢ (;(;;;;;;;;402025020 + ;;;;;;;26801668)0 + ;;;;;;6700417) = ;;;;;;;;;4294967297 |
| 61 | 8, 1 | deccl 12748 |
. . 3
⊢ ;64 ∈
ℕ0 |
| 62 | 20, 14 | deccl 12748 |
. . 3
⊢ ;;;;;;6700417 ∈ ℕ0 |
| 63 | | fmtno5faclem2 47567 |
. . . . . 6
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 |
| 64 | 63 | eqcomi 2746 |
. . . . 5
⊢ ;;;;;;;40202502 = (;;;;;;6700417 · 6) |
| 65 | | fmtno5faclem1 47566 |
. . . . . 6
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 |
| 66 | 65 | eqcomi 2746 |
. . . . 5
⊢ ;;;;;;;26801668 = (;;;;;;6700417 · 4) |
| 67 | 8, 1, 62, 64, 66 | decmul10add 12802 |
. . . 4
⊢ (;;;;;;6700417 · ;64) = (;;;;;;;;402025020 + ;;;;;;;26801668) |
| 68 | 67 | eqcomi 2746 |
. . 3
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = (;;;;;;6700417 · ;64) |
| 69 | 62 | nn0cni 12538 |
. . . . 5
⊢ ;;;;;;6700417 ∈ ℂ |
| 70 | 69 | mulridi 11265 |
. . . 4
⊢ (;;;;;;6700417 · 1) = ;;;;;;6700417 |
| 71 | 70 | eqcomi 2746 |
. . 3
⊢ ;;;;;;6700417 = (;;;;;;6700417 · 1) |
| 72 | 61, 19, 62, 68, 71 | decmul10add 12802 |
. 2
⊢ (;;;;;;6700417 · ;;641) =
(;(;;;;;;;;402025020 + ;;;;;;;26801668)0 + ;;;;;;6700417) |
| 73 | | fmtno5 47544 |
. 2
⊢
(FermatNo‘5) = ;;;;;;;;;4294967297 |
| 74 | 60, 72, 73 | 3eqtr4ri 2776 |
1
⊢
(FermatNo‘5) = (;;;;;;6700417 · ;;641) |