Metamath Proof Explorer


Theorem sq7

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

Ref Expression
Assertion sq7 7 2 = 49

Proof

Step Hyp Ref Expression
1 7cn 7
2 1 sqvali 7 2 = 7 7
3 7t7e49 7 7 = 49
4 2 3 eqtri 7 2 = 49