Theorem remulcli 7984

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

Syntax hints:   ∈ wcel 2158  (class class class)co 5888  ℝcr 7823   · cmul 7829

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

This theorem is referenced by:  addltmul  9168  nn0lele2xi  9240  numltc  9422  ef01bndlem  11777  cos2bnd  11781  sin4lt0  11787  sincosq3sgn  14489  sincosq4sgn  14490  cosq23lt0  14494  coseq0q4123  14495  coseq00topi  14496  coseq0negpitopi  14497  sincos4thpi  14501  cosq34lt1  14511  cos02pilt1  14512  cos0pilt1  14513  taupi  15062