Metamath Proof Explorer


Theorem sq5

Description: The square of 5 is 25. (Contributed by SN, 26-Aug-2025)

Ref Expression
Assertion sq5 ⊢ 5 2 = 25

Proof

Step Hyp Ref Expression
1 5cn ⊢ 5 ∈ ℂ
2 1 sqvali ⊢ 5 2 = 5 ⋅ 5
3 5t5e25 ⊢ 5 ⋅ 5 = 25
4 2 3 eqtri ⊢ 5 2 = 25