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 · ; 1 1 ) = ; 9 9

Proof

Step	Hyp	Ref	Expression
1		9nn0	⊢ 9 ∈ ℕ0
2	1	11multnc	⊢ ( 9 · ; 1 1 ) = ; 9 9