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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to AB\in ℝ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℝ$$
5	2 4	wa	$$wff\left(A\in ℝ\wedge B\in ℝ\right)$$
6		cmul	$$class\times$$
7	0 3 6	co	$$classAB$$
8	7 1	wcel	$$wffAB\in ℝ$$
9	5 8	wi	$$wff\left(\left(A\in ℝ\wedge B\in ℝ\right)\to AB\in ℝ\right)$$