Proof of Theorem 3exp7
| Step | Hyp | Ref
| Expression |
| 1 | | 3nn0 12544 |
. 2
⊢ 3 ∈
ℕ0 |
| 2 | | 6nn0 12547 |
. 2
⊢ 6 ∈
ℕ0 |
| 3 | | 6p1e7 12414 |
. 2
⊢ (6 + 1) =
7 |
| 4 | | 7nn0 12548 |
. . . 4
⊢ 7 ∈
ℕ0 |
| 5 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 6 | 4, 5 | deccl 12748 |
. . 3
⊢ ;72 ∈
ℕ0 |
| 7 | | 9nn0 12550 |
. . 3
⊢ 9 ∈
ℕ0 |
| 8 | | 3cn 12347 |
. . . . 5
⊢ 3 ∈
ℂ |
| 9 | | 2cn 12341 |
. . . . 5
⊢ 2 ∈
ℂ |
| 10 | | 3t2e6 12432 |
. . . . 5
⊢ (3
· 2) = 6 |
| 11 | 8, 9, 10 | mulcomli 11270 |
. . . 4
⊢ (2
· 3) = 6 |
| 12 | | 3exp3 17129 |
. . . 4
⊢
(3↑3) = ;27 |
| 13 | 5, 4 | deccl 12748 |
. . . . 5
⊢ ;27 ∈
ℕ0 |
| 14 | | eqid 2737 |
. . . . 5
⊢ ;27 = ;27 |
| 15 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 16 | | 8nn0 12549 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
| 17 | 15, 16 | deccl 12748 |
. . . . 5
⊢ ;18 ∈
ℕ0 |
| 18 | | 0nn0 12541 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
| 19 | 5 | dec0h 12755 |
. . . . . 6
⊢ 2 = ;02 |
| 20 | | eqid 2737 |
. . . . . 6
⊢ ;18 = ;18 |
| 21 | 13 | nn0cni 12538 |
. . . . . . . . 9
⊢ ;27 ∈ ℂ |
| 22 | 21 | mul02i 11450 |
. . . . . . . 8
⊢ (0
· ;27) = 0 |
| 23 | | 6cn 12357 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
| 24 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 25 | 23, 24, 3 | addcomli 11453 |
. . . . . . . 8
⊢ (1 + 6) =
7 |
| 26 | 22, 25 | oveq12i 7443 |
. . . . . . 7
⊢ ((0
· ;27) + (1 + 6)) = (0 +
7) |
| 27 | | 7cn 12360 |
. . . . . . . 8
⊢ 7 ∈
ℂ |
| 28 | 27 | addlidi 11449 |
. . . . . . 7
⊢ (0 + 7) =
7 |
| 29 | 26, 28 | eqtri 2765 |
. . . . . 6
⊢ ((0
· ;27) + (1 + 6)) =
7 |
| 30 | 16 | dec0h 12755 |
. . . . . . 7
⊢ 8 = ;08 |
| 31 | | 2t2e4 12430 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
| 32 | 9 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 2) =
2 |
| 33 | 31, 32 | oveq12i 7443 |
. . . . . . . 8
⊢ ((2
· 2) + (0 + 2)) = (4 + 2) |
| 34 | | 4p2e6 12419 |
. . . . . . . 8
⊢ (4 + 2) =
6 |
| 35 | 33, 34 | eqtri 2765 |
. . . . . . 7
⊢ ((2
· 2) + (0 + 2)) = 6 |
| 36 | | 4nn0 12545 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
| 37 | | 7t2e14 12842 |
. . . . . . . . 9
⊢ (7
· 2) = ;14 |
| 38 | 27, 9, 37 | mulcomli 11270 |
. . . . . . . 8
⊢ (2
· 7) = ;14 |
| 39 | | 1p1e2 12391 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
| 40 | | 8cn 12363 |
. . . . . . . . 9
⊢ 8 ∈
ℂ |
| 41 | | 4cn 12351 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
| 42 | | 8p4e12 12815 |
. . . . . . . . 9
⊢ (8 + 4) =
;12 |
| 43 | 40, 41, 42 | addcomli 11453 |
. . . . . . . 8
⊢ (4 + 8) =
;12 |
| 44 | 15, 36, 16, 38, 39, 5, 43 | decaddci 12794 |
. . . . . . 7
⊢ ((2
· 7) + 8) = ;22 |
| 45 | 5, 4, 18, 16, 14, 30, 5, 5, 5,
35, 44 | decma2c 12786 |
. . . . . 6
⊢ ((2
· ;27) + 8) = ;62 |
| 46 | 18, 5, 15, 16, 19, 20, 13, 5, 2, 29, 45 | decmac 12785 |
. . . . 5
⊢ ((2
· ;27) + ;18) = ;72 |
| 47 | | 4p4e8 12421 |
. . . . . . 7
⊢ (4 + 4) =
8 |
| 48 | 15, 36, 36, 37, 47 | decaddi 12793 |
. . . . . 6
⊢ ((7
· 2) + 4) = ;18 |
| 49 | | 7t7e49 12847 |
. . . . . 6
⊢ (7
· 7) = ;49 |
| 50 | 4, 5, 4, 14, 7, 36, 48, 49 | decmul2c 12799 |
. . . . 5
⊢ (7
· ;27) = ;;189 |
| 51 | 13, 5, 4, 14, 7, 17, 46, 50 | decmul1c 12798 |
. . . 4
⊢ (;27 · ;27) = ;;729 |
| 52 | 1, 1, 11, 12, 51 | numexp2x 17116 |
. . 3
⊢
(3↑6) = ;;729 |
| 53 | | eqid 2737 |
. . . 4
⊢ ;72 = ;72 |
| 54 | | 7t3e21 12843 |
. . . . 5
⊢ (7
· 3) = ;21 |
| 55 | | 1p0e1 12390 |
. . . . 5
⊢ (1 + 0) =
1 |
| 56 | 5, 15, 18, 54, 55 | decaddi 12793 |
. . . 4
⊢ ((7
· 3) + 0) = ;21 |
| 57 | 11 | oveq1i 7441 |
. . . . 5
⊢ ((2
· 3) + 2) = (6 + 2) |
| 58 | | 6p2e8 12425 |
. . . . 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 12784 |
. . 3
⊢ ((;72 · 3) + 2) = ;;218 |
| 61 | | 9t3e27 12856 |
. . 3
⊢ (9
· 3) = ;27 |
| 62 | 1, 6, 7, 52, 4, 5,
60, 61 | decmul1c 12798 |
. 2
⊢
((3↑6) · 3) = ;;;2187 |
| 63 | 1, 2, 3, 62 | numexpp1 17115 |
1
⊢
(3↑7) = ;;;2187 |