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

Theorem rehalfcld 11872
Description: Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
rehalfcld.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
rehalfcld (𝜑 → (𝐴 / 2) ∈ ℝ)

Proof of Theorem rehalfcld
StepHypRef Expression
1 rehalfcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 rehalfcl 11851 . 2 (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
31, 2syl 17 1 (𝜑 → (𝐴 / 2) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cr 10524   / cdiv 11285  2c2 11680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-2 11688
This theorem is referenced by:  div4p1lem1div2  11880  flhalf  13188  fldiv4p1lem1div2  13193  fldiv4lem1div2uz2  13194  facavg  13649  recl  14457  crre  14461  geomulcvg  15220  resin4p  15479  recos4p  15480  resinhcl  15497  cos01bnd  15527  rpnnen2lem11  15565  ruclem1  15572  ruclem2  15573  ruclem3  15574  nno  15721  bitsp1  15768  prmreclem5  16244  4sqlem5  16266  4sqlem6  16267  4sqlem10  16271  4sqlem15  16283  4sqlem16  16284  blhalf  22942  metustexhalf  23093  cfilucfil  23096  nlmvscnlem2  23221  ioo2bl  23328  ioo2blex  23329  reperflem  23353  metnrmlem3  23396  ipcnlem2  23774  iscau3  23808  minveclem4  23962  ovolunlem1a  24024  dvferm1lem  24508  dvferm2lem  24510  lhop1lem  24537  ulmdvlem1  24915  radcnvle  24935  psercnlem1  24940  pserdvlem1  24942  pilem3  24968  coseq00topi  25015  cosordlem  25042  logtayl  25170  cxpcn3lem  25255  isosctrlem1  25323  chordthmlem4  25340  heron  25343  birthdaylem3  25458  cxp2limlem  25480  lgamgulmlem2  25534  lgamgulmlem3  25535  lgamucov  25542  ftalem2  25578  chtub  25715  bcmono  25780  lgsqrlem2  25850  gausslemma2dlem1a  25868  gausslemma2dlem2  25870  gausslemma2dlem3  25871  lgsquadlem1  25883  lgsquadlem2  25884  2lgslem1a2  25893  2lgslem1c  25896  2sqlem8  25929  chpo1ubb  25984  dchrisum0fno1  26014  logdivsum  26036  mulog2sumlem1  26037  mulog2sumlem2  26038  vmalogdivsum2  26041  vmalogdivsum  26042  2vmadivsumlem  26043  selberg4lem1  26063  selberg3r  26072  selberg4r  26073  selberg34r  26074  pntpbnd1a  26088  pntibndlem2  26094  pntibndlem3  26095  pntlemg  26101  pntlemh  26102  minvecolem4  28584  nmcexi  29730  lt2addrd  30401  le2halvesd  30405  sqsscirc1  31050  tpr2rico  31054  dnibndlem12  33725  knoppndvlem21  33768  iooelexlt  34525  sin2h  34763  cos2h  34764  tan2h  34765  mblfinlem4  34813  itg2addnclem  34824  ftc1anclem7  34854  ftc1anc  34856  oddfl  41419  dstregt0  41423  suplesup  41483  infleinflem1  41514  ioomidp  41666  lptre2pt  41797  0ellimcdiv  41806  limsupgtlem  41934  dvbdfbdioolem2  42090  dvbdfbdioo  42091  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stoweidlem14  42176  stoweidlem24  42186  stoweidlem49  42211  stoweidlem52  42214  stoweidlem62  42224  dirker2re  42254  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncflem1  42265  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem5  42274  fourierdlem10  42279  fourierdlem43  42312  fourierdlem56  42324  fourierdlem58  42326  fourierdlem62  42330  fourierdlem66  42334  fourierdlem68  42336  fourierdlem72  42340  fourierdlem76  42344  fourierdlem78  42346  fourierdlem79  42347  fourierdlem83  42351  fourierdlem87  42355  fourierdlem103  42371  fourierdlem104  42372  fourierdlem112  42380  sge0xaddlem1  42592  smflimlem4  42927  flnn0div2ge  44521  dignn0flhalflem2  44604  dignn0flhalf  44606
  Copyright terms: Public domain W3C validator