Theorem decbin0

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	decbin0	$$⊢4A=22A$$

Proof

Step	Hyp	Ref	Expression
1		decbin.1	$$⊢A\in {\mathbb{N}}_0$$
2		2t2e4	$$⊢2\cdot 2=4$$
3	2	oveq1i	$$⊢2\cdot 2A=4A$$
4		2cn	$$⊢2\in ℂ$$
5	1	nn0cni	$$⊢A\in ℂ$$
6	4 4 5	mulassi	$$⊢2\cdot 2A=22A$$
7	3 6	eqtr3i	$$⊢4A=22A$$