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