Metamath Proof Explorer


Theorem 6m1e5

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

Ref Expression
Assertion 6m1e5 ( 6 − 1 ) = 5

Proof

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