Metamath Proof Explorer

Theorem sq4e2t8

Description: The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion sq4e2t8 
|- ( 4 ^ 2 ) = ( 2 x. 8 )

Proof

Step Hyp Ref Expression
1 2t2e4 
 |-  ( 2 x. 2 ) = 4
2 1 eqcomi 
 |-  4 = ( 2 x. 2 )
3 2 oveq1i 
 |-  ( 4 ^ 2 ) = ( ( 2 x. 2 ) ^ 2 )
4 2cn 
 |-  2 e. CC
5 4 4 sqmuli 
 |-  ( ( 2 x. 2 ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( 2 ^ 2 ) )
6 4 sqvali 
 |-  ( 2 ^ 2 ) = ( 2 x. 2 )
7 sq2 
 |-  ( 2 ^ 2 ) = 4
8 6 7 oveq12i 
 |-  ( ( 2 ^ 2 ) x. ( 2 ^ 2 ) ) = ( ( 2 x. 2 ) x. 4 )
9 4cn 
 |-  4 e. CC
10 4 4 9 mulassi 
 |-  ( ( 2 x. 2 ) x. 4 ) = ( 2 x. ( 2 x. 4 ) )
11 4t2e8 
 |-  ( 4 x. 2 ) = 8
12 9 4 11 mulcomli 
 |-  ( 2 x. 4 ) = 8
13 12 oveq2i 
 |-  ( 2 x. ( 2 x. 4 ) ) = ( 2 x. 8 )
14 8 10 13 3eqtri 
 |-  ( ( 2 ^ 2 ) x. ( 2 ^ 2 ) ) = ( 2 x. 8 )
15 3 5 14 3eqtri 
 |-  ( 4 ^ 2 ) = ( 2 x. 8 )