Metamath Proof Explorer


Axiom ax-addcl

Description: Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by Theorem axaddcl . Proofs should normally use addcl instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-addcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cc
2 0 1 wcel 𝐴 ∈ ℂ
3 cB 𝐵
4 3 1 wcel 𝐵 ∈ ℂ
5 2 4 wa ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ )
6 caddc +
7 0 3 6 co ( 𝐴 + 𝐵 )
8 7 1 wcel ( 𝐴 + 𝐵 ) ∈ ℂ
9 5 8 wi ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )