Theorem remulcli 7913

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

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752   · cmul 7758

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

This theorem is referenced by:  addltmul  9093  nn0lele2xi  9165  numltc  9347  ef01bndlem  11697  cos2bnd  11701  sin4lt0  11707  sincosq3sgn  13389  sincosq4sgn  13390  cosq23lt0  13394  coseq0q4123  13395  coseq00topi  13396  coseq0negpitopi  13397  sincos4thpi  13401  cosq34lt1  13411  cos02pilt1  13412  cos0pilt1  13413  taupi  13949