Metamath Proof Explorer


Axiom ax-mulrcl

Description: Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by Theorem axmulrcl . Proofs should normally use remulcl instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-mulrcl
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wcel
 |-  A e. RR
3 cB
 |-  B
4 3 1 wcel
 |-  B e. RR
5 2 4 wa
 |-  ( A e. RR /\ B e. RR )
6 cmul
 |-  x.
7 0 3 6 co
 |-  ( A x. B )
8 7 1 wcel
 |-  ( A x. B ) e. RR
9 5 8 wi
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )