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

Theorem rpdivcld 11036
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 11005 . 2  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  ( A  /  B )  e.  RR+ )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  /  B
)  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756  (class class class)co 6086    / cdiv 9985   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-rp 10984
This theorem is referenced by:  bcpasc  12089  mulcn2  13065  o1rlimmul  13088  mertenslem1  13336  mertenslem2  13337  effsumlt  13387  prmind2  13766  nlmvscnlem2  20241  nlmvscnlem1  20242  nghmcn  20299  lebnumlem3  20510  lebnumii  20513  nmoleub3  20649  ipcnlem2  20731  ipcnlem1  20732  equivcfil  20785  equivcau  20786  ovollb2lem  20946  ovoliunlem1  20960  uniioombllem6  21043  itg2const2  21194  itg2cnlem2  21215  aalioulem2  21774  aalioulem4  21776  aalioulem5  21777  aalioulem6  21778  aaliou  21779  aaliou2b  21782  aaliou3lem9  21791  itgulm  21848  abelthlem7  21878  abelthlem8  21879  tanrpcl  21941  logdivlti  22044  logcnlem2  22063  ang180lem2  22181  isosctrlem2  22192  birthdaylem2  22321  cxp2limlem  22344  cxp2lim  22345  cxploglim  22346  cxploglim2  22347  amgmlem  22358  logdiflbnd  22363  emcllem2  22365  fsumharmonic  22380  ftalem4  22388  chpval2  22532  chpchtsum  22533  logfacrlim  22538  logexprlim  22539  bclbnd  22594  bposlem1  22598  bposlem2  22599  lgsquadlem2  22669  chebbnd1lem1  22693  chebbnd1lem3  22695  chebbnd1  22696  chtppilimlem2  22698  chebbnd2  22701  chto1lb  22702  rplogsumlem2  22709  rpvmasumlem  22711  dchrvmasumlem1  22719  dchrvmasum2if  22721  dchrisum0lem1b  22739  dchrisum0lem2a  22741  vmalogdivsum2  22762  2vmadivsumlem  22764  selberglem3  22771  selberg  22772  selberg4lem1  22784  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6a  22806  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntlemd  22818  pntlemc  22819  pntlema  22820  pntlemb  22821  pntlemg  22822  pntlemn  22824  pntlemq  22825  pntlemr  22826  pntlemj  22827  pntlemf  22829  pntlemo  22831  pnt2  22837  pnt  22838  ostth2lem3  22859  ostth2  22861  blocni  24156  ubthlem2  24223  lnconi  25388  rpxdivcld  26060  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgamucov  26976  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  regamcl  26999  relgamcl  27000  lgam1  27002  faclimlem1  27500  faclimlem3  27502  faclim  27503  iprodfac  27504  equivtotbnd  28630  rrncmslem  28684  rrnequiv  28687  irrapxlem5  29120  stoweidlem31  29779  stoweidlem59  29807  wallispilem3  29815  wallispilem4  29816  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  stirlinglem2  29823  stirlinglem4  29825  stirlinglem8  29829  stirlinglem13  29834  stirlinglem14  29835  stirlinglem15  29836  stirlingr  29838
  Copyright terms: Public domain W3C validator