Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
sq7
Next ⟩
sq8
Metamath Proof Explorer
Ascii
Unicode
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