Theorem decbin3

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	decbin3	$$⊢4A+3=2\left(2A+1\right)+1$$

Proof

Step	Hyp	Ref	Expression
1		decbin.1	$$⊢A\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		2p1e3	$$⊢2+1=3$$
5	1	decbin2	$$⊢4A+2=2\left(2A+1\right)$$
6	5	eqcomi	$$⊢2\left(2A+1\right)=4A+2$$
7	2 1 3 4 6	numsuc	$$⊢2\left(2A+1\right)+1=4A+3$$
8	7	eqcomi	$$⊢4A+3=2\left(2A+1\right)+1$$