Theorem 2exp8

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

	Ref	Expression
Assertion	2exp8	|- ( 2 ^ 8 ) = ; ; 2 5 6

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2		4nn0	|- 4 e. NN0
3	2	nn0cni	|- 4 e. CC
4		2cn	|- 2 e. CC
5		4t2e8	|- ( 4 x. 2 ) = 8
6	3 4 5	mulcomli	|- ( 2 x. 4 ) = 8
7		2exp4	|- ( 2 ^ 4 ) = ; 1 6
8		1nn0	|- 1 e. NN0
9		6nn0	|- 6 e. NN0
10	8 9	deccl	|- ; 1 6 e. NN0
11		eqid	|- ; 1 6 = ; 1 6
12		9nn0	|- 9 e. NN0
13	10	nn0cni	|- ; 1 6 e. CC
14	13	mulid1i	|- ( ; 1 6 x. 1 ) = ; 1 6
15		1p1e2	|- ( 1 + 1 ) = 2
16		5nn0	|- 5 e. NN0
17		9cn	|- 9 e. CC
18		6cn	|- 6 e. CC
19		9p6e15	|- ( 9 + 6 ) = ; 1 5
20	17 18 19	addcomli	|- ( 6 + 9 ) = ; 1 5
21	8 9 12 14 15 16 20	decaddci	|- ( ( ; 1 6 x. 1 ) + 9 ) = ; 2 5
22		3nn0	|- 3 e. NN0
23	18	mulid2i	|- ( 1 x. 6 ) = 6
24	23	oveq1i	|- ( ( 1 x. 6 ) + 3 ) = ( 6 + 3 )
25		6p3e9	|- ( 6 + 3 ) = 9
26	24 25	eqtri	|- ( ( 1 x. 6 ) + 3 ) = 9
27		6t6e36	|- ( 6 x. 6 ) = ; 3 6
28	9 8 9 11 9 22 26 27	decmul1c	|- ( ; 1 6 x. 6 ) = ; 9 6
29	10 8 9 11 9 12 21 28	decmul2c	|- ( ; 1 6 x. ; 1 6 ) = ; ; 2 5 6
30	1 2 6 7 29	numexp2x	|- ( 2 ^ 8 ) = ; ; 2 5 6