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