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