Description: 45 squared is 2025. (Contributed by SN, 30-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sq45 | |- ( ; 4 5 ^ 2 ) = ; ; ; 2 0 2 5 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4nn0 | |- 4 e. NN0 |
|
| 2 | 5nn0 | |- 5 e. NN0 |
|
| 3 | 1 2 | deccl | |- ; 4 5 e. NN0 |
| 4 | 3 | nn0cni | |- ; 4 5 e. CC |
| 5 | 4 | sqvali | |- ( ; 4 5 ^ 2 ) = ( ; 4 5 x. ; 4 5 ) |
| 6 | 4p1e5 | |- ( 4 + 1 ) = 5 |
|
| 7 | 4t5e20 | |- ( 4 x. 5 ) = ; 2 0 |
|
| 8 | 1 6 7 | sqn5ii | |- ( ; 4 5 x. ; 4 5 ) = ; ; ; 2 0 2 5 |
| 9 | 5 8 | eqtri | |- ( ; 4 5 ^ 2 ) = ; ; ; 2 0 2 5 |