Theorem rpdivcld 12998

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7362   / cdiv 11802  ℝ⁺crp 12937

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-po 5534  df-so 5535  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-rp 12938

This theorem is referenced by:  bcpasc  14278  mulcn2  15553  o1rlimmul  15576  mertenslem1  15844  mertenslem2  15845  effsumlt  16073  prmind2  16649  nlmvscnlem2  24664  nlmvscnlem1  24665  nghmcn  24724  lebnumlem3  24944  lebnumii  24947  nmoleub3  25100  ipcnlem2  25225  ipcnlem1  25226  equivcfil  25280  equivcau  25281  ovollb2lem  25469  ovoliunlem1  25483  uniioombllem6  25569  itg2const2  25722  itg2cnlem2  25743  aalioulem2  26314  aalioulem4  26316  aalioulem5  26317  aalioulem6  26318  aaliou  26319  aaliou2b  26322  aaliou3lem9  26331  itgulm  26390  abelthlem7  26420  abelthlem8  26421  tanrpcl  26485  logdivlti  26601  logcnlem2  26624  ang180lem2  26791  isosctrlem2  26800  birthdaylem2  26933  cxp2limlem  26957  cxp2lim  26958  cxploglim  26959  cxploglim2  26960  amgmlem  26971  logdiflbnd  26976  emcllem2  26978  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  regamcl  27042  relgamcl  27043  lgam1  27045  ftalem4  27057  chpval2  27199  chpchtsum  27200  logfacrlim  27205  logexprlim  27206  bclbnd  27261  bposlem1  27265  bposlem2  27266  lgsquadlem2  27362  chebbnd1lem1  27450  chebbnd1lem3  27452  chebbnd1  27453  chtppilimlem2  27455  chebbnd2  27458  chto1lb  27459  rplogsumlem2  27466  rpvmasumlem  27468  dchrvmasumlem1  27476  dchrvmasum2if  27478  dchrisum0lem1b  27496  dchrisum0lem2a  27498  vmalogdivsum2  27519  2vmadivsumlem  27521  selberglem3  27528  selberg  27529  selberg4lem1  27541  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6a  27563  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2  27572  pntibndlem3  27573  pntlemd  27575  pntlemc  27576  pntlema  27577  pntlemb  27578  pntlemg  27579  pntlemn  27581  pntlemq  27582  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemo  27588  pnt2  27594  pnt  27595  ostth2lem3  27616  ostth2  27618  nrt2irr  30562  blocni  30895  ubthlem2  30961  lnconi  32123  rpxdivcld  33012  omssubadd  34464  hgt750leme  34822  faclimlem1  35945  faclimlem3  35947  faclim  35948  iprodfac  35949  equivtotbnd  38117  rrncmslem  38171  rrnequiv  38174  3lexlogpow2ineq2  42516  3lexlogpow5ineq5  42517  aks4d1p1p7  42531  fltne  43095  irrapxlem5  43276  xralrple2  45806  xralrple3  45825  iooiinicc  45994  iooiinioc  46008  limclner  46101  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  stoweidlem31  46481  stoweidlem59  46509  wallispilem3  46517  wallispilem4  46518  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  stirlinglem2  46525  stirlinglem4  46527  stirlinglem8  46531  stirlinglem13  46536  stirlinglem15  46538  stirlingr  46540  fourierdlem30  46587  fourierdlem73  46629  fourierdlem87  46643  qndenserrnbllem  46744  ovnsubaddlem1  47020  ovnsubaddlem2  47021  hoiqssbllem1  47072  hoiqssbllem2  47073  hoiqssbllem3  47074  ovolval5lem1  47102  ovolval5lem2  47103  vonioolem1  47130  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243