Metamath Proof Explorer

Theorem 2exp5

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

Ref Expression
Assertion 2exp5 
|- ( 2 ^ 5 ) = ; 3 2

Proof

Step Hyp Ref Expression
1 3p2e5 
 |-  ( 3 + 2 ) = 5
2 1 eqcomi 
 |-  5 = ( 3 + 2 )
3 2 oveq2i 
 |-  ( 2 ^ 5 ) = ( 2 ^ ( 3 + 2 ) )
4 2cn 
 |-  2 e. CC
5 3nn0 
 |-  3 e. NN0
6 2nn0 
 |-  2 e. NN0
7 expadd 
 |-  ( ( 2 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 2 ^ ( 3 + 2 ) ) = ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) ) )
8 4 5 6 7 mp3an 
 |-  ( 2 ^ ( 3 + 2 ) ) = ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) )
9 cu2 
 |-  ( 2 ^ 3 ) = 8
10 sq2 
 |-  ( 2 ^ 2 ) = 4
11 9 10 oveq12i 
 |-  ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) ) = ( 8 x. 4 )
12 8 11 eqtri 
 |-  ( 2 ^ ( 3 + 2 ) ) = ( 8 x. 4 )
13 3 12 eqtri 
 |-  ( 2 ^ 5 ) = ( 8 x. 4 )
14 8t4e32 
 |-  ( 8 x. 4 ) = ; 3 2
15 13 14 eqtri 
 |-  ( 2 ^ 5 ) = ; 3 2