Theorem rpdivcld 13105

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7416   / cdiv 11898  ℝ⁺crp 13044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-rp 13045

This theorem is used by:  bcpasc  14387  mulcn2  15685  o1rlimmul  15708  mertenslem1  15975  mertenslem2  15976  effsumlt  16203  prmind2  16779  nlmvscnlem2  24912  nlmvscnlem1  24913  nghmcn  24972  lebnumlem3  25192  lebnumii  25195  nmoleub3  25348  ipcnlem2  25473  ipcnlem1  25474  equivcfil  25528  equivcau  25529  ovollb2lem  25717  ovoliunlem1  25731  uniioombllem6  25817  itg2const2  25970  itg2cnlem2  25991  aalioulem2  26566  aalioulem4  26568  aalioulem5  26569  aalioulem6  26570  aaliou  26571  aaliou2b  26574  aaliou3lem9  26583  itgulm  26641  abelthlem7  26671  abelthlem8  26672  tanrpcl  26739  logdivlti  26855  logcnlem2  26878  ang180lem2  27045  isosctrlem2  27054  birthdaylem2  27187  cxp2limlem  27210  cxp2lim  27211  cxploglim  27212  cxploglim2  27213  amgmlem  27224  logdiflbnd  27229  emcllem2  27231  fsumharmonic  27246  lgamgulmlem2  27264  lgamgulmlem3  27265  lgamgulmlem4  27266  lgamgulmlem5  27267  lgamgulmlem6  27268  lgamgulm2  27270  lgamucov  27272  lgamcvg2  27289  gamcvg  27290  gamcvg2lem  27293  regamcl  27295  relgamcl  27296  lgam1  27298  ftalem4  27310  chpval2  27452  chpchtsum  27453  logfacrlim  27458  logexprlim  27459  bclbnd  27514  bposlem1  27518  bposlem2  27519  lgsquadlem2  27615  chebbnd1lem1  27703  chebbnd1lem3  27705  chebbnd1  27706  chtppilimlem2  27708  chebbnd2  27711  chto1lb  27712  rplogsumlem2  27719  rpvmasumlem  27721  dchrvmasumlem1  27729  dchrvmasum2if  27731  dchrisum0lem1b  27749  dchrisum0lem2a  27751  vmalogdivsum2  27772  2vmadivsumlem  27774  selberglem3  27781  selberg  27782  selberg4lem1  27794  selberg3r  27803  selberg4r  27804  selberg34r  27805  pntrlog2bndlem1  27811  pntrlog2bndlem2  27812  pntrlog2bndlem3  27813  pntrlog2bndlem4  27814  pntrlog2bndlem5  27815  pntrlog2bndlem6a  27816  pntrlog2bndlem6  27817  pntrlog2bnd  27818  pntpbnd1a  27819  pntpbnd1  27820  pntpbnd2  27821  pntibndlem2  27825  pntibndlem3  27826  pntlemd  27828  pntlemc  27829  pntlema  27830  pntlemb  27831  pntlemg  27832  pntlemn  27834  pntlemq  27835  pntlemr  27836  pntlemj  27837  pntlemf  27839  pntlemo  27841  pnt2  27847  pnt  27848  ostth2lem3  27869  ostth2  27871  nrt2irr  30939  blocni  31272  ubthlem2  31338  lnconi  32500  rpxdivcld  33366  omssubadd  34798  hgt750leme  35153  faclimlem1  36309  faclimlem3  36311  faclim  36312  iprodfac  36313  equivtotbnd  38515  rrncmslem  38569  rrnequiv  38572  3lexlogpow2ineq2  42912  3lexlogpow5ineq5  42913  aks4d1p1p7  42927  fltne  43477  irrapxlem5  43654  xralrple2  46171  xralrple3  46190  iooiinicc  46359  iooiinioc  46373  limclner  46466  fprodsubrecnncnvlem  46722  fprodaddrecnncnvlem  46724  stoweidlem31  46846  stoweidlem59  46874  wallispilem3  46882  wallispilem4  46883  wallispilem5  46884  wallispi  46885  wallispi2lem1  46886  stirlinglem2  46890  stirlinglem4  46892  stirlinglem8  46896  stirlinglem13  46901  stirlinglem15  46903  stirlingr  46905  fourierdlem30  46952  fourierdlem73  46994  fourierdlem87  47008  qndenserrnbllem  47109  ovnsubaddlem1  47385  ovnsubaddlem2  47386  hoiqssbllem1  47437  hoiqssbllem2  47438  hoiqssbllem3  47439  ovolval5lem1  47467  ovolval5lem2  47468  vonioolem1  47495  smfmullem1  47606  smfmullem2  47607  smfmullem3  47608