Description: The square of 10 is 100. (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sq10 | |- ( ; 1 0 ^ 2 ) = ; ; 1 0 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 10nn0 | |- ; 1 0 e. NN0 |
|
| 2 | 1 | nn0cni | |- ; 1 0 e. CC |
| 3 | 2 | sqvali | |- ( ; 1 0 ^ 2 ) = ( ; 1 0 x. ; 1 0 ) |
| 4 | 1 | dec0u | |- ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0 |
| 5 | 3 4 | eqtri | |- ( ; 1 0 ^ 2 ) = ; ; 1 0 0 |