Theorem remulcli 8001

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

Syntax hints:   ∈ wcel 2160  (class class class)co 5896  ℝcr 7840   · cmul 7846

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

This theorem is referenced by:  addltmul  9185  nn0lele2xi  9257  numltc  9439  ef01bndlem  11796  cos2bnd  11800  sin4lt0  11806  sincosq3sgn  14706  sincosq4sgn  14707  cosq23lt0  14711  coseq0q4123  14712  coseq00topi  14713  coseq0negpitopi  14714  sincos4thpi  14718  cosq34lt1  14728  cos02pilt1  14729  cos0pilt1  14730  taupi  15280