Metamath Proof Explorer


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