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		2t4e8	|- ( 2 x. 4 ) = 8
4		2exp4	|- ( 2 ^ 4 ) = ; 1 6
5		1nn0	|- 1 e. NN0
6		6nn0	|- 6 e. NN0
7	5 6	deccl	|- ; 1 6 e. NN0
8		eqid	|- ; 1 6 = ; 1 6
9		9nn0	|- 9 e. NN0
10	7	nn0cni	|- ; 1 6 e. CC
11	10	mulridi	|- ( ; 1 6 x. 1 ) = ; 1 6
12		1p1e2	|- ( 1 + 1 ) = 2
13		5nn0	|- 5 e. NN0
14		9cn	|- 9 e. CC
15		6cn	|- 6 e. CC
16		9p6e15	|- ( 9 + 6 ) = ; 1 5
17	14 15 16	addcomli	|- ( 6 + 9 ) = ; 1 5
18	5 6 9 11 12 13 17	decaddci	|- ( ( ; 1 6 x. 1 ) + 9 ) = ; 2 5
19		3nn0	|- 3 e. NN0
20	15	mullidi	|- ( 1 x. 6 ) = 6
21	20	oveq1i	|- ( ( 1 x. 6 ) + 3 ) = ( 6 + 3 )
22		6p3e9	|- ( 6 + 3 ) = 9
23	21 22	eqtri	|- ( ( 1 x. 6 ) + 3 ) = 9
24		6t6e36	|- ( 6 x. 6 ) = ; 3 6
25	6 5 6 8 6 19 23 24	decmul1c	|- ( ; 1 6 x. 6 ) = ; 9 6
26	7 5 6 8 6 9 18 25	decmul2c	|- ( ; 1 6 x. ; 1 6 ) = ; ; 2 5 6
27	1 2 3 4 26	numexp2x	|- ( 2 ^ 8 ) = ; ; 2 5 6