Theorem remulcli 8019

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

Syntax hints:   ∈ wcel 2160  (class class class)co 5906  ℝcr 7857   · cmul 7863

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

This theorem is referenced by:  addltmul  9205  nn0lele2xi  9277  numltc  9459  ef01bndlem  11873  cos2bnd  11877  sin4lt0  11884  sincosq3sgn  14891  sincosq4sgn  14892  cosq23lt0  14896  coseq0q4123  14897  coseq00topi  14898  coseq0negpitopi  14899  sincos4thpi  14903  cosq34lt1  14913  cos02pilt1  14914  cos0pilt1  14915  taupi  15487