Theorem rerpdivcld 13086

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   / cdiv 11866  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-rp 13012

This theorem is referenced by:  iccf1o  13518  xov1plusxeqvd  13520  expmulnbnd  14267  discr  14272  geomulcvg  15926  mertenslem1  15934  retanhcl  16210  bitsfzolem  16487  bitsfzo  16488  bitsmod  16489  odmodnn0  19605  nmoi  24885  nmoleub  24888  icopnfcnv  25101  nmoleub2lem  25273  nmoleub2lem3  25274  pjthlem1  25596  ovolscalem1  25672  ovolscalem2  25673  ovolsca  25674  mbfmulc2lem  25806  itg2const2  25900  dvferm1lem  26143  abelthlem7  26601  logdivlti  26785  logdivle  26787  logcnlem3  26809  logcnlem4  26810  advlogexp  26820  cxpaddle  26917  cxploglim  27142  cxploglim2  27143  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamucov  27202  ftalem1  27237  ftalem2  27238  basellem3  27247  fsumvma2  27378  chpval2  27382  chpchtsum  27383  chpub  27384  logfacrlim  27388  logexprlim  27389  efexple  27445  bposlem9  27456  chebbnd1lem2  27634  chebbnd1lem3  27635  chtppilim  27639  chpchtlim  27643  chpo1ubb  27645  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrmusum2  27658  dchrvmasumlem2  27662  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  rplogsum  27691  mulog2sumlem1  27698  mulog2sumlem2  27699  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  log2sumbnd  27708  selberglem2  27710  selbergb  27713  selberg2b  27716  chpdifbndlem1  27717  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem2  27755  pntibndlem3  27756  pntlemb  27761  pntlemg  27762  pntlemh  27763  pntlemn  27764  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemk  27770  pntlemo  27771  pnt  27778  ostth2lem1  27782  ostth2lem4  27800  ostth3  27802  pjhthlem1  31743  esumcst  34453  dya2iocress  34664  dya2iocbrsiga  34665  dya2icobrsiga  34666  sxbrsigalem2  34676  probmeasb  34820  itg2addnclem3  38324  ftc1anclem7  38350  geomcau  38410  cntotbnd  38447  bfplem1  38473  fltnlta  43395  binomcxplemnotnn0  45066  divlt0gt0d  46005  lefldiveq  46011  ltmod  46352  0ellimcdiv  46363  wallispilem5  46783  stirlingr  46804  dirkercncflem1  46817  fourierdlem65  46885  hoiqssbllem2  47337