Theorem rehalfcld 10893

Description: Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
rehalfcld.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
rehalfcld	|- ( ph -> ( A / 2 ) e. RR )

Proof of Theorem rehalfcld

Step	Hyp	Ref	Expression
1		rehalfcld.1	. 2 |- ( ph -> A e. RR )
2		rehalfcl 10873	. 2 |- ( A e. RR -> ( A / 2 ) e. RR )
3	1, 2	syl 17	1 |- ( ph -> ( A / 2 ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1898  (class class class)co 6320   RRcr 9569   / cdiv 10302   2c2 10692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-po 4777  df-so 4778  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-2 10701

This theorem is referenced by:  flhalf  12100  facavg  12524  recl  13228  crre  13232  geomulcvg  13987  resin4p  14247  recos4p  14248  resinhcl  14265  cos01bnd  14295  rpnnen2lem11  14332  ruclem1  14338  ruclem2  14339  ruclem3  14340  bitsp1  14459  prmreclem5  14919  4sqlem5  14941  4sqlem6  14942  4sqlem10  14946  4sqlem15OLD  14958  4sqlem16OLD  14959  4sqlem15  14964  4sqlem16  14965  blhalf  21475  metustexhalf  21626  cfilucfil  21629  nlmvscnlem2  21743  ioo2bl  21866  ioo2blex  21867  reperflem  21891  metnrmlem3  21933  metnrmlem3OLD  21948  ipcnlem2  22270  iscau3  22303  minveclem4  22429  minveclem4OLD  22441  ovolunlem1a  22504  dvferm1lem  22992  dvferm2lem  22994  lhop1lem  23021  ulmdvlem1  23411  radcnvle  23431  psercnlem1  23436  pserdvlem1  23438  pilem3  23465  pilem3OLD  23466  coseq00topi  23513  cosordlem  23536  logtayl  23661  cxpcn3lem  23743  isosctrlem1  23803  chordthmlem4  23817  heron  23820  birthdaylem3  23935  cxp2limlem  23957  lgamgulmlem2  24011  lgamgulmlem3  24012  lgamucov  24019  ftalem2  24054  chtub  24196  bcmono  24261  lgsqrlem2  24326  lgsquadlem1  24338  lgsquadlem2  24339  2sqlem8  24356  chpo1ubb  24375  dchrisum0fno1  24405  logdivsum  24427  mulog2sumlem1  24428  mulog2sumlem2  24429  vmalogdivsum2  24432  vmalogdivsum  24433  2vmadivsumlem  24434  selberg4lem1  24454  selberg3r  24463  selberg4r  24464  selberg34r  24465  pntpbnd1a  24479  pntibndlem2  24485  pntibndlem3  24486  pntlemg  24492  pntlemh  24493  minvecolem4  26578  minvecolem4OLD  26588  nmcexi  27735  lt2addrd  28378  le2halvesd  28387  sqsscirc1  28765  tpr2rico  28769  iooelexlt  31811  sin2h  31981  cos2h  31982  tan2h  31983  mblfinlem4  32026  itg2addnclem  32039  ftc1anclem7  32069  ftc1anc  32071  oddfl  37562  dstregt0  37566  suplesup  37637  infleinflem1  37669  ioomidp  37700  lptre2pt  37806  0ellimcdiv  37816  dvbdfbdioolem2  37887  dvbdfbdioo  37888  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  stoweidlem14  37975  stoweidlem24  37985  stoweidlem49  38011  stoweidlem52  38014  stoweidlem62  38024  stoweidlem62OLD  38025  dirker2re  38055  dirkertrigeqlem3  38063  dirkertrigeq  38064  dirkercncflem1  38066  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem5  38075  fourierdlem10  38080  fourierdlem43  38115  fourierdlem56  38127  fourierdlem58  38129  fourierdlem62  38133  fourierdlem66  38137  fourierdlem68  38139  fourierdlem72  38143  fourierdlem76  38147  fourierdlem78  38149  fourierdlem79  38150  fourierdlem83  38154  fourierdlem87  38158  fourierdlem103  38174  fourierdlem104  38175  fourierdlem112  38183  sge0xaddlem1  38378  nno  40697  flnn0div2ge  40709  dignn0flhalflem2  40796  dignn0flhalf  40798