Theorem remulcli 8346

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

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

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

This theorem is used by:  addltmul  9553  nn0lele2xi  9625  numltc  9817  ef01bndlem  12547  cos2bnd  12551  sin4lt0  12558  sincosq3sgn  16072  sincosq4sgn  16073  cosq23lt0  16077  coseq0q4123  16078  coseq00topi  16079  coseq0negpitopi  16080  sincos4thpi  16084  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  log2ublem1  16238  log2ublem2  16239  bpos1lem  16326  bposlem7  16334  bposlem8  16335  bposlem9  16336  taupi  17347