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

Proof

Step	Hyp	Ref	Expression
1		elreal	$$⊢A\in ℝ\leftrightarrow \exists x\in 𝑹⟨x,0_{𝑹}⟩=A$$
2		elreal	$$⊢B\in ℝ\leftrightarrow \exists y\in 𝑹⟨y,0_{𝑹}⟩=B$$
3		oveq1	$$⊢⟨x,0_{𝑹}⟩=A\to ⟨x,0_{𝑹}⟩⟨y,0_{𝑹}⟩=A⟨y,0_{𝑹}⟩$$
4	3	eleq1d	$$⊢⟨x,0_{𝑹}⟩=A\to \left(⟨x,0_{𝑹}⟩⟨y,0_{𝑹}⟩\in ℝ\leftrightarrow A⟨y,0_{𝑹}⟩\in ℝ\right)$$
5		oveq2	$$⊢⟨y,0_{𝑹}⟩=B\to A⟨y,0_{𝑹}⟩=AB$$
6	5	eleq1d	$$⊢⟨y,0_{𝑹}⟩=B\to \left(A⟨y,0_{𝑹}⟩\in ℝ\leftrightarrow AB\in ℝ\right)$$
7		mulresr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x,0_{𝑹}⟩⟨y,0_{𝑹}⟩=⟨x{\cdot }_{𝑹}y,0_{𝑹}⟩$$
8		mulclsr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to x{\cdot }_{𝑹}y\in 𝑹$$
9		opelreal	$$⊢⟨x{\cdot }_{𝑹}y,0_{𝑹}⟩\in ℝ\leftrightarrow x{\cdot }_{𝑹}y\in 𝑹$$
10	8 9	sylibr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x{\cdot }_{𝑹}y,0_{𝑹}⟩\in ℝ$$
11	7 10	eqeltrd	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to ⟨x,0_{𝑹}⟩⟨y,0_{𝑹}⟩\in ℝ$$
12	1 2 4 6 11	2gencl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to AB\in ℝ$$