Theorem rerpdivcld 13082

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  ℝcr 11139   / cdiv 11903  ℝ⁺crp 13009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-rp 13010

This theorem is referenced by:  iccf1o  13508  xov1plusxeqvd  13510  expmulnbnd  14233  discr  14238  geomulcvg  15858  mertenslem1  15866  retanhcl  16139  bitsfzolem  16412  bitsfzo  16413  bitsmod  16414  odmodnn0  19507  nmoi  24689  nmoleub  24692  icopnfcnv  24911  nmoleub2lem  25085  nmoleub2lem3  25086  pjthlem1  25409  ovolscalem1  25486  ovolscalem2  25487  ovolsca  25488  mbfmulc2lem  25620  itg2const2  25715  dvferm1lem  25960  abelthlem7  26420  logdivlti  26599  logdivle  26601  logcnlem3  26623  logcnlem4  26624  advlogexp  26634  cxpaddle  26732  cxploglim  26955  cxploglim2  26956  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamucov  27015  ftalem1  27050  ftalem2  27051  basellem3  27060  fsumvma2  27192  chpval2  27196  chpchtsum  27197  chpub  27198  logfacrlim  27202  logexprlim  27203  efexple  27259  bposlem9  27270  chebbnd1lem2  27448  chebbnd1lem3  27449  chtppilim  27453  chpchtlim  27457  chpo1ubb  27459  rplogsumlem1  27462  rplogsumlem2  27463  rpvmasumlem  27465  dchrmusum2  27472  dchrvmasumlem2  27476  dchrisum0fno1  27489  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2a  27495  rplogsum  27505  mulog2sumlem1  27512  mulog2sumlem2  27513  vmalogdivsum2  27516  vmalogdivsum  27517  2vmadivsumlem  27518  log2sumbnd  27522  selberglem2  27524  selbergb  27527  selberg2b  27530  chpdifbndlem1  27531  selberg3lem1  27535  selberg3lem2  27536  selberg3  27537  selberg4lem1  27538  selberg4  27539  pntrsumo1  27543  selberg3r  27547  selberg4r  27548  selberg34r  27549  pntrlog2bndlem1  27555  pntrlog2bndlem2  27556  pntrlog2bndlem3  27557  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  pntrlog2bndlem6  27561  pntrlog2bnd  27562  pntpbnd1a  27563  pntpbnd2  27565  pntibndlem2  27569  pntibndlem3  27570  pntlemb  27575  pntlemg  27576  pntlemh  27577  pntlemn  27578  pntlemr  27580  pntlemj  27581  pntlemf  27583  pntlemk  27584  pntlemo  27585  pnt  27592  ostth2lem1  27596  ostth2lem4  27614  ostth3  27616  pjhthlem1  31273  esumcst  33813  dya2iocress  34025  dya2iocbrsiga  34026  dya2icobrsiga  34027  sxbrsigalem2  34037  probmeasb  34181  itg2addnclem3  37277  ftc1anclem7  37303  geomcau  37363  cntotbnd  37400  bfplem1  37426  fltnlta  42222  binomcxplemnotnn0  43935  divlt0gt0d  44806  lefldiveq  44812  ltmod  45164  0ellimcdiv  45175  wallispilem5  45595  stirlingr  45616  dirkercncflem1  45629  fourierdlem65  45697  hoiqssbllem2  46149