This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cc 
 |-  CC
2 0 1 wcel 
 |-  A e. CC
3 cB 
 |-  B
4 3 1 wcel 
 |-  B e. CC
5 2 4 wa 
 |-  ( A e. CC /\ B e. CC )
6 caddc 
 |-  +
7 0 3 6 co 
 |-  ( A + B )
8 7 1 wcel 
 |-  ( A + B ) e. CC
9 5 8 wi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )