Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Exemplar theorems
sq45
Next ⟩
sum9cubes
Metamath Proof Explorer
Ascii
Unicode
Theorem
sq45
Description:
45 squared is 2025.
(Contributed by
SN
, 30-Mar-2025)
Ref
Expression
Assertion
sq45
⊢
45
2
=
2025
Proof
Step
Hyp
Ref
Expression
1
4nn0
⊢
4
∈
ℕ
0
2
5nn0
⊢
5
∈
ℕ
0
3
1
2
deccl
⊢
45
∈
ℕ
0
4
3
nn0cni
⊢
45
∈
ℂ
5
4
sqvali
⊢
45
2
=
45
⋅
45
6
4p1e5
⊢
4
+
1
=
5
7
4t5e20
⊢
4
⋅
5
=
20
8
1
6
7
sqn5ii
⊢
45
⋅
45
=
2025
9
5
8
eqtri
⊢
45
2
=
2025