Theorem remulcli 8040

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878   · cmul 7884

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

This theorem is referenced by:  addltmul  9228  nn0lele2xi  9300  numltc  9482  ef01bndlem  11921  cos2bnd  11925  sin4lt0  11932  sincosq3sgn  15064  sincosq4sgn  15065  cosq23lt0  15069  coseq0q4123  15070  coseq00topi  15071  coseq0negpitopi  15072  sincos4thpi  15076  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  taupi  15717