Theorem remulcli 8192

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030   · cmul 8036

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

This theorem is referenced by:  addltmul  9380  nn0lele2xi  9452  numltc  9635  ef01bndlem  12316  cos2bnd  12320  sin4lt0  12327  sincosq3sgn  15551  sincosq4sgn  15552  cosq23lt0  15556  coseq0q4123  15557  coseq00topi  15558  coseq0negpitopi  15559  sincos4thpi  15563  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  taupi  16677