Theorem rehalfcld 12230

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 12209	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7267  ℝcr 10880   / cdiv 11642  2c2 12038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-resscn 10938  ax-1cn 10939  ax-icn 10940  ax-addcl 10941  ax-addrcl 10942  ax-mulcl 10943  ax-mulrcl 10944  ax-mulcom 10945  ax-addass 10946  ax-mulass 10947  ax-distr 10948  ax-i2m1 10949  ax-1ne0 10950  ax-1rid 10951  ax-rnegex 10952  ax-rrecex 10953  ax-cnre 10954  ax-pre-lttri 10955  ax-pre-lttrn 10956  ax-pre-ltadd 10957  ax-pre-mulgt0 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-po 5498  df-so 5499  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-riota 7224  df-ov 7270  df-oprab 7271  df-mpo 7272  df-er 8485  df-en 8721  df-dom 8722  df-sdom 8723  df-pnf 11021  df-mnf 11022  df-xr 11023  df-ltxr 11024  df-le 11025  df-sub 11217  df-neg 11218  df-div 11643  df-2 12046

This theorem is referenced by:  div4p1lem1div2  12238  flhalf  13560  fldiv4p1lem1div2  13565  fldiv4lem1div2uz2  13566  facavg  14025  recl  14831  crre  14835  geomulcvg  15598  resin4p  15857  recos4p  15858  resinhcl  15875  cos01bnd  15905  rpnnen2lem11  15943  ruclem1  15950  ruclem2  15951  ruclem3  15952  nno  16101  bitsp1  16148  prmreclem5  16631  4sqlem5  16653  4sqlem6  16654  4sqlem10  16658  4sqlem15  16670  4sqlem16  16671  blhalf  23568  metustexhalf  23722  cfilucfil  23725  nlmvscnlem2  23859  ioo2bl  23966  ioo2blex  23967  reperflem  23991  metnrmlem3  24034  ipcnlem2  24418  iscau3  24452  minveclem4  24606  ovolunlem1a  24670  dvferm1lem  25158  dvferm2lem  25160  lhop1lem  25187  ulmdvlem1  25569  radcnvle  25589  psercnlem1  25594  pserdvlem1  25596  pilem3  25622  coseq00topi  25669  cosordlem  25696  logtayl  25825  cxpcn3lem  25910  isosctrlem1  25978  chordthmlem4  25995  heron  25998  birthdaylem3  26113  cxp2limlem  26135  lgamgulmlem2  26189  lgamgulmlem3  26190  lgamucov  26197  ftalem2  26233  chtub  26370  bcmono  26435  lgsqrlem2  26505  gausslemma2dlem1a  26523  gausslemma2dlem2  26525  gausslemma2dlem3  26526  lgsquadlem1  26538  lgsquadlem2  26539  2lgslem1a2  26548  2lgslem1c  26551  2sqlem8  26584  chpo1ubb  26639  dchrisum0fno1  26669  logdivsum  26691  mulog2sumlem1  26692  mulog2sumlem2  26693  vmalogdivsum2  26696  vmalogdivsum  26697  2vmadivsumlem  26698  selberg4lem1  26718  selberg3r  26727  selberg4r  26728  selberg34r  26729  pntpbnd1a  26743  pntibndlem2  26749  pntibndlem3  26750  pntlemg  26756  pntlemh  26757  minvecolem4  29250  nmcexi  30396  lt2addrd  31082  le2halvesd  31086  sqsscirc1  31866  tpr2rico  31870  dnibndlem12  34677  knoppndvlem21  34720  iooelexlt  35541  sin2h  35775  cos2h  35776  tan2h  35777  mblfinlem4  35825  itg2addnclem  35836  ftc1anclem7  35864  ftc1anc  35866  3lexlogpow2ineq1  40074  3lexlogpow2ineq2  40075  3lexlogpow5ineq5  40076  aks4d1p1p2  40086  aks4d1p1p4  40087  aks4d1p1p7  40090  sqrtcvallem3  41227  sqrtcvallem5  41229  sqrtcval  41230  oddfl  42797  dstregt0  42801  suplesup  42859  infleinflem1  42890  ioomidp  43033  lptre2pt  43162  0ellimcdiv  43171  limsupgtlem  43299  dvbdfbdioolem2  43451  dvbdfbdioo  43452  ioodvbdlimc1lem2  43454  ioodvbdlimc2lem  43456  stoweidlem14  43536  stoweidlem24  43546  stoweidlem49  43571  stoweidlem52  43574  stoweidlem62  43584  dirker2re  43614  dirkertrigeqlem3  43622  dirkertrigeq  43623  dirkercncflem1  43625  dirkercncflem2  43626  dirkercncflem4  43628  fourierdlem5  43634  fourierdlem10  43639  fourierdlem43  43672  fourierdlem56  43684  fourierdlem58  43686  fourierdlem62  43690  fourierdlem66  43694  fourierdlem68  43696  fourierdlem72  43700  fourierdlem76  43704  fourierdlem78  43706  fourierdlem79  43707  fourierdlem83  43711  fourierdlem87  43715  fourierdlem103  43731  fourierdlem104  43732  fourierdlem112  43740  sge0xaddlem1  43952  smflimlem4  44287  flnn0div2ge  45857  dignn0flhalflem2  45940  dignn0flhalf  45942