Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
addcli
Next ⟩
mulcli
Metamath Proof Explorer
Ascii
Unicode
Theorem
addcli
Description:
Closure law for addition.
(Contributed by
NM
, 23-Nov-1994)
Ref
Expression
Hypotheses
axi.1
⊢
A
∈
ℂ
axi.2
⊢
B
∈
ℂ
Assertion
addcli
⊢
A
+
B
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
axi.1
⊢
A
∈
ℂ
2
axi.2
⊢
B
∈
ℂ
3
addcl
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
A
+
B
∈
ℂ
4
1
2
3
mp2an
⊢
A
+
B
∈
ℂ