Proof of Theorem fmtno5faclem3
| Step | Hyp | Ref
| Expression |
| 1 | | 4nn0 12545 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
| 2 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 3 | 1, 2 | deccl 12748 |
. . . . . . . 8
⊢ ;40 ∈
ℕ0 |
| 4 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 5 | 3, 4 | deccl 12748 |
. . . . . . 7
⊢ ;;402 ∈ ℕ0 |
| 6 | 5, 2 | deccl 12748 |
. . . . . 6
⊢ ;;;4020
∈ ℕ0 |
| 7 | 6, 4 | deccl 12748 |
. . . . 5
⊢ ;;;;40202 ∈
ℕ0 |
| 8 | | 5nn0 12546 |
. . . . 5
⊢ 5 ∈
ℕ0 |
| 9 | 7, 8 | deccl 12748 |
. . . 4
⊢ ;;;;;402025 ∈ ℕ0 |
| 10 | 9, 2 | deccl 12748 |
. . 3
⊢ ;;;;;;4020250 ∈ ℕ0 |
| 11 | 10, 4 | deccl 12748 |
. 2
⊢ ;;;;;;;40202502 ∈
ℕ0 |
| 12 | | 6nn0 12547 |
. . . . . . . 8
⊢ 6 ∈
ℕ0 |
| 13 | 4, 12 | deccl 12748 |
. . . . . . 7
⊢ ;26 ∈
ℕ0 |
| 14 | | 8nn0 12549 |
. . . . . . 7
⊢ 8 ∈
ℕ0 |
| 15 | 13, 14 | deccl 12748 |
. . . . . 6
⊢ ;;268 ∈ ℕ0 |
| 16 | 15, 2 | deccl 12748 |
. . . . 5
⊢ ;;;2680
∈ ℕ0 |
| 17 | | 1nn0 12542 |
. . . . 5
⊢ 1 ∈
ℕ0 |
| 18 | 16, 17 | deccl 12748 |
. . . 4
⊢ ;;;;26801 ∈
ℕ0 |
| 19 | 18, 12 | deccl 12748 |
. . 3
⊢ ;;;;;268016 ∈ ℕ0 |
| 20 | 19, 12 | deccl 12748 |
. 2
⊢ ;;;;;;2680166 ∈ ℕ0 |
| 21 | | eqid 2737 |
. 2
⊢ ;;;;;;;;402025020 = ;;;;;;;;402025020 |
| 22 | | eqid 2737 |
. 2
⊢ ;;;;;;;26801668 = ;;;;;;;26801668 |
| 23 | | eqid 2737 |
. . 3
⊢ ;;;;;;;40202502 = ;;;;;;;40202502 |
| 24 | | eqid 2737 |
. . 3
⊢ ;;;;;;2680166 = ;;;;;;2680166 |
| 25 | | eqid 2737 |
. . . 4
⊢ ;;;;;;4020250 = ;;;;;;4020250 |
| 26 | | eqid 2737 |
. . . 4
⊢ ;;;;;268016 = ;;;;;268016 |
| 27 | | eqid 2737 |
. . . . 5
⊢ ;;;;;402025 = ;;;;;402025 |
| 28 | | eqid 2737 |
. . . . 5
⊢ ;;;;26801 = ;;;;26801 |
| 29 | | eqid 2737 |
. . . . . 6
⊢ ;;;;40202 = ;;;;40202 |
| 30 | | eqid 2737 |
. . . . . 6
⊢ ;;;2680 =
;;;2680 |
| 31 | | eqid 2737 |
. . . . . . 7
⊢ ;;;4020 =
;;;4020 |
| 32 | | eqid 2737 |
. . . . . . 7
⊢ ;;268 = ;;268 |
| 33 | | eqid 2737 |
. . . . . . . 8
⊢ ;;402 = ;;402 |
| 34 | | eqid 2737 |
. . . . . . . 8
⊢ ;26 = ;26 |
| 35 | | eqid 2737 |
. . . . . . . . 9
⊢ ;40 = ;40 |
| 36 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 37 | 36 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
| 38 | 1, 2, 4, 35, 37 | decaddi 12793 |
. . . . . . . 8
⊢ (;40 + 2) = ;42 |
| 39 | | 6cn 12357 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
| 40 | | 6p2e8 12425 |
. . . . . . . . 9
⊢ (6 + 2) =
8 |
| 41 | 39, 36, 40 | addcomli 11453 |
. . . . . . . 8
⊢ (2 + 6) =
8 |
| 42 | 3, 4, 4, 12, 33, 34, 38, 41 | decadd 12787 |
. . . . . . 7
⊢ (;;402 + ;26) = ;;428 |
| 43 | | 8cn 12363 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
| 44 | 43 | addlidi 11449 |
. . . . . . 7
⊢ (0 + 8) =
8 |
| 45 | 5, 2, 13, 14, 31, 32, 42, 44 | decadd 12787 |
. . . . . 6
⊢ (;;;4020 +
;;268) = ;;;4288 |
| 46 | 36 | addridi 11448 |
. . . . . 6
⊢ (2 + 0) =
2 |
| 47 | 6, 4, 15, 2, 29, 30, 45, 46 | decadd 12787 |
. . . . 5
⊢ (;;;;40202 + ;;;2680) = ;;;;42882 |
| 48 | | 5p1e6 12413 |
. . . . 5
⊢ (5 + 1) =
6 |
| 49 | 7, 8, 16, 17, 27, 28, 47, 48 | decadd 12787 |
. . . 4
⊢ (;;;;;402025 + ;;;;26801) = ;;;;;428826 |
| 50 | 39 | addlidi 11449 |
. . . 4
⊢ (0 + 6) =
6 |
| 51 | 9, 2, 18, 12, 25, 26, 49, 50 | decadd 12787 |
. . 3
⊢ (;;;;;;4020250 + ;;;;;268016) = ;;;;;;4288266 |
| 52 | 10, 4, 19, 12, 23, 24, 51, 41 | decadd 12787 |
. 2
⊢ (;;;;;;;40202502 + ;;;;;;2680166) = ;;;;;;;42882668 |
| 53 | 11, 2, 20, 14, 21, 22, 52, 44 | decadd 12787 |
1
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 |