Theorem 3exp7

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

	Ref	Expression
Assertion	3exp7	$$⊢3^7=2187$$

Proof

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