Theorem remulcli 7780

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
remulcli	⊢ (𝐴 · 𝐵) ∈ ℝ

Proof of Theorem remulcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		remulcl 7748	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 422	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5774  ℝcr 7619   · cmul 7625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7719

This theorem is referenced by:  addltmul  8956  nn0lele2xi  9028  numltc  9207  ef01bndlem  11463  cos2bnd  11467  sin4lt0  11473  sincosq3sgn  12909  sincosq4sgn  12910  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  sincos4thpi  12921  cosq34lt1  12931  cos02pilt1  12932  taupi  13239