Theorem remulcli 8156

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994   · cmul 8000

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

This theorem is referenced by:  addltmul  9344  nn0lele2xi  9416  numltc  9599  ef01bndlem  12262  cos2bnd  12266  sin4lt0  12273  sincosq3sgn  15496  sincosq4sgn  15497  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  sincos4thpi  15508  cosq34lt1  15518  cos02pilt1  15519  cos0pilt1  15520  taupi  16400