Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
0m0e0
Next ⟩
1m0e1
Metamath Proof Explorer
Ascii
Structured
Theorem
0m0e0
Description:
0 minus 0 equals 0.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
0m0e0
⊢
( 0 − 0 ) = 0
Proof
Step
Hyp
Ref
Expression
1
0cn
⊢
0 ∈ ℂ
2
1
subidi
⊢
( 0 − 0 ) = 0