Theorem remulcli 8086

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

Syntax hints:   ∈ wcel 2176  (class class class)co 5944  ℝcr 7924   · cmul 7930

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

This theorem is referenced by:  addltmul  9274  nn0lele2xi  9346  numltc  9529  ef01bndlem  12067  cos2bnd  12071  sin4lt0  12078  sincosq3sgn  15300  sincosq4sgn  15301  cosq23lt0  15305  coseq0q4123  15306  coseq00topi  15307  coseq0negpitopi  15308  sincos4thpi  15312  cosq34lt1  15322  cos02pilt1  15323  cos0pilt1  15324  taupi  16012