Theorem remulcli 8183

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021   · cmul 8027

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

This theorem is referenced by:  addltmul  9371  nn0lele2xi  9443  numltc  9626  ef01bndlem  12307  cos2bnd  12311  sin4lt0  12318  sincosq3sgn  15542  sincosq4sgn  15543  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  sincos4thpi  15554  cosq34lt1  15564  cos02pilt1  15565  cos0pilt1  15566  taupi  16613