Theorem decbin2

Description: Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypothesis	decbin.1	$$⊢A\in {\mathbb{N}}_0$$
Assertion	decbin2	$$⊢4A+2=2\left(2A+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		decbin.1	$$⊢A\in {\mathbb{N}}_0$$
2		2t1e2	$$⊢2\cdot 1=2$$
3	2	oveq2i	$$⊢22A+2\cdot 1=22A+2$$
4		2cn	$$⊢2\in ℂ$$
5	1	nn0cni	$$⊢A\in ℂ$$
6	4 5	mulcli	$$⊢2A\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
8	4 6 7	adddii	$$⊢2\left(2A+1\right)=22A+2\cdot 1$$
9	1	decbin0	$$⊢4A=22A$$
10	9	oveq1i	$$⊢4A+2=22A+2$$
11	3 8 10	3eqtr4ri	$$⊢4A+2=2\left(2A+1\right)$$