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

Metamath Proof Explorer

Theorem decbin2

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

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

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