Theorem 2exp16

Description: Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Assertion	2exp16	$$⊢2^{16}=65536$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		8nn0	$$⊢8\in {\mathbb{N}}_0$$
3		8cn	$$⊢8\in ℂ$$
4		2cn	$$⊢2\in ℂ$$
5		8t2e16	$$⊢8\cdot 2=16$$
6	3 4 5	mulcomli	$$⊢2\cdot 8=16$$
7		2exp8	$$⊢2^8=256$$
8		5nn0	$$⊢5\in {\mathbb{N}}_0$$
9	1 8	deccl	$$⊢25\in {\mathbb{N}}_0$$
10		6nn0	$$⊢6\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢256\in {\mathbb{N}}_0$$
12		eqid	$$⊢256=256$$
13		1nn0	$$⊢1\in {\mathbb{N}}_0$$
14	13 8	deccl	$$⊢15\in {\mathbb{N}}_0$$
15		3nn0	$$⊢3\in {\mathbb{N}}_0$$
16	14 15	deccl	$$⊢153\in {\mathbb{N}}_0$$
17		eqid	$$⊢25=25$$
18		eqid	$$⊢153=153$$
19	13 1	deccl	$$⊢12\in {\mathbb{N}}_0$$
20	19 2	deccl	$$⊢128\in {\mathbb{N}}_0$$
21		4nn0	$$⊢4\in {\mathbb{N}}_0$$
22	13 21	deccl	$$⊢14\in {\mathbb{N}}_0$$
23		eqid	$$⊢15=15$$
24		eqid	$$⊢128=128$$
25		0nn0	$$⊢0\in {\mathbb{N}}_0$$
26	13	dec0h	$$⊢1=01$$
27		eqid	$$⊢12=12$$
28		0p1e1	$$⊢0+1=1$$
29		1p2e3	$$⊢1+2=3$$
30	25 13 13 1 26 27 28 29	decadd	$$⊢1+12=13$$
31		3p1e4	$$⊢3+1=4$$
32	13 15 13 30 31	decaddi	$$⊢1+12+1=14$$
33		5cn	$$⊢5\in ℂ$$
34		8p5e13	$$⊢8+5=13$$
35	3 33 34	addcomli	$$⊢5+8=13$$
36	13 8 19 2 23 24 32 15 35	decaddc	$$⊢15+128=143$$
37		eqid	$$⊢14=14$$
38		4p1e5	$$⊢4+1=5$$
39	13 21 13 37 38	decaddi	$$⊢14+1=15$$
40		2t2e4	$$⊢2\cdot 2=4$$
41		1p1e2	$$⊢1+1=2$$
42	40 41	oveq12i	$$⊢2\cdot 2+1+1=4+2$$
43		4p2e6	$$⊢4+2=6$$
44	42 43	eqtri	$$⊢2\cdot 2+1+1=6$$
45		5t2e10	$$⊢5\cdot 2=10$$
46	33	addlidi	$$⊢0+5=5$$
47	13 25 8 45 46	decaddi	$$⊢5\cdot 2+5=15$$
48	1 8 13 8 17 39 1 8 13 44 47	decmac	$$⊢25\cdot 2+14+1=65$$
49		6t2e12	$$⊢6\cdot 2=12$$
50		3cn	$$⊢3\in ℂ$$
51		3p2e5	$$⊢3+2=5$$
52	50 4 51	addcomli	$$⊢2+3=5$$
53	13 1 15 49 52	decaddi	$$⊢6\cdot 2+3=15$$
54	9 10 22 15 12 36 1 8 13 48 53	decmac	$$⊢256\cdot 2+15+128=655$$
55	15	dec0h	$$⊢3=03$$
56	50	addlidi	$$⊢0+3=3$$
57	56 55	eqtri	$$⊢0+3=03$$
58	4	addlidi	$$⊢0+2=2$$
59	58	oveq2i	$$⊢2\cdot 5+0+2=2\cdot 5+2$$
60	33 4 45	mulcomli	$$⊢2\cdot 5=10$$
61	13 25 1 60 58	decaddi	$$⊢2\cdot 5+2=12$$
62	59 61	eqtri	$$⊢2\cdot 5+0+2=12$$
63		5t5e25	$$⊢5\cdot 5=25$$
64		5p3e8	$$⊢5+3=8$$
65	1 8 15 63 64	decaddi	$$⊢5\cdot 5+3=28$$
66	1 8 25 15 17 57 8 2 1 62 65	decmac	$$⊢25\cdot 5+0+3=128$$
67		6t5e30	$$⊢6\cdot 5=30$$
68	15 25 15 67 56	decaddi	$$⊢6\cdot 5+3=33$$
69	9 10 25 15 12 55 8 15 15 66 68	decmac	$$⊢256\cdot 5+3=1283$$
70	1 8 14 15 17 18 11 15 20 54 69	decma2c	$$⊢256\cdot 25+153=6553$$
71		6cn	$$⊢6\in ℂ$$
72	71 4 49	mulcomli	$$⊢2\cdot 6=12$$
73	13 1 15 72 52	decaddi	$$⊢2\cdot 6+3=15$$
74	71 33 67	mulcomli	$$⊢5\cdot 6=30$$
75	15 25 15 74 56	decaddi	$$⊢5\cdot 6+3=33$$
76	1 8 15 17 10 15 15 73 75	decrmac	$$⊢25\cdot 6+3=153$$
77		6t6e36	$$⊢6\cdot 6=36$$
78	10 9 10 12 10 15 76 77	decmul1c	$$⊢256\cdot 6=1536$$
79	11 9 10 12 10 16 70 78	decmul2c	$$⊢256\cdot 256=65536$$
80	1 2 6 7 79	numexp2x	$$⊢2^{16}=65536$$