Theorem rpdivcld 12544

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7183   / cdiv 11388  ℝ⁺crp 12485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7492  ax-resscn 10685  ax-1cn 10686  ax-icn 10687  ax-addcl 10688  ax-addrcl 10689  ax-mulcl 10690  ax-mulrcl 10691  ax-mulcom 10692  ax-addass 10693  ax-mulass 10694  ax-distr 10695  ax-i2m1 10696  ax-1ne0 10697  ax-1rid 10698  ax-rnegex 10699  ax-rrecex 10700  ax-cnre 10701  ax-pre-lttri 10702  ax-pre-lttrn 10703  ax-pre-ltadd 10704  ax-pre-mulgt0 10705

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-po 5452  df-so 5453  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-iota 6308  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7140  df-ov 7186  df-oprab 7187  df-mpo 7188  df-er 8333  df-en 8569  df-dom 8570  df-sdom 8571  df-pnf 10768  df-mnf 10769  df-xr 10770  df-ltxr 10771  df-le 10772  df-sub 10963  df-neg 10964  df-div 11389  df-rp 12486

This theorem is referenced by:  bcpasc  13786  mulcn2  15056  o1rlimmul  15079  mertenslem1  15345  mertenslem2  15346  effsumlt  15569  prmind2  16139  nlmvscnlem2  23451  nlmvscnlem1  23452  nghmcn  23511  lebnumlem3  23728  lebnumii  23731  nmoleub3  23884  ipcnlem2  24009  ipcnlem1  24010  equivcfil  24064  equivcau  24065  ovollb2lem  24253  ovoliunlem1  24267  uniioombllem6  24353  itg2const2  24507  itg2cnlem2  24528  aalioulem2  25094  aalioulem4  25096  aalioulem5  25097  aalioulem6  25098  aaliou  25099  aaliou2b  25102  aaliou3lem9  25111  itgulm  25168  abelthlem7  25198  abelthlem8  25199  tanrpcl  25262  logdivlti  25376  logcnlem2  25399  ang180lem2  25561  isosctrlem2  25570  birthdaylem2  25703  cxp2limlem  25726  cxp2lim  25727  cxploglim  25728  cxploglim2  25729  amgmlem  25740  logdiflbnd  25745  emcllem2  25747  fsumharmonic  25762  lgamgulmlem2  25780  lgamgulmlem3  25781  lgamgulmlem4  25782  lgamgulmlem5  25783  lgamgulmlem6  25784  lgamgulm2  25786  lgamucov  25788  lgamcvg2  25805  gamcvg  25806  gamcvg2lem  25809  regamcl  25811  relgamcl  25812  lgam1  25814  ftalem4  25826  chpval2  25967  chpchtsum  25968  logfacrlim  25973  logexprlim  25974  bclbnd  26029  bposlem1  26033  bposlem2  26034  lgsquadlem2  26130  chebbnd1lem1  26218  chebbnd1lem3  26220  chebbnd1  26221  chtppilimlem2  26223  chebbnd2  26226  chto1lb  26227  rplogsumlem2  26234  rpvmasumlem  26236  dchrvmasumlem1  26244  dchrvmasum2if  26246  dchrisum0lem1b  26264  dchrisum0lem2a  26266  vmalogdivsum2  26287  2vmadivsumlem  26289  selberglem3  26296  selberg  26297  selberg4lem1  26309  selberg3r  26318  selberg4r  26319  selberg34r  26320  pntrlog2bndlem1  26326  pntrlog2bndlem2  26327  pntrlog2bndlem3  26328  pntrlog2bndlem4  26329  pntrlog2bndlem5  26330  pntrlog2bndlem6a  26331  pntrlog2bndlem6  26332  pntrlog2bnd  26333  pntpbnd1a  26334  pntpbnd1  26335  pntpbnd2  26336  pntibndlem2  26340  pntibndlem3  26341  pntlemd  26343  pntlemc  26344  pntlema  26345  pntlemb  26346  pntlemg  26347  pntlemn  26349  pntlemq  26350  pntlemr  26351  pntlemj  26352  pntlemf  26354  pntlemo  26356  pnt2  26362  pnt  26363  ostth2lem3  26384  ostth2  26386  blocni  28753  ubthlem2  28819  lnconi  29981  rpxdivcld  30796  omssubadd  31850  hgt750leme  32221  faclimlem1  33295  faclimlem3  33297  faclim  33298  iprodfac  33299  equivtotbnd  35592  rrncmslem  35646  rrnequiv  35649  3lexlogpow2ineq2  39720  3lexlogpow5ineq5  39721  aks4d1p1p7  39734  fltne  40094  irrapxlem5  40261  xralrple2  42472  xralrple3  42492  iooiinicc  42661  iooiinioc  42675  limclner  42775  fprodsubrecnncnvlem  43031  fprodaddrecnncnvlem  43033  stoweidlem31  43155  stoweidlem59  43183  wallispilem3  43191  wallispilem4  43192  wallispilem5  43193  wallispi  43194  wallispi2lem1  43195  stirlinglem2  43199  stirlinglem4  43201  stirlinglem8  43205  stirlinglem13  43210  stirlinglem15  43212  stirlingr  43214  fourierdlem30  43261  fourierdlem73  43303  fourierdlem87  43317  qndenserrnbllem  43418  ovnsubaddlem1  43691  ovnsubaddlem2  43692  hoiqssbllem1  43743  hoiqssbllem2  43744  hoiqssbllem3  43745  ovolval5lem1  43773  ovolval5lem2  43774  vonioolem1  43801  smfmullem1  43905  smfmullem2  43906  smfmullem3  43907