Metamath Proof Explorer

Theorem decexp2

Description: Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014)

Ref Expression
Hypotheses decexp2.1 
|- M e. NN0
decexp2.2 
|- ( M + 2 ) = N
Assertion decexp2 
|- ( ( 4 x. ( 2 ^ M ) ) + 0 ) = ( 2 ^ N )

Proof

Step Hyp Ref Expression
1 decexp2.1 
 |-  M e. NN0
2 decexp2.2 
 |-  ( M + 2 ) = N
3 2cn 
 |-  2 e. CC
4 2nn0 
 |-  2 e. NN0
5 4 1 nn0expcli 
 |-  ( 2 ^ M ) e. NN0
6 5 nn0cni 
 |-  ( 2 ^ M ) e. CC
7 3 6 mulcli 
 |-  ( 2 x. ( 2 ^ M ) ) e. CC
8 expp1 
 |-  ( ( 2 e. CC /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) = ( ( 2 ^ M ) x. 2 ) )
9 3 1 8 mp2an 
 |-  ( 2 ^ ( M + 1 ) ) = ( ( 2 ^ M ) x. 2 )
10 6 3 mulcomi 
 |-  ( ( 2 ^ M ) x. 2 ) = ( 2 x. ( 2 ^ M ) )
11 9 10 eqtr2i 
 |-  ( 2 x. ( 2 ^ M ) ) = ( 2 ^ ( M + 1 ) )
12 11 oveq1i 
 |-  ( ( 2 x. ( 2 ^ M ) ) x. 2 ) = ( ( 2 ^ ( M + 1 ) ) x. 2 )
13 7 3 12 mulcomli 
 |-  ( 2 x. ( 2 x. ( 2 ^ M ) ) ) = ( ( 2 ^ ( M + 1 ) ) x. 2 )
14 5 decbin0 
 |-  ( 4 x. ( 2 ^ M ) ) = ( 2 x. ( 2 x. ( 2 ^ M ) ) )
15 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
16 1 15 ax-mp 
 |-  ( M + 1 ) e. NN0
17 expp1 
 |-  ( ( 2 e. CC /\ ( M + 1 ) e. NN0 ) -> ( 2 ^ ( ( M + 1 ) + 1 ) ) = ( ( 2 ^ ( M + 1 ) ) x. 2 ) )
18 3 16 17 mp2an 
 |-  ( 2 ^ ( ( M + 1 ) + 1 ) ) = ( ( 2 ^ ( M + 1 ) ) x. 2 )
19 13 14 18 3eqtr4i 
 |-  ( 4 x. ( 2 ^ M ) ) = ( 2 ^ ( ( M + 1 ) + 1 ) )
20 4nn0 
 |-  4 e. NN0
21 20 5 nn0mulcli 
 |-  ( 4 x. ( 2 ^ M ) ) e. NN0
22 21 nn0cni 
 |-  ( 4 x. ( 2 ^ M ) ) e. CC
23 22 addid1i 
 |-  ( ( 4 x. ( 2 ^ M ) ) + 0 ) = ( 4 x. ( 2 ^ M ) )
24 1 nn0cni 
 |-  M e. CC
25 ax-1cn 
 |-  1 e. CC
26 24 25 25 addassi 
 |-  ( ( M + 1 ) + 1 ) = ( M + ( 1 + 1 ) )
27 df-2 
 |-  2 = ( 1 + 1 )
28 27 oveq2i 
 |-  ( M + 2 ) = ( M + ( 1 + 1 ) )
29 26 28 2 3eqtr2ri 
 |-  N = ( ( M + 1 ) + 1 )
30 29 oveq2i 
 |-  ( 2 ^ N ) = ( 2 ^ ( ( M + 1 ) + 1 ) )
31 19 23 30 3eqtr4i 
 |-  ( ( 4 x. ( 2 ^ M ) ) + 0 ) = ( 2 ^ N )