Theorem rerpdivcld 13074

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7399  ℝcr 11120   / cdiv 11886  ℝ⁺crp 13000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197  ax-pre-mulgt0 11198

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-po 5558  df-so 5559  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11460  df-neg 11461  df-div 11887  df-rp 13001

This theorem is referenced by:  iccf1o  13502  xov1plusxeqvd  13504  expmulnbnd  14241  discr  14246  geomulcvg  15879  mertenslem1  15887  retanhcl  16162  bitsfzolem  16438  bitsfzo  16439  bitsmod  16440  odmodnn0  19506  nmoi  24652  nmoleub  24655  icopnfcnv  24876  nmoleub2lem  25050  nmoleub2lem3  25051  pjthlem1  25374  ovolscalem1  25451  ovolscalem2  25452  ovolsca  25453  mbfmulc2lem  25585  itg2const2  25679  dvferm1lem  25925  abelthlem7  26385  logdivlti  26565  logdivle  26567  logcnlem3  26589  logcnlem4  26590  advlogexp  26600  cxpaddle  26698  cxploglim  26924  cxploglim2  26925  lgamgulmlem2  26976  lgamgulmlem3  26977  lgamucov  26984  ftalem1  27019  ftalem2  27020  basellem3  27029  fsumvma2  27161  chpval2  27165  chpchtsum  27166  chpub  27167  logfacrlim  27171  logexprlim  27172  efexple  27228  bposlem9  27239  chebbnd1lem2  27417  chebbnd1lem3  27418  chtppilim  27422  chpchtlim  27426  chpo1ubb  27428  rplogsumlem1  27431  rplogsumlem2  27432  rpvmasumlem  27434  dchrmusum2  27441  dchrvmasumlem2  27445  dchrisum0fno1  27458  dchrisum0lem1b  27462  dchrisum0lem1  27463  dchrisum0lem2a  27464  rplogsum  27474  mulog2sumlem1  27481  mulog2sumlem2  27482  vmalogdivsum2  27485  vmalogdivsum  27486  2vmadivsumlem  27487  log2sumbnd  27491  selberglem2  27493  selbergb  27496  selberg2b  27499  chpdifbndlem1  27500  selberg3lem1  27504  selberg3lem2  27505  selberg3  27506  selberg4lem1  27507  selberg4  27508  pntrsumo1  27512  selberg3r  27516  selberg4r  27517  selberg34r  27518  pntrlog2bndlem1  27524  pntrlog2bndlem2  27525  pntrlog2bndlem3  27526  pntrlog2bndlem4  27527  pntrlog2bndlem5  27528  pntrlog2bndlem6  27530  pntrlog2bnd  27531  pntpbnd1a  27532  pntpbnd2  27534  pntibndlem2  27538  pntibndlem3  27539  pntlemb  27544  pntlemg  27545  pntlemh  27546  pntlemn  27547  pntlemr  27549  pntlemj  27550  pntlemf  27552  pntlemk  27553  pntlemo  27554  pnt  27561  ostth2lem1  27565  ostth2lem4  27583  ostth3  27585  pjhthlem1  31304  esumcst  34002  dya2iocress  34214  dya2iocbrsiga  34215  dya2icobrsiga  34216  sxbrsigalem2  34226  probmeasb  34370  itg2addnclem3  37618  ftc1anclem7  37644  geomcau  37704  cntotbnd  37741  bfplem1  37767  fltnlta  42611  binomcxplemnotnn0  44306  divlt0gt0d  45242  lefldiveq  45248  ltmod  45597  0ellimcdiv  45608  wallispilem5  46028  stirlingr  46049  dirkercncflem1  46062  fourierdlem65  46130  hoiqssbllem2  46582