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 ∈ ℕ0
2		4nn0	⊢ 4 ∈ ℕ0
3	2	nn0cni	⊢ 4 ∈ ℂ
4		2cn	⊢ 2 ∈ ℂ
5		4t2e8	⊢ ( 4 · 2 ) = 8
6	3 4 5	mulcomli	⊢ ( 2 · 4 ) = 8
7		2exp4	⊢ ( 2 ↑ 4 ) = ; 1 6
8		1nn0	⊢ 1 ∈ ℕ0
9		6nn0	⊢ 6 ∈ ℕ0
10	8 9	deccl	⊢ ; 1 6 ∈ ℕ0
11		eqid	⊢ ; 1 6 = ; 1 6
12		9nn0	⊢ 9 ∈ ℕ0
13	10	nn0cni	⊢ ; 1 6 ∈ ℂ
14	13	mulid1i	⊢ ( ; 1 6 · 1 ) = ; 1 6
15		1p1e2	⊢ ( 1 + 1 ) = 2
16		5nn0	⊢ 5 ∈ ℕ0
17		9cn	⊢ 9 ∈ ℂ
18		6cn	⊢ 6 ∈ ℂ
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 · 1 ) + 9 ) = ; 2 5
22		3nn0	⊢ 3 ∈ ℕ0
23	18	mulid2i	⊢ ( 1 · 6 ) = 6
24	23	oveq1i	⊢ ( ( 1 · 6 ) + 3 ) = ( 6 + 3 )
25		6p3e9	⊢ ( 6 + 3 ) = 9
26	24 25	eqtri	⊢ ( ( 1 · 6 ) + 3 ) = 9
27		6t6e36	⊢ ( 6 · 6 ) = ; 3 6
28	9 8 9 11 9 22 26 27	decmul1c	⊢ ( ; 1 6 · 6 ) = ; 9 6
29	10 8 9 11 9 12 21 28	decmul2c	⊢ ( ; 1 6 · ; 1 6 ) = ; ; 2 5 6
30	1 2 6 7 29	numexp2x	⊢ ( 2 ↑ 8 ) = ; ; 2 5 6