Theorem rerpdivcld 13090

Description: Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
rpgecld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
rpgecld.2	⊢ (𝜑 → 𝐵 ∈ ℝ+)

Assertion

Ref	Expression
rerpdivcld	⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Proof of Theorem rerpdivcld

Step	Hyp	Ref	Expression
1		rpgecld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		rpgecld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
3		rerpdivcl 13047	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℝcr 11098   / cdiv 11870  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  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 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-rp 13016

This theorem is referenced by:  iccf1o  13522  xov1plusxeqvd  13524  expmulnbnd  14270  discr  14275  geomulcvg  15929  mertenslem1  15937  retanhcl  16214  bitsfzolem  16491  bitsfzo  16492  bitsmod  16493  odmodnn0  19609  nmoi  24853  nmoleub  24856  icopnfcnv  25069  nmoleub2lem  25241  nmoleub2lem3  25242  pjthlem1  25564  ovolscalem1  25640  ovolscalem2  25641  ovolsca  25642  mbfmulc2lem  25774  itg2const2  25868  dvferm1lem  26111  abelthlem7  26566  logdivlti  26750  logdivle  26752  logcnlem3  26774  logcnlem4  26775  advlogexp  26785  cxpaddle  26882  cxploglim  27107  cxploglim2  27108  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamucov  27167  ftalem1  27202  ftalem2  27203  basellem3  27212  fsumvma2  27343  chpval2  27347  chpchtsum  27348  chpub  27349  logfacrlim  27353  logexprlim  27354  efexple  27410  bposlem9  27421  chebbnd1lem2  27599  chebbnd1lem3  27600  chtppilim  27604  chpchtlim  27608  chpo1ubb  27610  rplogsumlem1  27613  rplogsumlem2  27614  rpvmasumlem  27616  dchrmusum2  27623  dchrvmasumlem2  27627  dchrisum0fno1  27640  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  rplogsum  27656  mulog2sumlem1  27663  mulog2sumlem2  27664  vmalogdivsum2  27667  vmalogdivsum  27668  2vmadivsumlem  27669  log2sumbnd  27673  selberglem2  27675  selbergb  27678  selberg2b  27681  chpdifbndlem1  27682  selberg3lem1  27686  selberg3lem2  27687  selberg3  27688  selberg4lem1  27689  selberg4  27690  pntrsumo1  27694  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd1a  27714  pntpbnd2  27716  pntibndlem2  27720  pntibndlem3  27721  pntlemb  27726  pntlemg  27727  pntlemh  27728  pntlemn  27729  pntlemr  27731  pntlemj  27732  pntlemf  27734  pntlemk  27735  pntlemo  27736  pnt  27743  ostth2lem1  27747  ostth2lem4  27765  ostth3  27767  pjhthlem1  31683  esumcst  34397  dya2iocress  34608  dya2iocbrsiga  34609  dya2icobrsiga  34610  sxbrsigalem2  34620  probmeasb  34764  itg2addnclem3  38211  ftc1anclem7  38237  geomcau  38297  cntotbnd  38334  bfplem1  38360  fltnlta  43286  binomcxplemnotnn0  44957  divlt0gt0d  45896  lefldiveq  45902  ltmod  46243  0ellimcdiv  46254  wallispilem5  46674  stirlingr  46695  dirkercncflem1  46708  fourierdlem65  46776  hoiqssbllem2  47228