Theorem remulcli 7804

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

Syntax hints:   ∈ wcel 1481  (class class class)co 5782  ℝcr 7643   · cmul 7649

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

This theorem is referenced by:  addltmul  8980  nn0lele2xi  9052  numltc  9231  ef01bndlem  11499  cos2bnd  11503  sin4lt0  11509  sincosq3sgn  12957  sincosq4sgn  12958  cosq23lt0  12962  coseq0q4123  12963  coseq00topi  12964  coseq0negpitopi  12965  sincos4thpi  12969  cosq34lt1  12979  cos02pilt1  12980  cos0pilt1  12981  taupi  13430