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

Theorem rpdivcld 11365
Description: Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
rpaddcld.1  |-  ( ph  ->  B  e.  RR+ )
Assertion
Ref Expression
rpdivcld  |-  ( ph  ->  ( A  /  B
)  e.  RR+ )

Proof of Theorem rpdivcld
StepHypRef Expression
1 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
2 rpaddcld.1 . 2  |-  ( ph  ->  B  e.  RR+ )
3 rpdivcl 11332 . 2  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  ( A  /  B )  e.  RR+ )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  ( A  /  B
)  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1889  (class class class)co 6295    / cdiv 10276   RR+crp 11309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-po 4758  df-so 4759  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-rp 11310
This theorem is referenced by:  bcpasc  12513  mulcn2  13671  o1rlimmul  13694  mertenslem1  13952  mertenslem2  13953  effsumlt  14177  prmind2  14647  nlmvscnlem2  21700  nlmvscnlem1  21701  nghmcn  21778  lebnumlem3  22003  lebnumlem3OLD  22006  lebnumii  22009  nmoleub3  22145  ipcnlem2  22227  ipcnlem1  22228  equivcfil  22281  equivcau  22282  ovollb2lem  22453  ovoliunlem1  22467  uniioombllem6  22558  itg2const2  22711  itg2cnlem2  22732  aalioulem2  23301  aalioulem4  23303  aalioulem5  23304  aalioulem6  23305  aaliou  23306  aaliou2b  23309  aaliou3lem9  23318  itgulm  23375  abelthlem7  23405  abelthlem8  23406  tanrpcl  23471  logdivlti  23581  logcnlem2  23600  ang180lem2  23751  isosctrlem2  23760  birthdaylem2  23890  cxp2limlem  23913  cxp2lim  23914  cxploglim  23915  cxploglim2  23916  amgmlem  23927  logdiflbnd  23932  emcllem2  23934  fsumharmonic  23949  lgamgulmlem2  23967  lgamgulmlem3  23968  lgamgulmlem4  23969  lgamgulmlem5  23970  lgamgulmlem6  23971  lgamgulm2  23973  lgamucov  23975  lgamcvg2  23992  gamcvg  23993  gamcvg2lem  23996  regamcl  23998  relgamcl  23999  lgam1  24001  ftalem4  24012  ftalem4OLD  24014  chpval2  24158  chpchtsum  24159  logfacrlim  24164  logexprlim  24165  bclbnd  24220  bposlem1  24224  bposlem2  24225  lgsquadlem2  24295  chebbnd1lem1  24319  chebbnd1lem3  24321  chebbnd1  24322  chtppilimlem2  24324  chebbnd2  24327  chto1lb  24328  rplogsumlem2  24335  rpvmasumlem  24337  dchrvmasumlem1  24345  dchrvmasum2if  24347  dchrisum0lem1b  24365  dchrisum0lem2a  24367  vmalogdivsum2  24388  2vmadivsumlem  24390  selberglem3  24397  selberg  24398  selberg4lem1  24410  selberg3r  24419  selberg4r  24420  selberg34r  24421  pntrlog2bndlem1  24427  pntrlog2bndlem2  24428  pntrlog2bndlem3  24429  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  pntrlog2bndlem6a  24432  pntrlog2bndlem6  24433  pntrlog2bnd  24434  pntpbnd1a  24435  pntpbnd1  24436  pntpbnd2  24437  pntibndlem2  24441  pntibndlem3  24442  pntlemd  24444  pntlemc  24445  pntlema  24446  pntlemb  24447  pntlemg  24448  pntlemn  24450  pntlemq  24451  pntlemr  24452  pntlemj  24453  pntlemf  24455  pntlemo  24457  pnt2  24463  pnt  24464  ostth2lem3  24485  ostth2  24487  blocni  26458  ubthlem2  26525  lnconi  27698  rpxdivcld  28415  omssubadd  29140  omssubaddOLD  29144  faclimlem1  30391  faclimlem3  30393  faclim  30394  iprodfac  30395  equivtotbnd  32122  rrncmslem  32176  rrnequiv  32179  irrapxlem5  35682  xralrple2  37587  limclner  37742  stoweidlem31  37902  stoweidlem59  37930  wallispilem3  37939  wallispilem4  37940  wallispilem5  37941  wallispi  37942  wallispi2lem1  37943  stirlinglem2  37947  stirlinglem4  37949  stirlinglem8  37953  stirlinglem13  37958  stirlinglem15  37960  stirlingr  37962  fourierdlem30  38009  fourierdlem73  38053  fourierdlem87  38067  qndenserrnbllem  38173  ovnsubaddlem1  38402  ovnsubaddlem2  38403  hoiqssbllem1  38454  hoiqssbllem2  38455  hoiqssbllem3  38456
  Copyright terms: Public domain W3C validator