Theorem remulcli 8330

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

Syntax hints:   ∈ wcel 2209  (class class class)co 6075  ℝcr 8168   · cmul 8174

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

This theorem is referenced by:  addltmul  9521  nn0lele2xi  9593  numltc  9781  ef01bndlem  12501  cos2bnd  12505  sin4lt0  12512  sincosq3sgn  15852  sincosq4sgn  15853  cosq23lt0  15857  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  sincos4thpi  15864  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  taupi  17028