Theorem remulcli 8341

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

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

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

This theorem is used by:  addltmul  9547  nn0lele2xi  9619  numltc  9812  ef01bndlem  12542  cos2bnd  12546  sin4lt0  12553  sincosq3sgn  16021  sincosq4sgn  16022  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  sincos4thpi  16033  cosq34lt1  16043  cos02pilt1  16044  cos0pilt1  16045  log2ublem1  16182  log2ublem2  16183  bpos1lem  16270  bposlem7  16278  bposlem8  16279  bposlem9  16280  taupi  17290