Metamath Proof Explorer

Theorem 3exp7

Description: 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024)

Ref Expression
Assertion 3exp7 ( 3 ↑ 7 ) = 2 1 8 7

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 6nn0 ⊢ 6 ∈ ℕ0
3 6p1e7 ⊢ ( 6 + 1 ) = 7
4 7nn0 ⊢ 7 ∈ ℕ0
5 2nn0 ⊢ 2 ∈ ℕ0
6 4 5 deccl ⊢ 7 2 ∈ ℕ0
7 9nn0 ⊢ 9 ∈ ℕ0
8 2t3e6 ⊢ ( 2 · 3 ) = 6
9 3exp3 ⊢ ( 3 ↑ 3 ) = 2 7
10 5 4 deccl ⊢ 2 7 ∈ ℕ0
11 eqid ⊢ 2 7 = 2 7
12 1nn0 ⊢ 1 ∈ ℕ0
13 8nn0 ⊢ 8 ∈ ℕ0
14 12 13 deccl ⊢ 1 8 ∈ ℕ0
15 0nn0 ⊢ 0 ∈ ℕ0
16 5 dec0h ⊢ 2 = 0 2
17 eqid ⊢ 1 8 = 1 8
18 10 nn0cni ⊢ 2 7 ∈ ℂ
19 18 mul02i ⊢ ( 0 · 2 7 ) = 0
20 6cn ⊢ 6 ∈ ℂ
21 ax-1cn ⊢ 1 ∈ ℂ
22 20 21 3 addcomli ⊢ ( 1 + 6 ) = 7
23 19 22 oveq12i ⊢ ( ( 0 · 2 7 ) + ( 1 + 6 ) ) = ( 0 + 7 )
24 7cn ⊢ 7 ∈ ℂ
25 24 addlidi ⊢ ( 0 + 7 ) = 7
26 23 25 eqtri ⊢ ( ( 0 · 2 7 ) + ( 1 + 6 ) ) = 7
27 13 dec0h ⊢ 8 = 0 8
28 2t2e4 ⊢ ( 2 · 2 ) = 4
29 2cn ⊢ 2 ∈ ℂ
30 29 addlidi ⊢ ( 0 + 2 ) = 2
31 28 30 oveq12i ⊢ ( ( 2 · 2 ) + ( 0 + 2 ) ) = ( 4 + 2 )
32 4p2e6 ⊢ ( 4 + 2 ) = 6
33 31 32 eqtri ⊢ ( ( 2 · 2 ) + ( 0 + 2 ) ) = 6
34 4nn0 ⊢ 4 ∈ ℕ0
35 7t2e14 ⊢ ( 7 · 2 ) = 1 4
36 24 29 35 mulcomli ⊢ ( 2 · 7 ) = 1 4
37 1p1e2 ⊢ ( 1 + 1 ) = 2
38 8cn ⊢ 8 ∈ ℂ
39 4cn ⊢ 4 ∈ ℂ
40 8p4e12 ⊢ ( 8 + 4 ) = 1 2
41 38 39 40 addcomli ⊢ ( 4 + 8 ) = 1 2
42 12 34 13 36 37 5 41 decaddci ⊢ ( ( 2 · 7 ) + 8 ) = 2 2
43 5 4 15 13 11 27 5 5 5 33 42 decma2c ⊢ ( ( 2 · 2 7 ) + 8 ) = 6 2
44 15 5 12 13 16 17 10 5 2 26 43 decmac ⊢ ( ( 2 · 2 7 ) + 1 8 ) = 7 2
45 4p4e8 ⊢ ( 4 + 4 ) = 8
46 12 34 34 35 45 decaddi ⊢ ( ( 7 · 2 ) + 4 ) = 1 8
47 7t7e49 ⊢ ( 7 · 7 ) = 4 9
48 4 5 4 11 7 34 46 47 decmul2c ⊢ ( 7 · 2 7 ) = 1 8 9
49 10 5 4 11 7 14 44 48 decmul1c ⊢ ( 2 7 · 2 7 ) = 7 2 9
50 1 1 8 9 49 numexp2x ⊢ ( 3 ↑ 6 ) = 7 2 9
51 eqid ⊢ 7 2 = 7 2
52 7t3e21 ⊢ ( 7 · 3 ) = 2 1
53 1p0e1 ⊢ ( 1 + 0 ) = 1
54 5 12 15 52 53 decaddi ⊢ ( ( 7 · 3 ) + 0 ) = 2 1
55 8 oveq1i ⊢ ( ( 2 · 3 ) + 2 ) = ( 6 + 2 )
56 6p2e8 ⊢ ( 6 + 2 ) = 8
57 55 56 eqtri ⊢ ( ( 2 · 3 ) + 2 ) = 8
58 4 5 15 5 51 16 1 54 57 decma ⊢ ( ( 7 2 · 3 ) + 2 ) = 2 1 8
59 9t3e27 ⊢ ( 9 · 3 ) = 2 7
60 1 6 7 50 4 5 58 59 decmul1c ⊢ ( ( 3 ↑ 6 ) · 3 ) = 2 1 8 7
61 1 2 3 60 numexpp1 ⊢ ( 3 ↑ 7 ) = 2 1 8 7