Theorem rerpdivcld 13011

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031   / cdiv 11801  ℝ⁺crp 12936

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 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

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 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-rp 12937

This theorem is referenced by:  iccf1o  13443  xov1plusxeqvd  13445  expmulnbnd  14191  discr  14196  geomulcvg  15835  mertenslem1  15843  retanhcl  16120  bitsfzolem  16397  bitsfzo  16398  bitsmod  16399  odmodnn0  19509  nmoi  24706  nmoleub  24709  icopnfcnv  24922  nmoleub2lem  25094  nmoleub2lem3  25095  pjthlem1  25417  ovolscalem1  25493  ovolscalem2  25494  ovolsca  25495  mbfmulc2lem  25627  itg2const2  25721  dvferm1lem  25964  abelthlem7  26419  logdivlti  26600  logdivle  26602  logcnlem3  26624  logcnlem4  26625  advlogexp  26635  cxpaddle  26732  cxploglim  26958  cxploglim2  26959  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamucov  27018  ftalem1  27053  ftalem2  27054  basellem3  27063  fsumvma2  27194  chpval2  27198  chpchtsum  27199  chpub  27200  logfacrlim  27204  logexprlim  27205  efexple  27261  bposlem9  27272  chebbnd1lem2  27450  chebbnd1lem3  27451  chtppilim  27455  chpchtlim  27459  chpo1ubb  27461  rplogsumlem1  27464  rplogsumlem2  27465  rpvmasumlem  27467  dchrmusum2  27474  dchrvmasumlem2  27478  dchrisum0fno1  27491  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  rplogsum  27507  mulog2sumlem1  27514  mulog2sumlem2  27515  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  log2sumbnd  27524  selberglem2  27526  selbergb  27529  selberg2b  27532  chpdifbndlem1  27533  selberg3lem1  27537  selberg3lem2  27538  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd2  27567  pntibndlem2  27571  pntibndlem3  27572  pntlemb  27577  pntlemg  27578  pntlemh  27579  pntlemn  27580  pntlemr  27582  pntlemj  27583  pntlemf  27585  pntlemk  27586  pntlemo  27587  pnt  27594  ostth2lem1  27598  ostth2lem4  27616  ostth3  27618  pjhthlem1  31480  esumcst  34226  dya2iocress  34437  dya2iocbrsiga  34438  dya2icobrsiga  34439  sxbrsigalem2  34449  probmeasb  34593  itg2addnclem3  38011  ftc1anclem7  38037  geomcau  38097  cntotbnd  38134  bfplem1  38160  fltnlta  43113  binomcxplemnotnn0  44804  divlt0gt0d  45740  lefldiveq  45746  ltmod  46087  0ellimcdiv  46098  wallispilem5  46518  stirlingr  46539  dirkercncflem1  46552  fourierdlem65  46620  hoiqssbllem2  47072