Theorem decbin3

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

	Ref	Expression
Hypothesis	decbin.1	⊢ 𝐴 ∈ ℕ0
Assertion	decbin3	⊢ ( ( 4 · 𝐴 ) + 3 ) = ( ( 2 · ( ( 2 · 𝐴 ) + 1 ) ) + 1 )

Proof

Step	Hyp	Ref	Expression
1		decbin.1	⊢ 𝐴 ∈ ℕ0
2		4nn0	⊢ 4 ∈ ℕ0
3		2nn0	⊢ 2 ∈ ℕ0
4		2p1e3	⊢ ( 2 + 1 ) = 3
5	1	decbin2	⊢ ( ( 4 · 𝐴 ) + 2 ) = ( 2 · ( ( 2 · 𝐴 ) + 1 ) )
6	5	eqcomi	⊢ ( 2 · ( ( 2 · 𝐴 ) + 1 ) ) = ( ( 4 · 𝐴 ) + 2 )
7	2 1 3 4 6	numsuc	⊢ ( ( 2 · ( ( 2 · 𝐴 ) + 1 ) ) + 1 ) = ( ( 4 · 𝐴 ) + 3 )
8	7	eqcomi	⊢ ( ( 4 · 𝐴 ) + 3 ) = ( ( 2 · ( ( 2 · 𝐴 ) + 1 ) ) + 1 )