Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sq3
Next ⟩
sq4e2t8
Metamath Proof Explorer
Ascii
Unicode
Theorem
sq3
Description:
The square of 3 is 9.
(Contributed by
NM
, 26-Apr-2006)
Ref
Expression
Assertion
sq3
⊢
3
2
=
9
Proof
Step
Hyp
Ref
Expression
1
3cn
⊢
3
∈
ℂ
2
1
sqvali
⊢
3
2
=
3
⋅
3
3
3t3e9
⊢
3
⋅
3
=
9
4
2
3
eqtri
⊢
3
2
=
9