Theorem remulcli 8288

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

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126   · cmul 8132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8226

This theorem is referenced by:  addltmul  9475  nn0lele2xi  9547  numltc  9734  ef01bndlem  12442  cos2bnd  12446  sin4lt0  12453  sincosq3sgn  15693  sincosq4sgn  15694  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  sincos4thpi  15705  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  taupi  16859