Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Subtraction
subcld
Next ⟩
pncand
Metamath Proof Explorer
Ascii
Unicode
Theorem
subcld
Description:
Closure law for subtraction.
(Contributed by
Mario Carneiro
, 27-May-2016)
Ref
Expression
Hypotheses
negidd.1
⊢
φ
→
A
∈
ℂ
pncand.2
⊢
φ
→
B
∈
ℂ
Assertion
subcld
⊢
φ
→
A
−
B
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
negidd.1
⊢
φ
→
A
∈
ℂ
2
pncand.2
⊢
φ
→
B
∈
ℂ
3
subcl
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
A
−
B
∈
ℂ
4
1
2
3
syl2anc
⊢
φ
→
A
−
B
∈
ℂ