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

Theorem rpdivcld 12087
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 12054 . 2 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
41, 2, 3syl2anc 579 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  (class class class)co 6842   / cdiv 10938  +crp 12028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-rp 12029
This theorem is referenced by:  bcpasc  13312  mulcn2  14611  o1rlimmul  14634  mertenslem1  14899  mertenslem2  14900  effsumlt  15123  prmind2  15678  nlmvscnlem2  22768  nlmvscnlem1  22769  nghmcn  22828  lebnumlem3  23041  lebnumii  23044  nmoleub3  23197  ipcnlem2  23321  ipcnlem1  23322  equivcfil  23376  equivcau  23377  ovollb2lem  23546  ovoliunlem1  23560  uniioombllem6  23646  itg2const2  23799  itg2cnlem2  23820  aalioulem2  24379  aalioulem4  24381  aalioulem5  24382  aalioulem6  24383  aaliou  24384  aaliou2b  24387  aaliou3lem9  24396  itgulm  24453  abelthlem7  24483  abelthlem8  24484  tanrpcl  24548  logdivlti  24657  logcnlem2  24680  ang180lem2  24831  isosctrlem2  24840  birthdaylem2  24970  cxp2limlem  24993  cxp2lim  24994  cxploglim  24995  cxploglim2  24996  amgmlem  25007  logdiflbnd  25012  emcllem2  25014  fsumharmonic  25029  lgamgulmlem2  25047  lgamgulmlem3  25048  lgamgulmlem4  25049  lgamgulmlem5  25050  lgamgulmlem6  25051  lgamgulm2  25053  lgamucov  25055  lgamcvg2  25072  gamcvg  25073  gamcvg2lem  25076  regamcl  25078  relgamcl  25079  lgam1  25081  ftalem4  25093  chpval2  25234  chpchtsum  25235  logfacrlim  25240  logexprlim  25241  bclbnd  25296  bposlem1  25300  bposlem2  25301  lgsquadlem2  25397  chebbnd1lem1  25449  chebbnd1lem3  25451  chebbnd1  25452  chtppilimlem2  25454  chebbnd2  25457  chto1lb  25458  rplogsumlem2  25465  rpvmasumlem  25467  dchrvmasumlem1  25475  dchrvmasum2if  25477  dchrisum0lem1b  25495  dchrisum0lem2a  25497  vmalogdivsum2  25518  2vmadivsumlem  25520  selberglem3  25527  selberg  25528  selberg4lem1  25540  selberg3r  25549  selberg4r  25550  selberg34r  25551  pntrlog2bndlem1  25557  pntrlog2bndlem2  25558  pntrlog2bndlem3  25559  pntrlog2bndlem4  25560  pntrlog2bndlem5  25561  pntrlog2bndlem6a  25562  pntrlog2bndlem6  25563  pntrlog2bnd  25564  pntpbnd1a  25565  pntpbnd1  25566  pntpbnd2  25567  pntibndlem2  25571  pntibndlem3  25572  pntlemd  25574  pntlemc  25575  pntlema  25576  pntlemb  25577  pntlemg  25578  pntlemn  25580  pntlemq  25581  pntlemr  25582  pntlemj  25583  pntlemf  25585  pntlemo  25587  pnt2  25593  pnt  25594  ostth2lem3  25615  ostth2  25617  blocni  28116  ubthlem2  28183  lnconi  29348  rpxdivcld  30089  omssubadd  30809  hgt750leme  31187  faclimlem1  32074  faclimlem3  32076  faclim  32077  iprodfac  32078  equivtotbnd  33999  rrncmslem  34053  rrnequiv  34056  irrapxlem5  38068  xralrple2  40208  xralrple3  40228  iooiinicc  40407  iooiinioc  40421  limclner  40521  fprodsubrecnncnvlem  40759  fprodaddrecnncnvlem  40761  stoweidlem31  40885  stoweidlem59  40913  wallispilem3  40921  wallispilem4  40922  wallispilem5  40923  wallispi  40924  wallispi2lem1  40925  stirlinglem2  40929  stirlinglem4  40931  stirlinglem8  40935  stirlinglem13  40940  stirlinglem15  40942  stirlingr  40944  fourierdlem30  40991  fourierdlem73  41033  fourierdlem87  41047  qndenserrnbllem  41151  ovnsubaddlem1  41424  ovnsubaddlem2  41425  hoiqssbllem1  41476  hoiqssbllem2  41477  hoiqssbllem3  41478  ovolval5lem1  41506  ovolval5lem2  41507  vonioolem1  41534  smfmullem1  41638  smfmullem2  41639  smfmullem3  41640
  Copyright terms: Public domain W3C validator