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

Metamath Proof Explorer

Theorem decbin3

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

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

Step	Hyp	Ref	Expression
1		decbin.1	$⊢ A \in ℕ_{0}$
2		4nn0	$⊢ 4 \in ℕ_{0}$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4		2p1e3	$⊢ 2 + 1 = 3$
5	1	decbin2	$⊢ 4 A + 2 = 2 (2 A + 1)$
6	5	eqcomi	$⊢ 2 (2 A + 1) = 4 A + 2$
7	2 1 3 4 6	numsuc	$⊢ 2 (2 A + 1) + 1 = 4 A + 3$
8	7	eqcomi	$⊢ 4 A + 3 = 2 (2 A + 1) + 1$