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

Metamath Proof Explorer

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 )