Theorem rpdivcld 12980

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

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
3		rpdivcl 12946	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7370   / cdiv 11808  ℝ⁺crp 12919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-rp 12920

This theorem is referenced by:  bcpasc  14258  mulcn2  15533  o1rlimmul  15556  mertenslem1  15821  mertenslem2  15822  effsumlt  16050  prmind2  16626  nlmvscnlem2  24646  nlmvscnlem1  24647  nghmcn  24706  lebnumlem3  24935  lebnumii  24938  nmoleub3  25092  ipcnlem2  25217  ipcnlem1  25218  equivcfil  25272  equivcau  25273  ovollb2lem  25462  ovoliunlem1  25476  uniioombllem6  25562  itg2const2  25715  itg2cnlem2  25736  aalioulem2  26314  aalioulem4  26316  aalioulem5  26317  aalioulem6  26318  aaliou  26319  aaliou2b  26322  aaliou3lem9  26331  itgulm  26390  abelthlem7  26421  abelthlem8  26422  tanrpcl  26486  logdivlti  26602  logcnlem2  26625  ang180lem2  26793  isosctrlem2  26802  birthdaylem2  26935  cxp2limlem  26959  cxp2lim  26960  cxploglim  26961  cxploglim2  26962  amgmlem  26973  logdiflbnd  26978  emcllem2  26980  fsumharmonic  26995  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamgulmlem4  27015  lgamgulmlem5  27016  lgamgulmlem6  27017  lgamgulm2  27019  lgamucov  27021  lgamcvg2  27038  gamcvg  27039  gamcvg2lem  27042  regamcl  27044  relgamcl  27045  lgam1  27047  ftalem4  27059  chpval2  27202  chpchtsum  27203  logfacrlim  27208  logexprlim  27209  bclbnd  27264  bposlem1  27268  bposlem2  27269  lgsquadlem2  27365  chebbnd1lem1  27453  chebbnd1lem3  27455  chebbnd1  27456  chtppilimlem2  27458  chebbnd2  27461  chto1lb  27462  rplogsumlem2  27469  rpvmasumlem  27471  dchrvmasumlem1  27479  dchrvmasum2if  27481  dchrisum0lem1b  27499  dchrisum0lem2a  27501  vmalogdivsum2  27522  2vmadivsumlem  27524  selberglem3  27531  selberg  27532  selberg4lem1  27544  selberg3r  27553  selberg4r  27554  selberg34r  27555  pntrlog2bndlem1  27561  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  pntrlog2bndlem6a  27566  pntrlog2bndlem6  27567  pntrlog2bnd  27568  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem2  27575  pntibndlem3  27576  pntlemd  27578  pntlemc  27579  pntlema  27580  pntlemb  27581  pntlemg  27582  pntlemn  27584  pntlemq  27585  pntlemr  27586  pntlemj  27587  pntlemf  27589  pntlemo  27591  pnt2  27597  pnt  27598  ostth2lem3  27619  ostth2  27621  nrt2irr  30566  blocni  30899  ubthlem2  30965  lnconi  32127  rpxdivcld  33032  omssubadd  34484  hgt750leme  34842  faclimlem1  35965  faclimlem3  35967  faclim  35968  iprodfac  35969  equivtotbnd  38058  rrncmslem  38112  rrnequiv  38115  3lexlogpow2ineq2  42458  3lexlogpow5ineq5  42459  aks4d1p1p7  42473  fltne  43031  irrapxlem5  43212  xralrple2  45742  xralrple3  45761  iooiinicc  45931  iooiinioc  45945  limclner  46038  fprodsubrecnncnvlem  46294  fprodaddrecnncnvlem  46296  stoweidlem31  46418  stoweidlem59  46446  wallispilem3  46454  wallispilem4  46455  wallispilem5  46456  wallispi  46457  wallispi2lem1  46458  stirlinglem2  46462  stirlinglem4  46464  stirlinglem8  46468  stirlinglem13  46473  stirlinglem15  46475  stirlingr  46477  fourierdlem30  46524  fourierdlem73  46566  fourierdlem87  46580  qndenserrnbllem  46681  ovnsubaddlem1  46957  ovnsubaddlem2  46958  hoiqssbllem1  47009  hoiqssbllem2  47010  hoiqssbllem3  47011  ovolval5lem1  47039  ovolval5lem2  47040  vonioolem1  47067  smfmullem1  47178  smfmullem2  47179  smfmullem3  47180