Theorem rehalfcld 12486

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

Step	Hyp	Ref	Expression
1		rehalfcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		rehalfcl 12466	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   / cdiv 11866  2c2 12290

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-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  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-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  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-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  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-nn 12229  df-2 12298

This theorem is referenced by:  div4p1lem1div2  12494  flhalf  13859  fldiv4p1lem1div2  13864  fldiv4lem1div2uz2  13865  facavg  14333  recl  15157  crre  15161  geomulcvg  15926  resin4p  16189  recos4p  16190  resinhcl  16207  cos01bnd  16237  rpnnen2lem11  16275  ruclem1  16282  ruclem2  16283  ruclem3  16284  nno  16435  bitsp1  16484  prmreclem5  16975  4sqlem5  16997  4sqlem6  16998  4sqlem10  17002  4sqlem15  17014  4sqlem16  17015  blhalf  24562  metustexhalf  24713  cfilucfil  24716  nlmvscnlem2  24842  ioo2bl  24950  ioo2blex  24951  reperflem  24976  metnrmlem3  25019  ipcnlem2  25403  iscau3  25437  minveclem4  25591  ovolunlem1a  25655  dvferm1lem  26143  dvferm2lem  26145  lhop1lem  26172  ulmdvlem1  26563  radcnvle  26583  psercnlem1  26588  pserdvlem1  26590  pilem3  26616  coseq00topi  26667  cosordlem  26695  logtayl  26825  cxpcn3lem  26912  isosctrlem1  26983  chordthmlem4  27000  heron  27003  birthdaylem3  27118  cxp2limlem  27140  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamucov  27202  ftalem2  27238  chtub  27376  bcmono  27441  lgsqrlem2  27511  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem3  27532  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1a2  27554  2lgslem1c  27557  2sqlem8  27590  chpo1ubb  27645  dchrisum0fno1  27675  logdivsum  27697  mulog2sumlem1  27698  mulog2sumlem2  27699  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  selberg4lem1  27724  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntpbnd1a  27749  pntibndlem2  27755  pntibndlem3  27756  pntlemg  27762  pntlemh  27763  minvecolem4  31232  nmcexi  32378  lt2addrd  33095  le2halvesd  33101  constrresqrtcl  34167  sqsscirc1  34298  tpr2rico  34302  dnibndlem12  37098  knoppndvlem21  37141  iooelexlt  38028  sin2h  38281  cos2h  38282  tan2h  38283  mblfinlem4  38331  itg2addnclem  38342  ftc1anclem7  38370  ftc1anc  38372  3lexlogpow2ineq1  42845  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p7  42861  sqrtcvallem3  44384  sqrtcvallem5  44386  sqrtcval  44387  oddfl  46017  dstregt0  46021  suplesup  46075  infleinflem1  46105  ioomidp  46250  lptre2pt  46374  0ellimcdiv  46383  limsupgtlem  46511  dvbdfbdioolem2  46663  dvbdfbdioo  46664  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  stoweidlem14  46748  stoweidlem24  46758  stoweidlem49  46783  stoweidlem52  46786  stoweidlem62  46796  dirker2re  46826  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkercncflem1  46837  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem5  46846  fourierdlem10  46851  fourierdlem43  46884  fourierdlem56  46896  fourierdlem58  46898  fourierdlem62  46902  fourierdlem66  46906  fourierdlem68  46908  fourierdlem72  46912  fourierdlem76  46916  fourierdlem78  46918  fourierdlem79  46919  fourierdlem83  46923  fourierdlem87  46927  fourierdlem103  46943  fourierdlem104  46944  fourierdlem112  46952  sge0xaddlem1  47167  smflimlem4  47508  2ltceilhalf  48089  ceilhalfgt1  48090  ceilhalfelfzo1  48091  2tceilhalfelfzo1  48093  ceilhalfnn  48097  gpgusgralem  48841  gpg3nbgrvtx0ALT  48862  gpg3kgrtriexlem1  48868  gpg3kgrtriexlem4  48871  gpg3kgrtriexlem6  48873  flnn0div2ge  49333  dignn0flhalflem2  49416  dignn0flhalf  49418