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  16029  sincosq4sgn  16030  cosq23lt0  16034  coseq0q4123  16035  coseq00topi  16036  coseq0negpitopi  16037  sincos4thpi  16041  cosq34lt1  16052  cos02pilt1  16053  cos0pilt1  16054  log2ublem1  16195  log2ublem2  16196  bpos1lem  16283  bposlem7  16291  bposlem8  16292  bposlem9  16293  taupi  17303