Theorem remulcli 11252

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126   · cmul 11132

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11190

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ledivp1i  12167  ltdivp1i  12168  addltmul  12507  nn0lele2xi  12587  10re  12762  numltc  12770  nn0opthlem2  14336  faclbnd4lem1  14360  ef01bndlem  16275  cos2bnd  16279  sin4lt0  16286  dvdslelem  16402  divalglem1  16487  divalglem6  16491  2pire  26696  sincosq3sgn  26741  sincosq4sgn  26742  sincos4thpi  26754  cos02pilt1  26766  cosq34lt1  26767  cos0pilt1  26772  efif1olem1  26782  efif1olem2  26783  efif1olem4  26785  efif1o  26786  efifo  26787  ang180lem1  27049  ang180lem2  27050  log2ublem1  27186  log2ublem2  27187  bpos1lem  27521  bposlem7  27529  bposlem8  27530  bposlem9  27531  chebbnd1lem3  27710  chebbnd1  27711  chto1ub  27715  siilem1  31335  normlem6  31599  normlem7  31600  norm-ii-i  31621  bcsiALT  31663  nmopadjlem  32573  nmopcoi  32579  bdopcoi  32582  nmopcoadji  32585  unierri  32588  dpmul4  33362  hgt750lem  35162  hgt750lem2  35163  hgt750leme  35169  problem5  36251  circum  36256  iexpire  36317  taupi  38078  sin2h  38367  tan2h  38369  sumnnodd  46463  sinaover2ne0  46699  stirlinglem11  46915  dirkercncflem4  46937  fourierdlem24  46962  fourierdlem43  46981  fourierdlem44  46982  fourierdlem68  47005  fourierdlem94  47031  fourierdlem111  47048  sqwvfoura  47059  sqwvfourb  47060  fourierswlem  47061  fouriersw  47062  goldrarr  47749  goldratval  47757  lighneallem4a  48514  tgoldbach  48736