Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
sq4
Next ⟩
sq5
Metamath Proof Explorer
Ascii
Unicode
Theorem
sq4
Description:
The square of 4 is 16.
(Contributed by
SN
, 26-Aug-2025)
Ref
Expression
Assertion
sq4
⊢
4
2
=
16
Proof
Step
Hyp
Ref
Expression
1
4cn
⊢
4
∈
ℂ
2
1
sqvali
⊢
4
2
=
4
⋅
4
3
4t4e16
⊢
4
⋅
4
=
16
4
2
3
eqtri
⊢
4
2
=
16