Theorem remulcli 8171

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009   · cmul 8015

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

This theorem is referenced by:  addltmul  9359  nn0lele2xi  9431  numltc  9614  ef01bndlem  12282  cos2bnd  12286  sin4lt0  12293  sincosq3sgn  15517  sincosq4sgn  15518  cosq23lt0  15522  coseq0q4123  15523  coseq00topi  15524  coseq0negpitopi  15525  sincos4thpi  15529  cosq34lt1  15539  cos02pilt1  15540  cos0pilt1  15541  taupi  16501