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 |
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 |