Theorem decexp2

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

	Ref	Expression
Hypotheses	decexp2.1	$$⊢M\in {\mathbb{N}}_0$$
	decexp2.2	$$⊢M+2=N$$
Assertion	decexp2	$$⊢42^M+0=2^N$$

Proof

Step	Hyp	Ref	Expression
1		decexp2.1	$$⊢M\in {\mathbb{N}}_0$$
2		decexp2.2	$$⊢M+2=N$$
3		2cn	$$⊢2\in ℂ$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5	4 1	nn0expcli	$$⊢2^M\in {\mathbb{N}}_0$$
6	5	nn0cni	$$⊢2^M\in ℂ$$
7	3 6	mulcli	$$⊢22^M\in ℂ$$
8		expp1	$$⊢\left(2\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to 2^{M+1}=2^M\cdot 2$$
9	3 1 8	mp2an	$$⊢2^{M+1}=2^M\cdot 2$$
10	6 3	mulcomi	$$⊢2^M\cdot 2=22^M$$
11	9 10	eqtr2i	$$⊢22^M=2^{M+1}$$
12	11	oveq1i	$$⊢22^M\cdot 2=2^{M+1}\cdot 2$$
13	7 3 12	mulcomli	$$⊢222^M=2^{M+1}\cdot 2$$
14	5	decbin0	$$⊢42^M=222^M$$
15		peano2nn0	$$⊢M\in {\mathbb{N}}_0\to M+1\in {\mathbb{N}}_0$$
16	1 15	ax-mp	$$⊢M+1\in {\mathbb{N}}_0$$
17		expp1	$$⊢\left(2\in ℂ\wedge M+1\in {\mathbb{N}}_0\right)\to 2^{M+1+1}=2^{M+1}\cdot 2$$
18	3 16 17	mp2an	$$⊢2^{M+1+1}=2^{M+1}\cdot 2$$
19	13 14 18	3eqtr4i	$$⊢42^M=2^{M+1+1}$$
20		4nn0	$$⊢4\in {\mathbb{N}}_0$$
21	20 5	nn0mulcli	$$⊢42^M\in {\mathbb{N}}_0$$
22	21	nn0cni	$$⊢42^M\in ℂ$$
23	22	addridi	$$⊢42^M+0=42^M$$
24	1	nn0cni	$$⊢M\in ℂ$$
25		ax-1cn	$$⊢1\in ℂ$$
26	24 25 25	addassi	$$⊢M+1+1=M+1+1$$
27		df-2	$$⊢2=1+1$$
28	27	oveq2i	$$⊢M+2=M+1+1$$
29	26 28 2	3eqtr2ri	$$⊢N=M+1+1$$
30	29	oveq2i	$$⊢2^N=2^{M+1+1}$$
31	19 23 30	3eqtr4i	$$⊢42^M+0=2^N$$