Theorem remulcli 8121

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

Syntax hints:   ∈ wcel 2178  (class class class)co 5967  ℝcr 7959   · cmul 7965

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

This theorem is referenced by:  addltmul  9309  nn0lele2xi  9381  numltc  9564  ef01bndlem  12182  cos2bnd  12186  sin4lt0  12193  sincosq3sgn  15415  sincosq4sgn  15416  cosq23lt0  15420  coseq0q4123  15421  coseq00topi  15422  coseq0negpitopi  15423  sincos4thpi  15427  cosq34lt1  15437  cos02pilt1  15438  cos0pilt1  15439  taupi  16214