Proof of Theorem 3exp7
Step | Hyp | Ref
| Expression |
1 | | 3nn0 12431 |
. 2
⊢ 3 ∈
ℕ0 |
2 | | 6nn0 12434 |
. 2
⊢ 6 ∈
ℕ0 |
3 | | 6p1e7 12301 |
. 2
⊢ (6 + 1) =
7 |
4 | | 7nn0 12435 |
. . . 4
⊢ 7 ∈
ℕ0 |
5 | | 2nn0 12430 |
. . . 4
⊢ 2 ∈
ℕ0 |
6 | 4, 5 | deccl 12633 |
. . 3
⊢ ;72 ∈
ℕ0 |
7 | | 9nn0 12437 |
. . 3
⊢ 9 ∈
ℕ0 |
8 | | 3cn 12234 |
. . . . 5
⊢ 3 ∈
ℂ |
9 | | 2cn 12228 |
. . . . 5
⊢ 2 ∈
ℂ |
10 | | 3t2e6 12319 |
. . . . 5
⊢ (3
· 2) = 6 |
11 | 8, 9, 10 | mulcomli 11164 |
. . . 4
⊢ (2
· 3) = 6 |
12 | | 3exp3 16964 |
. . . 4
⊢
(3↑3) = ;27 |
13 | 5, 4 | deccl 12633 |
. . . . 5
⊢ ;27 ∈
ℕ0 |
14 | | eqid 2736 |
. . . . 5
⊢ ;27 = ;27 |
15 | | 1nn0 12429 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
16 | | 8nn0 12436 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
17 | 15, 16 | deccl 12633 |
. . . . 5
⊢ ;18 ∈
ℕ0 |
18 | | 0nn0 12428 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
19 | 5 | dec0h 12640 |
. . . . . 6
⊢ 2 = ;02 |
20 | | eqid 2736 |
. . . . . 6
⊢ ;18 = ;18 |
21 | 13 | nn0cni 12425 |
. . . . . . . . 9
⊢ ;27 ∈ ℂ |
22 | 21 | mul02i 11344 |
. . . . . . . 8
⊢ (0
· ;27) = 0 |
23 | | 6cn 12244 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
24 | | ax-1cn 11109 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
25 | 23, 24, 3 | addcomli 11347 |
. . . . . . . 8
⊢ (1 + 6) =
7 |
26 | 22, 25 | oveq12i 7369 |
. . . . . . 7
⊢ ((0
· ;27) + (1 + 6)) = (0 +
7) |
27 | | 7cn 12247 |
. . . . . . . 8
⊢ 7 ∈
ℂ |
28 | 27 | addid2i 11343 |
. . . . . . 7
⊢ (0 + 7) =
7 |
29 | 26, 28 | eqtri 2764 |
. . . . . 6
⊢ ((0
· ;27) + (1 + 6)) =
7 |
30 | 16 | dec0h 12640 |
. . . . . . 7
⊢ 8 = ;08 |
31 | | 2t2e4 12317 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
32 | 9 | addid2i 11343 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
33 | 31, 32 | oveq12i 7369 |
. . . . . . . 8
⊢ ((2
· 2) + (0 + 2)) = (4 + 2) |
34 | | 4p2e6 12306 |
. . . . . . . 8
⊢ (4 + 2) =
6 |
35 | 33, 34 | eqtri 2764 |
. . . . . . 7
⊢ ((2
· 2) + (0 + 2)) = 6 |
36 | | 4nn0 12432 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
37 | | 7t2e14 12727 |
. . . . . . . . 9
⊢ (7
· 2) = ;14 |
38 | 27, 9, 37 | mulcomli 11164 |
. . . . . . . 8
⊢ (2
· 7) = ;14 |
39 | | 1p1e2 12278 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
40 | | 8cn 12250 |
. . . . . . . . 9
⊢ 8 ∈
ℂ |
41 | | 4cn 12238 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
42 | | 8p4e12 12700 |
. . . . . . . . 9
⊢ (8 + 4) =
;12 |
43 | 40, 41, 42 | addcomli 11347 |
. . . . . . . 8
⊢ (4 + 8) =
;12 |
44 | 15, 36, 16, 38, 39, 5, 43 | decaddci 12679 |
. . . . . . 7
⊢ ((2
· 7) + 8) = ;22 |
45 | 5, 4, 18, 16, 14, 30, 5, 5, 5,
35, 44 | decma2c 12671 |
. . . . . 6
⊢ ((2
· ;27) + 8) = ;62 |
46 | 18, 5, 15, 16, 19, 20, 13, 5, 2, 29, 45 | decmac 12670 |
. . . . 5
⊢ ((2
· ;27) + ;18) = ;72 |
47 | | 4p4e8 12308 |
. . . . . . 7
⊢ (4 + 4) =
8 |
48 | 15, 36, 36, 37, 47 | decaddi 12678 |
. . . . . 6
⊢ ((7
· 2) + 4) = ;18 |
49 | | 7t7e49 12732 |
. . . . . 6
⊢ (7
· 7) = ;49 |
50 | 4, 5, 4, 14, 7, 36, 48, 49 | decmul2c 12684 |
. . . . 5
⊢ (7
· ;27) = ;;189 |
51 | 13, 5, 4, 14, 7, 17, 46, 50 | decmul1c 12683 |
. . . 4
⊢ (;27 · ;27) = ;;729 |
52 | 1, 1, 11, 12, 51 | numexp2x 16951 |
. . 3
⊢
(3↑6) = ;;729 |
53 | | eqid 2736 |
. . . 4
⊢ ;72 = ;72 |
54 | | 7t3e21 12728 |
. . . . 5
⊢ (7
· 3) = ;21 |
55 | | 1p0e1 12277 |
. . . . 5
⊢ (1 + 0) =
1 |
56 | 5, 15, 18, 54, 55 | decaddi 12678 |
. . . 4
⊢ ((7
· 3) + 0) = ;21 |
57 | 11 | oveq1i 7367 |
. . . . 5
⊢ ((2
· 3) + 2) = (6 + 2) |
58 | | 6p2e8 12312 |
. . . . 5
⊢ (6 + 2) =
8 |
59 | 57, 58 | eqtri 2764 |
. . . 4
⊢ ((2
· 3) + 2) = 8 |
60 | 4, 5, 18, 5, 53, 19, 1, 56, 59 | decma 12669 |
. . 3
⊢ ((;72 · 3) + 2) = ;;218 |
61 | | 9t3e27 12741 |
. . 3
⊢ (9
· 3) = ;27 |
62 | 1, 6, 7, 52, 4, 5,
60, 61 | decmul1c 12683 |
. 2
⊢
((3↑6) · 3) = ;;;2187 |
63 | 1, 2, 3, 62 | numexpp1 16950 |
1
⊢
(3↑7) = ;;;2187 |