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  9818  ef01bndlem  12548  cos2bnd  12552  sin4lt0  12559  sincosq3sgn  16055  sincosq4sgn  16056  cosq23lt0  16060  coseq0q4123  16061  coseq00topi  16062  coseq0negpitopi  16063  sincos4thpi  16067  cosq34lt1  16078  cos02pilt1  16079  cos0pilt1  16080  log2ublem1  16221  log2ublem2  16222  bpos1lem  16309  bposlem7  16317  bposlem8  16318  bposlem9  16319  taupi  17330