Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
6m1e5
Next ⟩
7m1e6
Metamath Proof Explorer
Ascii
Structured
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