Theorem remulcli 7989

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 7957	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 426	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2160  (class class class)co 5891  ℝcr 7828   · cmul 7834

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

This theorem is referenced by:  addltmul  9173  nn0lele2xi  9245  numltc  9427  ef01bndlem  11782  cos2bnd  11786  sin4lt0  11792  sincosq3sgn  14646  sincosq4sgn  14647  cosq23lt0  14651  coseq0q4123  14652  coseq00topi  14653  coseq0negpitopi  14654  sincos4thpi  14658  cosq34lt1  14668  cos02pilt1  14669  cos0pilt1  14670  taupi  15219