Metamath Proof Explorer


Theorem sq7

Description: The square of 7 is 49. (Contributed by SN, 26-Aug-2025)

Ref Expression
Assertion sq7
|- ( 7 ^ 2 ) = ; 4 9

Proof

Step Hyp Ref Expression
1 7cn
 |-  7 e. CC
2 1 sqvali
 |-  ( 7 ^ 2 ) = ( 7 x. 7 )
3 7t7e49
 |-  ( 7 x. 7 ) = ; 4 9
4 2 3 eqtri
 |-  ( 7 ^ 2 ) = ; 4 9