Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
sq9
Next ⟩
235t711
Metamath Proof Explorer
Ascii
Unicode
Theorem
sq9
Description:
The square of 9 is 81.
(Contributed by
SN
, 30-Mar-2025)
Ref
Expression
Assertion
sq9
⊢
9
2
=
81
Proof
Step
Hyp
Ref
Expression
1
9cn
⊢
9
∈
ℂ
2
1
sqvali
⊢
9
2
=
9
⋅
9
3
9t9e81
⊢
9
⋅
9
=
81
4
2
3
eqtri
⊢
9
2
=
81