MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rerpdivcld Structured version   Visualization version   GIF version

Theorem rerpdivcld 12441
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
StepHypRef Expression
1 rpgecld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 rpgecld.2 . 2 (𝜑𝐵 ∈ ℝ+)
3 rerpdivcl 12398 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ)
41, 2, 3syl2anc 586 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  (class class class)co 7133  cr 10514   / cdiv 11275  +crp 12368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-po 5450  df-so 5451  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-er 8267  df-en 8488  df-dom 8489  df-sdom 8490  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-rp 12369
This theorem is referenced by:  iccf1o  12865  xov1plusxeqvd  12867  expmulnbnd  13581  discr  13586  geomulcvg  15212  mertenslem1  15220  retanhcl  15492  bitsfzolem  15761  bitsfzo  15762  bitsmod  15763  odmodnn0  18647  nmoi  23313  nmoleub  23316  icopnfcnv  23526  nmoleub2lem  23698  nmoleub2lem3  23699  pjthlem1  24020  ovolscalem1  24096  ovolscalem2  24097  ovolsca  24098  mbfmulc2lem  24230  itg2const2  24324  dvferm1lem  24566  abelthlem7  25012  logdivlti  25190  logdivle  25192  logcnlem3  25214  logcnlem4  25215  advlogexp  25225  cxpaddle  25320  cxploglim  25542  cxploglim2  25543  lgamgulmlem2  25594  lgamgulmlem3  25595  lgamucov  25602  ftalem1  25637  ftalem2  25638  basellem3  25647  fsumvma2  25777  chpval2  25781  chpchtsum  25782  chpub  25783  logfacrlim  25787  logexprlim  25788  efexple  25844  bposlem9  25855  chebbnd1lem2  26033  chebbnd1lem3  26034  chtppilim  26038  chpchtlim  26042  chpo1ubb  26044  rplogsumlem1  26047  rplogsumlem2  26048  rpvmasumlem  26050  dchrmusum2  26057  dchrvmasumlem2  26061  dchrisum0fno1  26074  dchrisum0lem1b  26078  dchrisum0lem1  26079  dchrisum0lem2a  26080  rplogsum  26090  mulog2sumlem1  26097  mulog2sumlem2  26098  vmalogdivsum2  26101  vmalogdivsum  26102  2vmadivsumlem  26103  log2sumbnd  26107  selberglem2  26109  selbergb  26112  selberg2b  26115  chpdifbndlem1  26116  selberg3lem1  26120  selberg3lem2  26121  selberg3  26122  selberg4lem1  26123  selberg4  26124  pntrsumo1  26128  selberg3r  26132  selberg4r  26133  selberg34r  26134  pntrlog2bndlem1  26140  pntrlog2bndlem2  26141  pntrlog2bndlem3  26142  pntrlog2bndlem4  26143  pntrlog2bndlem5  26144  pntrlog2bndlem6  26146  pntrlog2bnd  26147  pntpbnd1a  26148  pntpbnd2  26150  pntibndlem2  26154  pntibndlem3  26155  pntlemb  26160  pntlemg  26161  pntlemh  26162  pntlemn  26163  pntlemr  26165  pntlemj  26166  pntlemf  26168  pntlemk  26169  pntlemo  26170  pnt  26177  ostth2lem1  26181  ostth2lem4  26199  ostth3  26201  pjhthlem1  29153  esumcst  31330  dya2iocress  31540  dya2iocbrsiga  31541  dya2icobrsiga  31542  sxbrsigalem2  31552  probmeasb  31696  itg2addnclem3  34986  ftc1anclem7  35012  geomcau  35073  cntotbnd  35110  bfplem1  35136  fltnlta  39412  binomcxplemnotnn0  40843  divlt0gt0d  41706  lefldiveq  41713  ltmod  42071  0ellimcdiv  42082  wallispilem5  42502  stirlingr  42523  dirkercncflem1  42536  fourierdlem65  42604  hoiqssbllem2  43053
  Copyright terms: Public domain W3C validator