Theorem remulcli 8035

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

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873   · cmul 7879

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

This theorem is referenced by:  addltmul  9222  nn0lele2xi  9294  numltc  9476  ef01bndlem  11902  cos2bnd  11906  sin4lt0  11913  sincosq3sgn  14995  sincosq4sgn  14996  cosq23lt0  15000  coseq0q4123  15001  coseq00topi  15002  coseq0negpitopi  15003  sincos4thpi  15007  cosq34lt1  15017  cos02pilt1  15018  cos0pilt1  15019  taupi  15623