Metamath Proof Explorer


Theorem sq5

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

Ref Expression
Assertion sq5 ( 5 ↑ 2 ) = 2 5

Proof

Step Hyp Ref Expression
1 5cn 5 ∈ ℂ
2 1 sqvali ( 5 ↑ 2 ) = ( 5 · 5 )
3 5t5e25 ( 5 · 5 ) = 2 5
4 2 3 eqtri ( 5 ↑ 2 ) = 2 5