Theorem 2exp11

Description: Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021)

	Ref	Expression
Assertion	2exp11	$$⊢2^{11}=2048$$

Proof

Step	Hyp	Ref	Expression
1		8p3e11	$$⊢8+3=11$$
2	1	eqcomi	$$⊢11=8+3$$
3	2	oveq2i	$$⊢2^{11}=2^{8+3}$$
4		2cn	$$⊢2\in ℂ$$
5		8nn0	$$⊢8\in {\mathbb{N}}_0$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7		expadd	$$⊢\left(2\in ℂ\wedge 8\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\to 2^{8+3}=2^8{2}^3$$
8	4 5 6 7	mp3an	$$⊢2^{8+3}=2^8{2}^3$$
9	3 8	eqtri	$$⊢2^{11}=2^8{2}^3$$
10		2exp8	$$⊢2^8=256$$
11		cu2	$$⊢2^3=8$$
12	10 11	oveq12i	$$⊢2^8{2}^3=256\cdot 8$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢25\in {\mathbb{N}}_0$$
16		6nn0	$$⊢6\in {\mathbb{N}}_0$$
17		eqid	$$⊢256=256$$
18		4nn0	$$⊢4\in {\mathbb{N}}_0$$
19		0nn0	$$⊢0\in {\mathbb{N}}_0$$
20	13 19	deccl	$$⊢20\in {\mathbb{N}}_0$$
21		eqid	$$⊢25=25$$
22		1nn0	$$⊢1\in {\mathbb{N}}_0$$
23		8cn	$$⊢8\in ℂ$$
24		8t2e16	$$⊢8\cdot 2=16$$
25	23 4 24	mulcomli	$$⊢2\cdot 8=16$$
26		1p1e2	$$⊢1+1=2$$
27		6p4e10	$$⊢6+4=10$$
28	22 16 18 25 26 19 27	decaddci	$$⊢2\cdot 8+4=20$$
29		5cn	$$⊢5\in ℂ$$
30		8t5e40	$$⊢8\cdot 5=40$$
31	23 29 30	mulcomli	$$⊢5\cdot 8=40$$
32	5 13 14 21 19 18 28 31	decmul1c	$$⊢25\cdot 8=200$$
33		4cn	$$⊢4\in ℂ$$
34	33	addid2i	$$⊢0+4=4$$
35	20 19 18 32 34	decaddi	$$⊢25\cdot 8+4=204$$
36		6cn	$$⊢6\in ℂ$$
37		8t6e48	$$⊢8\cdot 6=48$$
38	23 36 37	mulcomli	$$⊢6\cdot 8=48$$
39	5 15 16 17 5 18 35 38	decmul1c	$$⊢256\cdot 8=2048$$
40	12 39	eqtri	$$⊢2^8{2}^3=2048$$
41	9 40	eqtri	$$⊢2^{11}=2048$$