Theorem decexp2

Description: Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014)

	Ref	Expression
Hypotheses	decexp2.1	⊢ 𝑀 ∈ ℕ0
	decexp2.2	⊢ ( 𝑀 + 2 ) = 𝑁
Assertion	decexp2	⊢ ( ( 4 · ( 2 ↑ 𝑀 ) ) + 0 ) = ( 2 ↑ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		decexp2.1	⊢ 𝑀 ∈ ℕ0
2		decexp2.2	⊢ ( 𝑀 + 2 ) = 𝑁
3		2cn	⊢ 2 ∈ ℂ
4		2nn0	⊢ 2 ∈ ℕ0
5	4 1	nn0expcli	⊢ ( 2 ↑ 𝑀 ) ∈ ℕ0
6	5	nn0cni	⊢ ( 2 ↑ 𝑀 ) ∈ ℂ
7	3 6	mulcli	⊢ ( 2 · ( 2 ↑ 𝑀 ) ) ∈ ℂ
8		expp1	⊢ ( ( 2 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ ( 𝑀 + 1 ) ) = ( ( 2 ↑ 𝑀 ) · 2 ) )
9	3 1 8	mp2an	⊢ ( 2 ↑ ( 𝑀 + 1 ) ) = ( ( 2 ↑ 𝑀 ) · 2 )
10	6 3	mulcomi	⊢ ( ( 2 ↑ 𝑀 ) · 2 ) = ( 2 · ( 2 ↑ 𝑀 ) )
11	9 10	eqtr2i	⊢ ( 2 · ( 2 ↑ 𝑀 ) ) = ( 2 ↑ ( 𝑀 + 1 ) )
12	11	oveq1i	⊢ ( ( 2 · ( 2 ↑ 𝑀 ) ) · 2 ) = ( ( 2 ↑ ( 𝑀 + 1 ) ) · 2 )
13	7 3 12	mulcomli	⊢ ( 2 · ( 2 · ( 2 ↑ 𝑀 ) ) ) = ( ( 2 ↑ ( 𝑀 + 1 ) ) · 2 )
14	5	decbin0	⊢ ( 4 · ( 2 ↑ 𝑀 ) ) = ( 2 · ( 2 · ( 2 ↑ 𝑀 ) ) )
15		peano2nn0	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
16	1 15	ax-mp	⊢ ( 𝑀 + 1 ) ∈ ℕ0
17		expp1	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑀 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑀 + 1 ) ) · 2 ) )
18	3 16 17	mp2an	⊢ ( 2 ↑ ( ( 𝑀 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑀 + 1 ) ) · 2 )
19	13 14 18	3eqtr4i	⊢ ( 4 · ( 2 ↑ 𝑀 ) ) = ( 2 ↑ ( ( 𝑀 + 1 ) + 1 ) )
20		4nn0	⊢ 4 ∈ ℕ0
21	20 5	nn0mulcli	⊢ ( 4 · ( 2 ↑ 𝑀 ) ) ∈ ℕ0
22	21	nn0cni	⊢ ( 4 · ( 2 ↑ 𝑀 ) ) ∈ ℂ
23	22	addid1i	⊢ ( ( 4 · ( 2 ↑ 𝑀 ) ) + 0 ) = ( 4 · ( 2 ↑ 𝑀 ) )
24	1	nn0cni	⊢ 𝑀 ∈ ℂ
25		ax-1cn	⊢ 1 ∈ ℂ
26	24 25 25	addassi	⊢ ( ( 𝑀 + 1 ) + 1 ) = ( 𝑀 + ( 1 + 1 ) )
27		df-2	⊢ 2 = ( 1 + 1 )
28	27	oveq2i	⊢ ( 𝑀 + 2 ) = ( 𝑀 + ( 1 + 1 ) )
29	26 28 2	3eqtr2ri	⊢ 𝑁 = ( ( 𝑀 + 1 ) + 1 )
30	29	oveq2i	⊢ ( 2 ↑ 𝑁 ) = ( 2 ↑ ( ( 𝑀 + 1 ) + 1 ) )
31	19 23 30	3eqtr4i	⊢ ( ( 4 · ( 2 ↑ 𝑀 ) ) + 0 ) = ( 2 ↑ 𝑁 )