Theorem rpdivcld 13056

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398   / cdiv 11846  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-rp 12996

This theorem is referenced by:  bcpasc  14336  mulcn2  15625  o1rlimmul  15648  mertenslem1  15916  mertenslem2  15917  effsumlt  16145  prmind2  16721  nlmvscnlem2  24747  nlmvscnlem1  24748  nghmcn  24807  lebnumlem3  25027  lebnumii  25030  nmoleub3  25183  ipcnlem2  25308  ipcnlem1  25309  equivcfil  25363  equivcau  25364  ovollb2lem  25552  ovoliunlem1  25566  uniioombllem6  25652  itg2const2  25805  itg2cnlem2  25826  aalioulem2  26399  aalioulem4  26401  aalioulem5  26402  aalioulem6  26403  aaliou  26404  aaliou2b  26407  aaliou3lem9  26416  itgulm  26473  abelthlem7  26503  abelthlem8  26504  tanrpcl  26571  logdivlti  26687  logcnlem2  26710  ang180lem2  26877  isosctrlem2  26886  birthdaylem2  27019  cxp2limlem  27042  cxp2lim  27043  cxploglim  27044  cxploglim2  27045  amgmlem  27056  logdiflbnd  27061  emcllem2  27063  fsumharmonic  27078  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem5  27099  lgamgulmlem6  27100  lgamgulm2  27102  lgamucov  27104  lgamcvg2  27121  gamcvg  27122  gamcvg2lem  27125  regamcl  27127  relgamcl  27128  lgam1  27130  ftalem4  27142  chpval2  27284  chpchtsum  27285  logfacrlim  27290  logexprlim  27291  bclbnd  27346  bposlem1  27350  bposlem2  27351  lgsquadlem2  27447  chebbnd1lem1  27535  chebbnd1lem3  27537  chebbnd1  27538  chtppilimlem2  27540  chebbnd2  27543  chto1lb  27544  rplogsumlem2  27551  rpvmasumlem  27553  dchrvmasumlem1  27561  dchrvmasum2if  27563  dchrisum0lem1b  27581  dchrisum0lem2a  27583  vmalogdivsum2  27604  2vmadivsumlem  27606  selberglem3  27613  selberg  27614  selberg4lem1  27626  selberg3r  27635  selberg4r  27636  selberg34r  27637  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6a  27648  pntrlog2bndlem6  27649  pntrlog2bnd  27650  pntpbnd1a  27651  pntpbnd1  27652  pntpbnd2  27653  pntibndlem2  27657  pntibndlem3  27658  pntlemd  27660  pntlemc  27661  pntlema  27662  pntlemb  27663  pntlemg  27664  pntlemn  27666  pntlemq  27667  pntlemr  27668  pntlemj  27669  pntlemf  27671  pntlemo  27673  pnt2  27679  pnt  27680  ostth2lem3  27701  ostth2  27703  nrt2irr  30677  blocni  31010  ubthlem2  31076  lnconi  32238  rpxdivcld  33113  omssubadd  34599  hgt750leme  34954  faclimlem1  36098  faclimlem3  36100  faclim  36101  iprodfac  36102  equivtotbnd  38282  rrncmslem  38336  rrnequiv  38339  3lexlogpow2ineq2  42681  3lexlogpow5ineq5  42682  aks4d1p1p7  42696  fltne  43231  irrapxlem5  43408  xralrple2  45935  xralrple3  45954  iooiinicc  46123  iooiinioc  46137  limclner  46230  fprodsubrecnncnvlem  46486  fprodaddrecnncnvlem  46488  stoweidlem31  46610  stoweidlem59  46638  wallispilem3  46646  wallispilem4  46647  wallispilem5  46648  wallispi  46649  wallispi2lem1  46650  stirlinglem2  46654  stirlinglem4  46656  stirlinglem8  46660  stirlinglem13  46665  stirlinglem15  46667  stirlingr  46669  fourierdlem30  46716  fourierdlem73  46758  fourierdlem87  46772  qndenserrnbllem  46873  ovnsubaddlem1  47149  ovnsubaddlem2  47150  hoiqssbllem1  47201  hoiqssbllem2  47202  hoiqssbllem3  47203  ovolval5lem1  47231  ovolval5lem2  47232  vonioolem1  47259  smfmullem1  47370  smfmullem2  47371  smfmullem3  47372