Theorem rpdivcld 13035

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 13001	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411   / cdiv 11873  ℝ⁺crp 12976

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-rp 12977

This theorem is referenced by:  bcpasc  14283  mulcn2  15542  o1rlimmul  15565  mertenslem1  15832  mertenslem2  15833  effsumlt  16056  prmind2  16624  nlmvscnlem2  24209  nlmvscnlem1  24210  nghmcn  24269  lebnumlem3  24486  lebnumii  24489  nmoleub3  24642  ipcnlem2  24768  ipcnlem1  24769  equivcfil  24823  equivcau  24824  ovollb2lem  25012  ovoliunlem1  25026  uniioombllem6  25112  itg2const2  25266  itg2cnlem2  25287  aalioulem2  25853  aalioulem4  25855  aalioulem5  25856  aalioulem6  25857  aaliou  25858  aaliou2b  25861  aaliou3lem9  25870  itgulm  25927  abelthlem7  25957  abelthlem8  25958  tanrpcl  26021  logdivlti  26135  logcnlem2  26158  ang180lem2  26322  isosctrlem2  26331  birthdaylem2  26464  cxp2limlem  26487  cxp2lim  26488  cxploglim  26489  cxploglim2  26490  amgmlem  26501  logdiflbnd  26506  emcllem2  26508  fsumharmonic  26523  lgamgulmlem2  26541  lgamgulmlem3  26542  lgamgulmlem4  26543  lgamgulmlem5  26544  lgamgulmlem6  26545  lgamgulm2  26547  lgamucov  26549  lgamcvg2  26566  gamcvg  26567  gamcvg2lem  26570  regamcl  26572  relgamcl  26573  lgam1  26575  ftalem4  26587  chpval2  26728  chpchtsum  26729  logfacrlim  26734  logexprlim  26735  bclbnd  26790  bposlem1  26794  bposlem2  26795  lgsquadlem2  26891  chebbnd1lem1  26979  chebbnd1lem3  26981  chebbnd1  26982  chtppilimlem2  26984  chebbnd2  26987  chto1lb  26988  rplogsumlem2  26995  rpvmasumlem  26997  dchrvmasumlem1  27005  dchrvmasum2if  27007  dchrisum0lem1b  27025  dchrisum0lem2a  27027  vmalogdivsum2  27048  2vmadivsumlem  27050  selberglem3  27057  selberg  27058  selberg4lem1  27070  selberg3r  27079  selberg4r  27080  selberg34r  27081  pntrlog2bndlem1  27087  pntrlog2bndlem2  27088  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  pntrlog2bndlem6a  27092  pntrlog2bndlem6  27093  pntrlog2bnd  27094  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  pntibndlem2  27101  pntibndlem3  27102  pntlemd  27104  pntlemc  27105  pntlema  27106  pntlemb  27107  pntlemg  27108  pntlemn  27110  pntlemq  27111  pntlemr  27112  pntlemj  27113  pntlemf  27115  pntlemo  27117  pnt2  27123  pnt  27124  ostth2lem3  27145  ostth2  27147  nrt2irr  29764  blocni  30096  ubthlem2  30162  lnconi  31324  rpxdivcld  32138  omssubadd  33368  hgt750leme  33739  faclimlem1  34782  faclimlem3  34784  faclim  34785  iprodfac  34786  equivtotbnd  36732  rrncmslem  36786  rrnequiv  36789  3lexlogpow2ineq2  41010  3lexlogpow5ineq5  41011  aks4d1p1p7  41025  fltne  41468  irrapxlem5  41646  xralrple2  44143  xralrple3  44163  iooiinicc  44334  iooiinioc  44348  limclner  44446  fprodsubrecnncnvlem  44702  fprodaddrecnncnvlem  44704  stoweidlem31  44826  stoweidlem59  44854  wallispilem3  44862  wallispilem4  44863  wallispilem5  44864  wallispi  44865  wallispi2lem1  44866  stirlinglem2  44870  stirlinglem4  44872  stirlinglem8  44876  stirlinglem13  44881  stirlinglem15  44883  stirlingr  44885  fourierdlem30  44932  fourierdlem73  44974  fourierdlem87  44988  qndenserrnbllem  45089  ovnsubaddlem1  45365  ovnsubaddlem2  45366  hoiqssbllem1  45417  hoiqssbllem2  45418  hoiqssbllem3  45419  ovolval5lem1  45447  ovolval5lem2  45448  vonioolem1  45475  smfmullem1  45586  smfmullem2  45587  smfmullem3  45588