Theorem remulcli 7973

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

Syntax hints:   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812   · cmul 7818

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

This theorem is referenced by:  addltmul  9157  nn0lele2xi  9229  numltc  9411  ef01bndlem  11766  cos2bnd  11770  sin4lt0  11776  sincosq3sgn  14288  sincosq4sgn  14289  cosq23lt0  14293  coseq0q4123  14294  coseq00topi  14295  coseq0negpitopi  14296  sincos4thpi  14300  cosq34lt1  14310  cos02pilt1  14311  cos0pilt1  14312  taupi  14860