Theorem 2exp8

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

	Ref	Expression
Assertion	2exp8	$$⊢2^8=256$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3	2	nn0cni	$$⊢4\in ℂ$$
4		2cn	$$⊢2\in ℂ$$
5		4t2e8	$$⊢4\cdot 2=8$$
6	3 4 5	mulcomli	$$⊢2\cdot 4=8$$
7		2exp4	$$⊢2^4=16$$
8		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9		6nn0	$$⊢6\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢16\in {\mathbb{N}}_0$$
11		eqid	$$⊢16=16$$
12		9nn0	$$⊢9\in {\mathbb{N}}_0$$
13	10	nn0cni	$$⊢16\in ℂ$$
14	13	mulridi	$$⊢16\cdot 1=16$$
15		1p1e2	$$⊢1+1=2$$
16		5nn0	$$⊢5\in {\mathbb{N}}_0$$
17		9cn	$$⊢9\in ℂ$$
18		6cn	$$⊢6\in ℂ$$
19		9p6e15	$$⊢9+6=15$$
20	17 18 19	addcomli	$$⊢6+9=15$$
21	8 9 12 14 15 16 20	decaddci	$$⊢16\cdot 1+9=25$$
22		3nn0	$$⊢3\in {\mathbb{N}}_0$$
23	18	mullidi	$$⊢1\cdot 6=6$$
24	23	oveq1i	$$⊢1\cdot 6+3=6+3$$
25		6p3e9	$$⊢6+3=9$$
26	24 25	eqtri	$$⊢1\cdot 6+3=9$$
27		6t6e36	$$⊢6\cdot 6=36$$
28	9 8 9 11 9 22 26 27	decmul1c	$$⊢16\cdot 6=96$$
29	10 8 9 11 9 12 21 28	decmul2c	$$⊢16\cdot 16=256$$
30	1 2 6 7 29	numexp2x	$$⊢2^8=256$$