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