Theorem 2exp16

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

	Ref	Expression
Assertion	2exp16	|- ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2		8nn0	|- 8 e. NN0
3		8cn	|- 8 e. CC
4		2cn	|- 2 e. CC
5		8t2e16	|- ( 8 x. 2 ) = ; 1 6
6	3 4 5	mulcomli	|- ( 2 x. 8 ) = ; 1 6
7		2exp8	|- ( 2 ^ 8 ) = ; ; 2 5 6
8		5nn0	|- 5 e. NN0
9	1 8	deccl	|- ; 2 5 e. NN0
10		6nn0	|- 6 e. NN0
11	9 10	deccl	|- ; ; 2 5 6 e. NN0
12		eqid	|- ; ; 2 5 6 = ; ; 2 5 6
13		1nn0	|- 1 e. NN0
14	13 8	deccl	|- ; 1 5 e. NN0
15		3nn0	|- 3 e. NN0
16	14 15	deccl	|- ; ; 1 5 3 e. NN0
17		eqid	|- ; 2 5 = ; 2 5
18		eqid	|- ; ; 1 5 3 = ; ; 1 5 3
19	13 1	deccl	|- ; 1 2 e. NN0
20	19 2	deccl	|- ; ; 1 2 8 e. NN0
21		4nn0	|- 4 e. NN0
22	13 21	deccl	|- ; 1 4 e. NN0
23		eqid	|- ; 1 5 = ; 1 5
24		eqid	|- ; ; 1 2 8 = ; ; 1 2 8
25		0nn0	|- 0 e. NN0
26	13	dec0h	|- 1 = ; 0 1
27		eqid	|- ; 1 2 = ; 1 2
28		0p1e1	|- ( 0 + 1 ) = 1
29		1p2e3	|- ( 1 + 2 ) = 3
30	25 13 13 1 26 27 28 29	decadd	|- ( 1 + ; 1 2 ) = ; 1 3
31		3p1e4	|- ( 3 + 1 ) = 4
32	13 15 13 30 31	decaddi	|- ( ( 1 + ; 1 2 ) + 1 ) = ; 1 4
33		5cn	|- 5 e. CC
34		8p5e13	|- ( 8 + 5 ) = ; 1 3
35	3 33 34	addcomli	|- ( 5 + 8 ) = ; 1 3
36	13 8 19 2 23 24 32 15 35	decaddc	|- ( ; 1 5 + ; ; 1 2 8 ) = ; ; 1 4 3
37		eqid	|- ; 1 4 = ; 1 4
38		4p1e5	|- ( 4 + 1 ) = 5
39	13 21 13 37 38	decaddi	|- ( ; 1 4 + 1 ) = ; 1 5
40		2t2e4	|- ( 2 x. 2 ) = 4
41		1p1e2	|- ( 1 + 1 ) = 2
42	40 41	oveq12i	|- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
43		4p2e6	|- ( 4 + 2 ) = 6
44	42 43	eqtri	|- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
45		5t2e10	|- ( 5 x. 2 ) = ; 1 0
46	33	addid2i	|- ( 0 + 5 ) = 5
47	13 25 8 45 46	decaddi	|- ( ( 5 x. 2 ) + 5 ) = ; 1 5
48	1 8 13 8 17 39 1 8 13 44 47	decmac	|- ( ( ; 2 5 x. 2 ) + ( ; 1 4 + 1 ) ) = ; 6 5
49		6t2e12	|- ( 6 x. 2 ) = ; 1 2
50		3cn	|- 3 e. CC
51		3p2e5	|- ( 3 + 2 ) = 5
52	50 4 51	addcomli	|- ( 2 + 3 ) = 5
53	13 1 15 49 52	decaddi	|- ( ( 6 x. 2 ) + 3 ) = ; 1 5
54	9 10 22 15 12 36 1 8 13 48 53	decmac	|- ( ( ; ; 2 5 6 x. 2 ) + ( ; 1 5 + ; ; 1 2 8 ) ) = ; ; 6 5 5
55	15	dec0h	|- 3 = ; 0 3
56	50	addid2i	|- ( 0 + 3 ) = 3
57	56 55	eqtri	|- ( 0 + 3 ) = ; 0 3
58	4	addid2i	|- ( 0 + 2 ) = 2
59	58	oveq2i	|- ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ( ( 2 x. 5 ) + 2 )
60	33 4 45	mulcomli	|- ( 2 x. 5 ) = ; 1 0
61	13 25 1 60 58	decaddi	|- ( ( 2 x. 5 ) + 2 ) = ; 1 2
62	59 61	eqtri	|- ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ; 1 2
63		5t5e25	|- ( 5 x. 5 ) = ; 2 5
64		5p3e8	|- ( 5 + 3 ) = 8
65	1 8 15 63 64	decaddi	|- ( ( 5 x. 5 ) + 3 ) = ; 2 8
66	1 8 25 15 17 57 8 2 1 62 65	decmac	|- ( ( ; 2 5 x. 5 ) + ( 0 + 3 ) ) = ; ; 1 2 8
67		6t5e30	|- ( 6 x. 5 ) = ; 3 0
68	15 25 15 67 56	decaddi	|- ( ( 6 x. 5 ) + 3 ) = ; 3 3
69	9 10 25 15 12 55 8 15 15 66 68	decmac	|- ( ( ; ; 2 5 6 x. 5 ) + 3 ) = ; ; ; 1 2 8 3
70	1 8 14 15 17 18 11 15 20 54 69	decma2c	|- ( ( ; ; 2 5 6 x. ; 2 5 ) + ; ; 1 5 3 ) = ; ; ; 6 5 5 3
71		6cn	|- 6 e. CC
72	71 4 49	mulcomli	|- ( 2 x. 6 ) = ; 1 2
73	13 1 15 72 52	decaddi	|- ( ( 2 x. 6 ) + 3 ) = ; 1 5
74	71 33 67	mulcomli	|- ( 5 x. 6 ) = ; 3 0
75	15 25 15 74 56	decaddi	|- ( ( 5 x. 6 ) + 3 ) = ; 3 3
76	1 8 15 17 10 15 15 73 75	decrmac	|- ( ( ; 2 5 x. 6 ) + 3 ) = ; ; 1 5 3
77		6t6e36	|- ( 6 x. 6 ) = ; 3 6
78	10 9 10 12 10 15 76 77	decmul1c	|- ( ; ; 2 5 6 x. 6 ) = ; ; ; 1 5 3 6
79	11 9 10 12 10 16 70 78	decmul2c	|- ( ; ; 2 5 6 x. ; ; 2 5 6 ) = ; ; ; ; 6 5 5 3 6
80	1 2 6 7 79	numexp2x	|- ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6