Theorem remulcli 8304

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

Syntax hints:   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142   · cmul 8148

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

This theorem is referenced by:  addltmul  9492  nn0lele2xi  9564  numltc  9752  ef01bndlem  12467  cos2bnd  12471  sin4lt0  12478  sincosq3sgn  15819  sincosq4sgn  15820  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  sincos4thpi  15831  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  taupi  16985