Theorem remulcli 7773

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

Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612   · cmul 7618

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

This theorem is referenced by:  addltmul  8949  nn0lele2xi  9021  numltc  9200  ef01bndlem  11452  cos2bnd  11456  sin4lt0  11462  sincosq3sgn  12898  sincosq4sgn  12899  cosq23lt0  12903  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  sincos4thpi  12910  cosq34lt1  12920  cos02pilt1  12921  taupi  13228