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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elreal	⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
2		elreal	⊢ ( 𝐵 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐵 )
3		oveq1	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) )
4	3	eleq1d	⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ↔ ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ) )
5		oveq2	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) = ( 𝐴 · 𝐵 ) )
6	5	eleq1d	⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 · ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ ↔ ( 𝐴 · 𝐵 ) ∈ ℝ ) )
7		mulresr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) = ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ )
8		mulclsr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( 𝑥 ·R 𝑦 ) ∈ R )
9		opelreal	⊢ ( ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ ∈ ℝ ↔ ( 𝑥 ·R 𝑦 ) ∈ R )
10	8 9	sylibr	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ⟨ ( 𝑥 ·R 𝑦 ) , 0R ⟩ ∈ ℝ )
11	7 10	eqeltrd	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 𝑦 , 0R ⟩ ) ∈ ℝ )
12	1 2 4 6 11	2gencl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )