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

Theorem rpdivcld 11874
Description: Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
rpaddcld.1 (𝜑𝐵 ∈ ℝ+)
Assertion
Ref Expression
rpdivcld (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Proof of Theorem rpdivcld
StepHypRef Expression
1 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
2 rpaddcld.1 . 2 (𝜑𝐵 ∈ ℝ+)
3 rpdivcl 11841 . 2 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
41, 2, 3syl2anc 692 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  (class class class)co 6635   / cdiv 10669  +crp 11817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-rp 11818
This theorem is referenced by:  bcpasc  13091  mulcn2  14307  o1rlimmul  14330  mertenslem1  14597  mertenslem2  14598  effsumlt  14822  prmind2  15379  nlmvscnlem2  22470  nlmvscnlem1  22471  nghmcn  22530  lebnumlem3  22743  lebnumii  22746  nmoleub3  22900  ipcnlem2  23024  ipcnlem1  23025  equivcfil  23078  equivcau  23079  ovollb2lem  23237  ovoliunlem1  23251  uniioombllem6  23337  itg2const2  23489  itg2cnlem2  23510  aalioulem2  24069  aalioulem4  24071  aalioulem5  24072  aalioulem6  24073  aaliou  24074  aaliou2b  24077  aaliou3lem9  24086  itgulm  24143  abelthlem7  24173  abelthlem8  24174  tanrpcl  24237  logdivlti  24347  logcnlem2  24370  ang180lem2  24521  isosctrlem2  24530  birthdaylem2  24660  cxp2limlem  24683  cxp2lim  24684  cxploglim  24685  cxploglim2  24686  amgmlem  24697  logdiflbnd  24702  emcllem2  24704  fsumharmonic  24719  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem4  24739  lgamgulmlem5  24740  lgamgulmlem6  24741  lgamgulm2  24743  lgamucov  24745  lgamcvg2  24762  gamcvg  24763  gamcvg2lem  24766  regamcl  24768  relgamcl  24769  lgam1  24771  ftalem4  24783  chpval2  24924  chpchtsum  24925  logfacrlim  24930  logexprlim  24931  bclbnd  24986  bposlem1  24990  bposlem2  24991  lgsquadlem2  25087  chebbnd1lem1  25139  chebbnd1lem3  25141  chebbnd1  25142  chtppilimlem2  25144  chebbnd2  25147  chto1lb  25148  rplogsumlem2  25155  rpvmasumlem  25157  dchrvmasumlem1  25165  dchrvmasum2if  25167  dchrisum0lem1b  25185  dchrisum0lem2a  25187  vmalogdivsum2  25208  2vmadivsumlem  25210  selberglem3  25217  selberg  25218  selberg4lem1  25230  selberg3r  25239  selberg4r  25240  selberg34r  25241  pntrlog2bndlem1  25247  pntrlog2bndlem2  25248  pntrlog2bndlem3  25249  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  pntrlog2bndlem6a  25252  pntrlog2bndlem6  25253  pntrlog2bnd  25254  pntpbnd1a  25255  pntpbnd1  25256  pntpbnd2  25257  pntibndlem2  25261  pntibndlem3  25262  pntlemd  25264  pntlemc  25265  pntlema  25266  pntlemb  25267  pntlemg  25268  pntlemn  25270  pntlemq  25271  pntlemr  25272  pntlemj  25273  pntlemf  25275  pntlemo  25277  pnt2  25283  pnt  25284  ostth2lem3  25305  ostth2  25307  blocni  27630  ubthlem2  27697  lnconi  28862  rpxdivcld  29616  omssubadd  30336  hgt750leme  30710  faclimlem1  31604  faclimlem3  31606  faclim  31607  iprodfac  31608  equivtotbnd  33548  rrncmslem  33602  rrnequiv  33605  irrapxlem5  37209  xralrple2  39383  xralrple3  39403  iooiinicc  39572  iooiinioc  39586  limclner  39683  fprodsubrecnncnvlem  39884  fprodaddrecnncnvlem  39886  stoweidlem31  40011  stoweidlem59  40039  wallispilem3  40047  wallispilem4  40048  wallispilem5  40049  wallispi  40050  wallispi2lem1  40051  stirlinglem2  40055  stirlinglem4  40057  stirlinglem8  40061  stirlinglem13  40066  stirlinglem15  40068  stirlingr  40070  fourierdlem30  40117  fourierdlem73  40159  fourierdlem87  40173  qndenserrnbllem  40277  ovnsubaddlem1  40547  ovnsubaddlem2  40548  hoiqssbllem1  40599  hoiqssbllem2  40600  hoiqssbllem3  40601  ovolval5lem1  40629  ovolval5lem2  40630  vonioolem1  40657  smfmullem1  40761  smfmullem2  40762  smfmullem3  40763
  Copyright terms: Public domain W3C validator