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

Theorem rehalfcld 11503
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 11482 . 2 (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
31, 2syl 17 1 (𝜑 → (𝐴 / 2) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2148  (class class class)co 6812  cr 10158   / cdiv 10907  2c2 11293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-po 5184  df-so 5185  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-2 11302
This theorem is referenced by:  div4p1lem1div2  11511  flhalf  12861  fldiv4p1lem1div2  12866  fldiv4lem1div2uz2  12867  facavg  13314  recl  14080  crre  14084  geomulcvg  14836  resin4p  15096  recos4p  15097  resinhcl  15114  cos01bnd  15144  rpnnen2lem11  15181  ruclem1  15188  ruclem2  15189  ruclem3  15190  nno  15328  bitsp1  15382  prmreclem5  15851  4sqlem5  15873  4sqlem6  15874  4sqlem10  15878  4sqlem15  15890  4sqlem16  15891  blhalf  22450  metustexhalf  22601  cfilucfil  22604  nlmvscnlem2  22729  ioo2bl  22836  ioo2blex  22837  reperflem  22861  metnrmlem3  22904  ipcnlem2  23282  iscau3  23315  minveclem4  23442  ovolunlem1a  23504  dvferm1lem  23988  dvferm2lem  23990  lhop1lem  24017  ulmdvlem1  24395  radcnvle  24415  psercnlem1  24420  pserdvlem1  24422  pilem3  24448  pilem3OLD  24449  coseq00topi  24496  cosordlem  24519  logtayl  24648  cxpcn3lem  24730  isosctrlem1  24790  chordthmlem4  24804  heron  24807  birthdaylem3  24922  cxp2limlem  24944  lgamgulmlem2  24998  lgamgulmlem3  24999  lgamucov  25006  ftalem2  25042  chtub  25179  bcmono  25244  lgsqrlem2  25314  gausslemma2dlem1a  25332  gausslemma2dlem2  25334  gausslemma2dlem3  25335  lgsquadlem1  25347  lgsquadlem2  25348  2lgslem1a2  25357  2lgslem1c  25360  2sqlem8  25393  chpo1ubb  25412  dchrisum0fno1  25442  logdivsum  25464  mulog2sumlem1  25465  mulog2sumlem2  25466  vmalogdivsum2  25469  vmalogdivsum  25470  2vmadivsumlem  25471  selberg4lem1  25491  selberg3r  25500  selberg4r  25501  selberg34r  25502  pntpbnd1a  25516  pntibndlem2  25522  pntibndlem3  25523  pntlemg  25529  pntlemh  25530  minvecolem4  28093  nmcexi  29242  lt2addrd  29873  le2halvesd  29877  sqsscirc1  30311  tpr2rico  30315  dnibndlem12  32833  knoppndvlem21  32877  iooelexlt  33564  sin2h  33749  cos2h  33750  tan2h  33751  mblfinlem4  33799  itg2addnclem  33810  ftc1anclem7  33840  ftc1anc  33842  oddfl  40015  dstregt0  40019  suplesup  40079  infleinflem1  40110  ioomidp  40265  lptre2pt  40396  0ellimcdiv  40405  limsupgtlem  40533  dvbdfbdioolem2  40668  dvbdfbdioo  40669  ioodvbdlimc1lem2  40671  ioodvbdlimc2lem  40673  stoweidlem14  40754  stoweidlem24  40764  stoweidlem49  40789  stoweidlem52  40792  stoweidlem62  40802  dirker2re  40832  dirkertrigeqlem3  40840  dirkertrigeq  40841  dirkercncflem1  40843  dirkercncflem2  40844  dirkercncflem4  40846  fourierdlem5  40852  fourierdlem10  40857  fourierdlem43  40890  fourierdlem56  40902  fourierdlem58  40904  fourierdlem62  40908  fourierdlem66  40912  fourierdlem68  40914  fourierdlem72  40918  fourierdlem76  40922  fourierdlem78  40924  fourierdlem79  40925  fourierdlem83  40929  fourierdlem87  40933  fourierdlem103  40949  fourierdlem104  40950  fourierdlem112  40958  sge0xaddlem1  41173  smflimlem4  41508  flnn0div2ge  42879  dignn0flhalflem2  42962  dignn0flhalf  42964
  Copyright terms: Public domain W3C validator