Theorem rpdivcld 13068

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7405   / cdiv 11894  ℝ⁺crp 13008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-rp 13009

This theorem is referenced by:  bcpasc  14339  mulcn2  15612  o1rlimmul  15635  mertenslem1  15900  mertenslem2  15901  effsumlt  16129  prmind2  16704  nlmvscnlem2  24624  nlmvscnlem1  24625  nghmcn  24684  lebnumlem3  24913  lebnumii  24916  nmoleub3  25070  ipcnlem2  25196  ipcnlem1  25197  equivcfil  25251  equivcau  25252  ovollb2lem  25441  ovoliunlem1  25455  uniioombllem6  25541  itg2const2  25694  itg2cnlem2  25715  aalioulem2  26293  aalioulem4  26295  aalioulem5  26296  aalioulem6  26297  aaliou  26298  aaliou2b  26301  aaliou3lem9  26310  itgulm  26369  abelthlem7  26400  abelthlem8  26401  tanrpcl  26465  logdivlti  26581  logcnlem2  26604  ang180lem2  26772  isosctrlem2  26781  birthdaylem2  26914  cxp2limlem  26938  cxp2lim  26939  cxploglim  26940  cxploglim2  26941  amgmlem  26952  logdiflbnd  26957  emcllem2  26959  fsumharmonic  26974  lgamgulmlem2  26992  lgamgulmlem3  26993  lgamgulmlem4  26994  lgamgulmlem5  26995  lgamgulmlem6  26996  lgamgulm2  26998  lgamucov  27000  lgamcvg2  27017  gamcvg  27018  gamcvg2lem  27021  regamcl  27023  relgamcl  27024  lgam1  27026  ftalem4  27038  chpval2  27181  chpchtsum  27182  logfacrlim  27187  logexprlim  27188  bclbnd  27243  bposlem1  27247  bposlem2  27248  lgsquadlem2  27344  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem2  27437  chebbnd2  27440  chto1lb  27441  rplogsumlem2  27448  rpvmasumlem  27450  dchrvmasumlem1  27458  dchrvmasum2if  27460  dchrisum0lem1b  27478  dchrisum0lem2a  27480  vmalogdivsum2  27501  2vmadivsumlem  27503  selberglem3  27510  selberg  27511  selberg4lem1  27523  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6a  27545  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntibndlem3  27555  pntlemd  27557  pntlemc  27558  pntlema  27559  pntlemb  27560  pntlemg  27561  pntlemn  27563  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemo  27570  pnt2  27576  pnt  27577  ostth2lem3  27598  ostth2  27600  nrt2irr  30454  blocni  30786  ubthlem2  30852  lnconi  32014  rpxdivcld  32908  omssubadd  34332  hgt750leme  34690  faclimlem1  35760  faclimlem3  35762  faclim  35763  iprodfac  35764  equivtotbnd  37802  rrncmslem  37856  rrnequiv  37859  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  aks4d1p1p7  42087  fltne  42667  irrapxlem5  42849  xralrple2  45381  xralrple3  45401  iooiinicc  45571  iooiinioc  45585  limclner  45680  fprodsubrecnncnvlem  45936  fprodaddrecnncnvlem  45938  stoweidlem31  46060  stoweidlem59  46088  wallispilem3  46096  wallispilem4  46097  wallispilem5  46098  wallispi  46099  wallispi2lem1  46100  stirlinglem2  46104  stirlinglem4  46106  stirlinglem8  46110  stirlinglem13  46115  stirlinglem15  46117  stirlingr  46119  fourierdlem30  46166  fourierdlem73  46208  fourierdlem87  46222  qndenserrnbllem  46323  ovnsubaddlem1  46599  ovnsubaddlem2  46600  hoiqssbllem1  46651  hoiqssbllem2  46652  hoiqssbllem3  46653  ovolval5lem1  46681  ovolval5lem2  46682  vonioolem1  46709  smfmullem1  46820  smfmullem2  46821  smfmullem3  46822