Theorem remulcli 11225

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

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11099   · cmul 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11163

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  ledivp1i  12140  ltdivp1i  12141  addltmul  12480  nn0lele2xi  12560  10re  12734  numltc  12742  nn0opthlem2  14305  faclbnd4lem1  14329  ef01bndlem  16240  cos2bnd  16244  sin4lt0  16251  dvdslelem  16367  divalglem1  16452  divalglem6  16456  2pire  26586  sincosq3sgn  26631  sincosq4sgn  26632  sincos4thpi  26644  cos02pilt1  26657  cosq34lt1  26658  cos0pilt1  26663  efif1olem1  26673  efif1olem2  26674  efif1olem4  26676  efif1o  26677  efifo  26678  ang180lem1  26940  ang180lem2  26941  log2ublem1  27077  log2ublem2  27078  bpos1lem  27412  bposlem7  27420  bposlem8  27421  bposlem9  27422  chebbnd1lem3  27601  chebbnd1  27602  chto1ub  27606  siilem1  31144  normlem6  31408  normlem7  31409  norm-ii-i  31430  bcsiALT  31472  nmopadjlem  32382  nmopcoi  32388  bdopcoi  32391  nmopcoadji  32394  unierri  32397  dpmul4  33174  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  problem5  36094  circum  36099  iexpire  36160  taupi  37889  sin2h  38183  tan2h  38185  sumnnodd  46272  sinaover2ne0  46508  stirlinglem11  46724  dirkercncflem4  46746  fourierdlem24  46771  fourierdlem43  46790  fourierdlem44  46791  fourierdlem68  46814  fourierdlem94  46840  fourierdlem111  46857  sqwvfoura  46868  sqwvfourb  46869  fourierswlem  46870  fouriersw  46871  goldrarr  47541  lighneallem4a  48283  tgoldbach  48505