Step | Hyp | Ref
| Expression |
1 | | 3nn0 12438 |
. 2
⊢ 3 ∈
ℕ0 |
2 | | 6nn0 12441 |
. 2
⊢ 6 ∈
ℕ0 |
3 | | 6p1e7 12308 |
. 2
⊢ (6 + 1) =
7 |
4 | | 7nn0 12442 |
. . . 4
⊢ 7 ∈
ℕ0 |
5 | | 2nn0 12437 |
. . . 4
⊢ 2 ∈
ℕ0 |
6 | 4, 5 | deccl 12640 |
. . 3
⊢ ;72 ∈
ℕ0 |
7 | | 9nn0 12444 |
. . 3
⊢ 9 ∈
ℕ0 |
8 | | 3cn 12241 |
. . . . 5
⊢ 3 ∈
ℂ |
9 | | 2cn 12235 |
. . . . 5
⊢ 2 ∈
ℂ |
10 | | 3t2e6 12326 |
. . . . 5
⊢ (3
· 2) = 6 |
11 | 8, 9, 10 | mulcomli 11171 |
. . . 4
⊢ (2
· 3) = 6 |
12 | | 3exp3 16971 |
. . . 4
⊢
(3↑3) = ;27 |
13 | 5, 4 | deccl 12640 |
. . . . 5
⊢ ;27 ∈
ℕ0 |
14 | | eqid 2737 |
. . . . 5
⊢ ;27 = ;27 |
15 | | 1nn0 12436 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
16 | | 8nn0 12443 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
17 | 15, 16 | deccl 12640 |
. . . . 5
⊢ ;18 ∈
ℕ0 |
18 | | 0nn0 12435 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
19 | 5 | dec0h 12647 |
. . . . . 6
⊢ 2 = ;02 |
20 | | eqid 2737 |
. . . . . 6
⊢ ;18 = ;18 |
21 | 13 | nn0cni 12432 |
. . . . . . . . 9
⊢ ;27 ∈ ℂ |
22 | 21 | mul02i 11351 |
. . . . . . . 8
⊢ (0
· ;27) = 0 |
23 | | 6cn 12251 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
24 | | ax-1cn 11116 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
25 | 23, 24, 3 | addcomli 11354 |
. . . . . . . 8
⊢ (1 + 6) =
7 |
26 | 22, 25 | oveq12i 7374 |
. . . . . . 7
⊢ ((0
· ;27) + (1 + 6)) = (0 +
7) |
27 | | 7cn 12254 |
. . . . . . . 8
⊢ 7 ∈
ℂ |
28 | 27 | addid2i 11350 |
. . . . . . 7
⊢ (0 + 7) =
7 |
29 | 26, 28 | eqtri 2765 |
. . . . . 6
⊢ ((0
· ;27) + (1 + 6)) =
7 |
30 | 16 | dec0h 12647 |
. . . . . . 7
⊢ 8 = ;08 |
31 | | 2t2e4 12324 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
32 | 9 | addid2i 11350 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
33 | 31, 32 | oveq12i 7374 |
. . . . . . . 8
⊢ ((2
· 2) + (0 + 2)) = (4 + 2) |
34 | | 4p2e6 12313 |
. . . . . . . 8
⊢ (4 + 2) =
6 |
35 | 33, 34 | eqtri 2765 |
. . . . . . 7
⊢ ((2
· 2) + (0 + 2)) = 6 |
36 | | 4nn0 12439 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
37 | | 7t2e14 12734 |
. . . . . . . . 9
⊢ (7
· 2) = ;14 |
38 | 27, 9, 37 | mulcomli 11171 |
. . . . . . . 8
⊢ (2
· 7) = ;14 |
39 | | 1p1e2 12285 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
40 | | 8cn 12257 |
. . . . . . . . 9
⊢ 8 ∈
ℂ |
41 | | 4cn 12245 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
42 | | 8p4e12 12707 |
. . . . . . . . 9
⊢ (8 + 4) =
;12 |
43 | 40, 41, 42 | addcomli 11354 |
. . . . . . . 8
⊢ (4 + 8) =
;12 |
44 | 15, 36, 16, 38, 39, 5, 43 | decaddci 12686 |
. . . . . . 7
⊢ ((2
· 7) + 8) = ;22 |
45 | 5, 4, 18, 16, 14, 30, 5, 5, 5,
35, 44 | decma2c 12678 |
. . . . . 6
⊢ ((2
· ;27) + 8) = ;62 |
46 | 18, 5, 15, 16, 19, 20, 13, 5, 2, 29, 45 | decmac 12677 |
. . . . 5
⊢ ((2
· ;27) + ;18) = ;72 |
47 | | 4p4e8 12315 |
. . . . . . 7
⊢ (4 + 4) =
8 |
48 | 15, 36, 36, 37, 47 | decaddi 12685 |
. . . . . 6
⊢ ((7
· 2) + 4) = ;18 |
49 | | 7t7e49 12739 |
. . . . . 6
⊢ (7
· 7) = ;49 |
50 | 4, 5, 4, 14, 7, 36, 48, 49 | decmul2c 12691 |
. . . . 5
⊢ (7
· ;27) = ;;189 |
51 | 13, 5, 4, 14, 7, 17, 46, 50 | decmul1c 12690 |
. . . 4
⊢ (;27 · ;27) = ;;729 |
52 | 1, 1, 11, 12, 51 | numexp2x 16958 |
. . 3
⊢
(3↑6) = ;;729 |
53 | | eqid 2737 |
. . . 4
⊢ ;72 = ;72 |
54 | | 7t3e21 12735 |
. . . . 5
⊢ (7
· 3) = ;21 |
55 | | 1p0e1 12284 |
. . . . 5
⊢ (1 + 0) =
1 |
56 | 5, 15, 18, 54, 55 | decaddi 12685 |
. . . 4
⊢ ((7
· 3) + 0) = ;21 |
57 | 11 | oveq1i 7372 |
. . . . 5
⊢ ((2
· 3) + 2) = (6 + 2) |
58 | | 6p2e8 12319 |
. . . . 5
⊢ (6 + 2) =
8 |
59 | 57, 58 | eqtri 2765 |
. . . 4
⊢ ((2
· 3) + 2) = 8 |
60 | 4, 5, 18, 5, 53, 19, 1, 56, 59 | decma 12676 |
. . 3
⊢ ((;72 · 3) + 2) = ;;218 |
61 | | 9t3e27 12748 |
. . 3
⊢ (9
· 3) = ;27 |
62 | 1, 6, 7, 52, 4, 5,
60, 61 | decmul1c 12690 |
. 2
⊢
((3↑6) · 3) = ;;;2187 |
63 | 1, 2, 3, 62 | numexpp1 16957 |
1
⊢
(3↑7) = ;;;2187 |