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