Theorem rpdivcld 13181

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420   / cdiv 11973  ℝ⁺crp 13120

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-rp 13121

This theorem is used by:  bcpasc  14465  mulcn2  15763  o1rlimmul  15786  mertenslem1  16053  mertenslem2  16054  effsumlt  16279  prmind2  16860  nlmvscnlem2  25004  nlmvscnlem1  25005  nghmcn  25064  lebnumlem3  25284  lebnumii  25287  nmoleub3  25440  ipcnlem2  25565  ipcnlem1  25566  equivcfil  25620  equivcau  25621  ovollb2lem  25809  ovoliunlem1  25823  uniioombllem6  25909  itg2const2  26062  itg2cnlem2  26083  aalioulem2  26660  aalioulem4  26662  aalioulem5  26663  aalioulem6  26664  aaliou  26665  aaliou2b  26668  aaliou3lem9  26677  itgulm  26735  abelthlem7  26765  abelthlem8  26766  tanrpcl  26833  logdivlti  26948  logcnlem2  26971  ang180lem2  27138  isosctrlem2  27147  birthdaylem2  27280  cxp2limlem  27303  cxp2lim  27304  cxploglim  27305  cxploglim2  27306  amgmlem  27317  logdiflbnd  27322  emcllem2  27324  fsumharmonic  27339  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem4  27359  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamucov  27365  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  regamcl  27388  relgamcl  27389  lgam1  27391  ftalem4  27403  chpval2  27545  chpchtsum  27546  logfacrlim  27551  logexprlim  27552  bclbnd  27607  bposlem1  27611  bposlem2  27612  lgsquadlem2  27708  chebbnd1lem1  27796  chebbnd1lem3  27798  chebbnd1  27799  chtppilimlem2  27801  chebbnd2  27804  chto1lb  27805  rplogsumlem2  27812  rpvmasumlem  27814  dchrvmasumlem1  27822  dchrvmasum2if  27824  dchrisum0lem1b  27842  dchrisum0lem2a  27844  vmalogdivsum2  27865  2vmadivsumlem  27867  selberglem3  27874  selberg  27875  selberg4lem1  27887  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6a  27909  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2  27918  pntibndlem3  27919  pntlemd  27921  pntlemc  27922  pntlema  27923  pntlemb  27924  pntlemg  27925  pntlemn  27927  pntlemq  27928  pntlemr  27929  pntlemj  27930  pntlemf  27932  pntlemo  27934  pnt2  27940  pnt  27941  ostth2lem3  27962  ostth2  27964  fltne  27975  nrt2irr  31074  blocni  31407  ubthlem2  31473  lnconi  32635  rpxdivcld  33500  omssubadd  34932  hgt750leme  35287  faclimlem1  36508  faclimlem3  36510  faclim  36511  iprodfac  36512  equivtotbnd  38713  rrncmslem  38767  rrnequiv  38770  3lexlogpow2ineq2  43110  3lexlogpow5ineq5  43111  aks4d1p1p7  43125  irrapxlem5  43833  xralrple2  46366  xralrple3  46385  iooiinicc  46554  iooiinioc  46568  limclner  46661  fprodsubrecnncnvlem  46917  fprodaddrecnncnvlem  46919  stoweidlem31  47041  stoweidlem59  47069  wallispilem3  47077  wallispilem4  47078  wallispilem5  47079  wallispi  47080  wallispi2lem1  47081  stirlinglem2  47085  stirlinglem4  47087  stirlinglem8  47091  stirlinglem13  47096  stirlinglem15  47098  stirlingr  47100  fourierdlem30  47147  fourierdlem73  47189  fourierdlem87  47203  qndenserrnbllem  47304  ovnsubaddlem1  47580  ovnsubaddlem2  47581  hoiqssbllem1  47632  hoiqssbllem2  47633  hoiqssbllem3  47634  ovolval5lem1  47662  ovolval5lem2  47663  vonioolem1  47690  smfmullem1  47801  smfmullem2  47802  smfmullem3  47803