MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  remulcli Structured version   Visualization version   GIF version

Theorem remulcli 9933
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
StepHypRef Expression
1 recni.1 . 2 𝐴 ∈ ℝ
2 axri.2 . 2 𝐵 ∈ ℝ
3 remulcl 9900 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 704 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  (class class class)co 6549  cr 9814   · cmul 9820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9878
This theorem depends on definitions:  df-bi 196  df-an 385
This theorem is referenced by:  ledivp1i  10828  ltdivp1i  10829  addltmul  11145  nn0lele2xi  11225  numltc  11404  decleOLD  11419  nn0opthlem2  12918  faclbnd4lem1  12942  ef01bndlem  14753  cos2bnd  14757  sin4lt0  14764  dvdslelem  14869  divalglem1  14955  divalglem6  14959  sincosq3sgn  24056  sincosq4sgn  24057  sincos4thpi  24069  efif1olem1  24092  efif1olem2  24093  efif1olem4  24095  efif1o  24096  efifo  24097  ang180lem1  24339  ang180lem2  24340  log2ublem1  24473  log2ublem2  24474  bpos1lem  24807  bposlem7  24815  bposlem8  24816  bposlem9  24817  chebbnd1lem3  24960  chebbnd1  24961  chto1ub  24965  siilem1  27090  normlem6  27356  normlem7  27357  norm-ii-i  27378  bcsiALT  27420  nmopadjlem  28332  nmopcoi  28338  bdopcoi  28341  nmopcoadji  28344  unierri  28347  problem5  30817  circum  30822  iexpire  30874  taupi  32346  sin2h  32569  tan2h  32571  sumnnodd  38697  sinaover2ne0  38751  stirlinglem11  38977  dirkerper  38989  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem24  39024  fourierdlem43  39043  fourierdlem44  39044  fourierdlem68  39067  fourierdlem94  39093  fourierdlem111  39110  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  lighneallem4a  40063  tgoldbach  40232  tgoldbachOLD  40239
  Copyright terms: Public domain W3C validator