Theorem remulcli 8340

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8278

This theorem is used by:  addltmul  9542  nn0lele2xi  9614  numltc  9802  ef01bndlem  12523  cos2bnd  12527  sin4lt0  12534  sincosq3sgn  15929  sincosq4sgn  15930  cosq23lt0  15934  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  sincos4thpi  15941  cosq34lt1  15951  cos02pilt1  15952  cos0pilt1  15953  log2ublem1  16083  log2ublem2  16084  taupi  17123