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  9546  nn0lele2xi  9618  numltc  9811  ef01bndlem  12539  cos2bnd  12543  sin4lt0  12550  sincosq3sgn  15979  sincosq4sgn  15980  cosq23lt0  15984  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  sincos4thpi  15991  cosq34lt1  16001  cos02pilt1  16002  cos0pilt1  16003  log2ublem1  16140  log2ublem2  16141  bpos1lem  16207  taupi  17221