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		2t4e8	$$⊢2\cdot 4=8$$
4		2exp4	$$⊢2^4=16$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		6nn0	$$⊢6\in {\mathbb{N}}_0$$
7	5 6	deccl	$$⊢16\in {\mathbb{N}}_0$$
8		eqid	$$⊢16=16$$
9		9nn0	$$⊢9\in {\mathbb{N}}_0$$
10	7	nn0cni	$$⊢16\in ℂ$$
11	10	mulridi	$$⊢16\cdot 1=16$$
12		1p1e2	$$⊢1+1=2$$
13		5nn0	$$⊢5\in {\mathbb{N}}_0$$
14		9cn	$$⊢9\in ℂ$$
15		6cn	$$⊢6\in ℂ$$
16		9p6e15	$$⊢9+6=15$$
17	14 15 16	addcomli	$$⊢6+9=15$$
18	5 6 9 11 12 13 17	decaddci	$$⊢16\cdot 1+9=25$$
19		3nn0	$$⊢3\in {\mathbb{N}}_0$$
20	15	mullidi	$$⊢1\cdot 6=6$$
21	20	oveq1i	$$⊢1\cdot 6+3=6+3$$
22		6p3e9	$$⊢6+3=9$$
23	21 22	eqtri	$$⊢1\cdot 6+3=9$$
24		6t6e36	$$⊢6\cdot 6=36$$
25	6 5 6 8 6 19 23 24	decmul1c	$$⊢16\cdot 6=96$$
26	7 5 6 8 6 9 18 25	decmul2c	$$⊢16\cdot 16=256$$
27	1 2 3 4 26	numexp2x	$$⊢2^8=256$$