Theorem 10m1e9

Description: 10 - 1 = 9. (Contributed by AV, 6-Sep-2021)

	Ref	Expression
Assertion	10m1e9	⊢ ( ; 1 0 − 1 ) = 9

Proof

Step	Hyp	Ref	Expression
1		9cn	⊢ 9 ∈ ℂ
2		ax-1cn	⊢ 1 ∈ ℂ
3		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
4	3	eqcomi	⊢ ; 1 0 = ( 9 + 1 )
5	1 2 4	mvrraddi	⊢ ( ; 1 0 − 1 ) = 9