Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
5m1e4
Next ⟩
6m1e5
Metamath Proof Explorer
Ascii
Structured
Theorem
5m1e4
Description:
5 - 1 = 4.
(Contributed by
AV
, 6-Sep-2021)
Ref
Expression
Assertion
5m1e4
⊢
( 5 − 1 ) = 4
Proof
Step
Hyp
Ref
Expression
1
4cn
⊢
4 ∈ ℂ
2
ax-1cn
⊢
1 ∈ ℂ
3
df-5
⊢
5 = ( 4 + 1 )
4
1
2
3
mvrraddi
⊢
( 5 − 1 ) = 4