Theorem remulcli 8057

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895   · cmul 7901

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

This theorem is referenced by:  addltmul  9245  nn0lele2xi  9317  numltc  9499  ef01bndlem  11938  cos2bnd  11942  sin4lt0  11949  sincosq3sgn  15148  sincosq4sgn  15149  cosq23lt0  15153  coseq0q4123  15154  coseq00topi  15155  coseq0negpitopi  15156  sincos4thpi  15160  cosq34lt1  15170  cos02pilt1  15171  cos0pilt1  15172  taupi  15804