Metamath Proof Explorer

Theorem 2exp7

Description: Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021)

Ref Expression
Assertion 2exp7 
|- ( 2 ^ 7 ) = ; ; 1 2 8

Proof

Step Hyp Ref Expression
1 df-7 
 |-  7 = ( 6 + 1 )
2 1 oveq2i 
 |-  ( 2 ^ 7 ) = ( 2 ^ ( 6 + 1 ) )
3 2cn 
 |-  2 e. CC
4 6nn0 
 |-  6 e. NN0
5 expp1 
 |-  ( ( 2 e. CC /\ 6 e. NN0 ) -> ( 2 ^ ( 6 + 1 ) ) = ( ( 2 ^ 6 ) x. 2 ) )
6 3 4 5 mp2an 
 |-  ( 2 ^ ( 6 + 1 ) ) = ( ( 2 ^ 6 ) x. 2 )
7 2exp6 
 |-  ( 2 ^ 6 ) = ; 6 4
8 7 oveq1i 
 |-  ( ( 2 ^ 6 ) x. 2 ) = ( ; 6 4 x. 2 )
9 6 8 eqtri 
 |-  ( 2 ^ ( 6 + 1 ) ) = ( ; 6 4 x. 2 )
10 2 9 eqtri 
 |-  ( 2 ^ 7 ) = ( ; 6 4 x. 2 )
11 2nn0 
 |-  2 e. NN0
12 4nn0 
 |-  4 e. NN0
13 eqid 
 |-  ; 6 4 = ; 6 4
14 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
15 4t2e8 
 |-  ( 4 x. 2 ) = 8
16 11 4 12 13 14 15 decmul1 
 |-  ( ; 6 4 x. 2 ) = ; ; 1 2 8
17 10 16 eqtri 
 |-  ( 2 ^ 7 ) = ; ; 1 2 8