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