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

Metamath Proof Explorer

Theorem axmulrcl

Description: Closure law for multiplication in the real subfield of complex numbers. Axiom 7 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-mulrcl be used later. Instead, in most cases use remulcl . (New usage is discouraged.) (Contributed by NM, 31-Mar-1996)

Ref Expression
Assertion axmulrcl 
|- ( ( A e. RR /\ B e. RR ) -> ( A x. 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 >. x. <. y , 0R >. ) = ( A x. <. y , 0R >. ) )
4 3 eleq1d 
 |-  ( <. x , 0R >. = A -> ( ( <. x , 0R >. x. <. y , 0R >. ) e. RR <-> ( A x. <. y , 0R >. ) e. RR ) )
5 oveq2 
 |-  ( <. y , 0R >. = B -> ( A x. <. y , 0R >. ) = ( A x. B ) )
6 5 eleq1d 
 |-  ( <. y , 0R >. = B -> ( ( A x. <. y , 0R >. ) e. RR <-> ( A x. B ) e. RR ) )
7 mulresr 
 |-  ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. x. <. y , 0R >. ) = <. ( x .R y ) , 0R >. )
8 mulclsr 
 |-  ( ( 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 >. x. <. y , 0R >. ) e. RR )
12 1 2 4 6 11 2gencl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )