Theorem rpdivcld 13029

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7405   / cdiv 11867  ℝ⁺crp 12970

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 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-rp 12971

This theorem is referenced by:  bcpasc  14277  mulcn2  15536  o1rlimmul  15559  mertenslem1  15826  mertenslem2  15827  effsumlt  16050  prmind2  16618  nlmvscnlem2  24193  nlmvscnlem1  24194  nghmcn  24253  lebnumlem3  24470  lebnumii  24473  nmoleub3  24626  ipcnlem2  24752  ipcnlem1  24753  equivcfil  24807  equivcau  24808  ovollb2lem  24996  ovoliunlem1  25010  uniioombllem6  25096  itg2const2  25250  itg2cnlem2  25271  aalioulem2  25837  aalioulem4  25839  aalioulem5  25840  aalioulem6  25841  aaliou  25842  aaliou2b  25845  aaliou3lem9  25854  itgulm  25911  abelthlem7  25941  abelthlem8  25942  tanrpcl  26005  logdivlti  26119  logcnlem2  26142  ang180lem2  26304  isosctrlem2  26313  birthdaylem2  26446  cxp2limlem  26469  cxp2lim  26470  cxploglim  26471  cxploglim2  26472  amgmlem  26483  logdiflbnd  26488  emcllem2  26490  fsumharmonic  26505  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamgulmlem4  26525  lgamgulmlem5  26526  lgamgulmlem6  26527  lgamgulm2  26529  lgamucov  26531  lgamcvg2  26548  gamcvg  26549  gamcvg2lem  26552  regamcl  26554  relgamcl  26555  lgam1  26557  ftalem4  26569  chpval2  26710  chpchtsum  26711  logfacrlim  26716  logexprlim  26717  bclbnd  26772  bposlem1  26776  bposlem2  26777  lgsquadlem2  26873  chebbnd1lem1  26961  chebbnd1lem3  26963  chebbnd1  26964  chtppilimlem2  26966  chebbnd2  26969  chto1lb  26970  rplogsumlem2  26977  rpvmasumlem  26979  dchrvmasumlem1  26987  dchrvmasum2if  26989  dchrisum0lem1b  27007  dchrisum0lem2a  27009  vmalogdivsum2  27030  2vmadivsumlem  27032  selberglem3  27039  selberg  27040  selberg4lem1  27052  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntrlog2bndlem1  27069  pntrlog2bndlem2  27070  pntrlog2bndlem3  27071  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  pntrlog2bndlem6a  27074  pntrlog2bndlem6  27075  pntrlog2bnd  27076  pntpbnd1a  27077  pntpbnd1  27078  pntpbnd2  27079  pntibndlem2  27083  pntibndlem3  27084  pntlemd  27086  pntlemc  27087  pntlema  27088  pntlemb  27089  pntlemg  27090  pntlemn  27092  pntlemq  27093  pntlemr  27094  pntlemj  27095  pntlemf  27097  pntlemo  27099  pnt2  27105  pnt  27106  ostth2lem3  27127  ostth2  27129  blocni  30045  ubthlem2  30111  lnconi  31273  rpxdivcld  32087  omssubadd  33287  hgt750leme  33658  faclimlem1  34701  faclimlem3  34703  faclim  34704  iprodfac  34705  equivtotbnd  36634  rrncmslem  36688  rrnequiv  36691  3lexlogpow2ineq2  40912  3lexlogpow5ineq5  40913  aks4d1p1p7  40927  fltne  41382  irrapxlem5  41549  xralrple2  44050  xralrple3  44070  iooiinicc  44241  iooiinioc  44255  limclner  44353  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  stoweidlem31  44733  stoweidlem59  44761  wallispilem3  44769  wallispilem4  44770  wallispilem5  44771  wallispi  44772  wallispi2lem1  44773  stirlinglem2  44777  stirlinglem4  44779  stirlinglem8  44783  stirlinglem13  44788  stirlinglem15  44790  stirlingr  44792  fourierdlem30  44839  fourierdlem73  44881  fourierdlem87  44895  qndenserrnbllem  44996  ovnsubaddlem1  45272  ovnsubaddlem2  45273  hoiqssbllem1  45324  hoiqssbllem2  45325  hoiqssbllem3  45326  ovolval5lem1  45354  ovolval5lem2  45355  vonioolem1  45382  smfmullem1  45493  smfmullem2  45494  smfmullem3  45495