Axiom ax-mulrcl 7347

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

Assertion

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

Detailed syntax breakdown of Axiom ax-mulrcl

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cr 7252	. . . 4 class RR
3	1, 2	wcel 1434	. . 3 wff A e. RR
4		cB	. . . 4 class B
5	4, 2	wcel 1434	. . 3 wff B e. RR
6	3, 5	wa 102	. 2 wff ( A e. RR /\ B e. RR )
7		cmul 7258	. . . 4 class x.
8	1, 4, 7	co 5591	. . 3 class ( A x. B )
9	8, 2	wcel 1434	. 2 wff ( A x. B ) e. RR
10	6, 9	wi 4	1 wff ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

This axiom is referenced by:  remulcl  7373