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 )