Theorem 9t11e99

Description: 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021) (Revised by AV, 6-Sep-2021) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	9t11e99	|- ( 9 x. ; 1 1 ) = ; 9 9

Proof

Step	Hyp	Ref	Expression
1		9nn0	|- 9 e. NN0
2	1	11multnc	|- ( 9 x. ; 1 1 ) = ; 9 9