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 ∈ ℕ0
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 )