Metamath Proof Explorer

Theorem sq10e99m1

Description: The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)

Ref Expression
Assertion sq10e99m1 
|- ( ; 1 0 ^ 2 ) = ( ; 9 9 + 1 )

Proof

Step Hyp Ref Expression
1 sq10 
 |-  ( ; 1 0 ^ 2 ) = ; ; 1 0 0
2 9nn0 
 |-  9 e. NN0
3 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
4 eqid 
 |-  ; 9 9 = ; 9 9
5 2 3 4 decsucc 
 |-  ( ; 9 9 + 1 ) = ; ; 1 0 0
6 1 5 eqtr4i 
 |-  ( ; 1 0 ^ 2 ) = ( ; 9 9 + 1 )