Theorem axaddrcl

Description: Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl be used later. Instead, in most cases use readdcl . (Contributed by NM, 31-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axaddrcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		elreal	|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
2		elreal	|- ( B e. RR <-> E. y e. R. <. y , 0R >. = B )
3		oveq1	|- ( <. x , 0R >. = A -> ( <. x , 0R >. + <. y , 0R >. ) = ( A + <. y , 0R >. ) )
4	3	eleq1d	|- ( <. x , 0R >. = A -> ( ( <. x , 0R >. + <. y , 0R >. ) e. RR <-> ( A + <. y , 0R >. ) e. RR ) )
5		oveq2	|- ( <. y , 0R >. = B -> ( A + <. y , 0R >. ) = ( A + B ) )
6	5	eleq1d	|- ( <. y , 0R >. = B -> ( ( A + <. y , 0R >. ) e. RR <-> ( A + B ) e. RR ) )
7		addresr	|- ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. + <. y , 0R >. ) = <. ( x +R y ) , 0R >. )
8		addclsr	|- ( ( x e. R. /\ y e. R. ) -> ( x +R y ) e. R. )
9		opelreal	|- ( <. ( x +R y ) , 0R >. e. RR <-> ( x +R y ) e. R. )
10	8 9	sylibr	|- ( ( x e. R. /\ y e. R. ) -> <. ( x +R y ) , 0R >. e. RR )
11	7 10	eqeltrd	|- ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. + <. y , 0R >. ) e. RR )
12	1 2 4 6 11	2gencl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )