This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 9m1e8

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

Ref Expression
Assertion 9m1e8 ( 9 − 1 ) = 8

Proof

Step Hyp Ref Expression
1 8cn ⊢ 8 ∈ ℂ
2 ax-1cn ⊢ 1 ∈ ℂ
3 df-9 ⊢ 9 = ( 8 + 1 )
4 1 2 3 mvrraddi ⊢ ( 9 − 1 ) = 8