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 e. NN0
Assertion decbin0 
|- ( 4 x. A ) = ( 2 x. ( 2 x. A ) )

Proof

Step Hyp Ref Expression
1 decbin.1 
 |-  A e. NN0
2 2t2e4 
 |-  ( 2 x. 2 ) = 4
3 2 oveq1i 
 |-  ( ( 2 x. 2 ) x. A ) = ( 4 x. A )
4 2cn 
 |-  2 e. CC
5 1 nn0cni 
 |-  A e. CC
6 4 4 5 mulassi 
 |-  ( ( 2 x. 2 ) x. A ) = ( 2 x. ( 2 x. A ) )
7 3 6 eqtr3i 
 |-  ( 4 x. A ) = ( 2 x. ( 2 x. A ) )