Proof of Theorem fmtno5faclem2
Step | Hyp | Ref
| Expression |
1 | | 6nn0 11190 |
. 2
⊢ 6 ∈
ℕ0 |
2 | | 7nn0 11191 |
. . . . . . 7
⊢ 7 ∈
ℕ0 |
3 | 1, 2 | deccl 11388 |
. . . . . 6
⊢ ;67 ∈
ℕ0 |
4 | | 0nn0 11184 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
5 | 3, 4 | deccl 11388 |
. . . . 5
⊢ ;;670 ∈ ℕ0 |
6 | 5, 4 | deccl 11388 |
. . . 4
⊢ ;;;6700
∈ ℕ0 |
7 | | 4nn0 11188 |
. . . 4
⊢ 4 ∈
ℕ0 |
8 | 6, 7 | deccl 11388 |
. . 3
⊢ ;;;;67004 ∈
ℕ0 |
9 | | 1nn0 11185 |
. . 3
⊢ 1 ∈
ℕ0 |
10 | 8, 9 | deccl 11388 |
. 2
⊢ ;;;;;670041 ∈ ℕ0 |
11 | | eqid 2610 |
. 2
⊢ ;;;;;;6700417 = ;;;;;;6700417 |
12 | | 2nn0 11186 |
. 2
⊢ 2 ∈
ℕ0 |
13 | 7, 4 | deccl 11388 |
. . . . . . 7
⊢ ;40 ∈
ℕ0 |
14 | 13, 12 | deccl 11388 |
. . . . . 6
⊢ ;;402 ∈ ℕ0 |
15 | 14, 4 | deccl 11388 |
. . . . 5
⊢ ;;;4020
∈ ℕ0 |
16 | 15, 12 | deccl 11388 |
. . . 4
⊢ ;;;;40202 ∈
ℕ0 |
17 | 16, 7 | deccl 11388 |
. . 3
⊢ ;;;;;402024 ∈ ℕ0 |
18 | | eqid 2610 |
. . . 4
⊢ ;;;;;670041 = ;;;;;670041 |
19 | | eqid 2610 |
. . . . 5
⊢ ;;;;67004 = ;;;;67004 |
20 | | eqid 2610 |
. . . . . . 7
⊢ ;;;6700 =
;;;6700 |
21 | | eqid 2610 |
. . . . . . . 8
⊢ ;;670 = ;;670 |
22 | | eqid 2610 |
. . . . . . . . 9
⊢ ;67 = ;67 |
23 | | 3nn0 11187 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
24 | | 6t6e36 11522 |
. . . . . . . . . 10
⊢ (6
· 6) = ;36 |
25 | | 3p1e4 11030 |
. . . . . . . . . 10
⊢ (3 + 1) =
4 |
26 | | 6p4e10 11474 |
. . . . . . . . . 10
⊢ (6 + 4) =
;10 |
27 | 23, 1, 7, 24, 25, 26 | decaddci2 11457 |
. . . . . . . . 9
⊢ ((6
· 6) + 4) = ;40 |
28 | | 7t6e42 11528 |
. . . . . . . . 9
⊢ (7
· 6) = ;42 |
29 | 1, 1, 2, 22, 12, 7, 27, 28 | decmul1c 11463 |
. . . . . . . 8
⊢ (;67 · 6) = ;;402 |
30 | | 6cn 10979 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
31 | 30 | mul02i 10104 |
. . . . . . . 8
⊢ (0
· 6) = 0 |
32 | 1, 3, 4, 21, 4, 29, 31 | decmul1 11461 |
. . . . . . 7
⊢ (;;670 · 6) = ;;;4020 |
33 | 1, 5, 4, 20, 4, 32, 31 | decmul1 11461 |
. . . . . 6
⊢ (;;;6700
· 6) = ;;;;40200 |
34 | | 2cn 10968 |
. . . . . . 7
⊢ 2 ∈
ℂ |
35 | 34 | addid2i 10103 |
. . . . . 6
⊢ (0 + 2) =
2 |
36 | 15, 4, 12, 33, 35 | decaddi 11455 |
. . . . 5
⊢ ((;;;6700
· 6) + 2) = ;;;;40202 |
37 | | 4cn 10975 |
. . . . . 6
⊢ 4 ∈
ℂ |
38 | | 6t4e24 11519 |
. . . . . 6
⊢ (6
· 4) = ;24 |
39 | 30, 37, 38 | mulcomli 9926 |
. . . . 5
⊢ (4
· 6) = ;24 |
40 | 1, 6, 7, 19, 7, 12, 36, 39 | decmul1c 11463 |
. . . 4
⊢ (;;;;67004 · 6) = ;;;;;402024 |
41 | 30 | mulid2i 9922 |
. . . 4
⊢ (1
· 6) = 6 |
42 | 1, 8, 9, 18, 1, 40, 41 | decmul1 11461 |
. . 3
⊢ (;;;;;670041 · 6) = ;;;;;;4020246 |
43 | | eqid 2610 |
. . . 4
⊢ ;;;;;402024 = ;;;;;402024 |
44 | | 4p1e5 11031 |
. . . 4
⊢ (4 + 1) =
5 |
45 | 16, 7, 9, 43, 44 | decaddi 11455 |
. . 3
⊢ (;;;;;402024 + 1) = ;;;;;402025 |
46 | 17, 1, 7, 42, 45, 26 | decaddci2 11457 |
. 2
⊢ ((;;;;;670041 · 6) + 4) = ;;;;;;4020250 |
47 | 1, 10, 2, 11, 12, 7, 46, 28 | decmul1c 11463 |
1
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 |