This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decbin0

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

		Ref	Expression
	Hypothesis	decbin.1	$⊢ A \in ℕ_{0}$
	Assertion	decbin0	$⊢ 4 A = 2 2 A$

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