Theorem rehalfcld 12429

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   / cdiv 11835  2c2 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249

This theorem is referenced by:  div4p1lem1div2  12437  flhalf  13792  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  facavg  14266  recl  15076  crre  15080  geomulcvg  15842  resin4p  16106  recos4p  16107  resinhcl  16124  cos01bnd  16154  rpnnen2lem11  16192  ruclem1  16199  ruclem2  16200  ruclem3  16201  nno  16352  bitsp1  16401  prmreclem5  16891  4sqlem5  16913  4sqlem6  16914  4sqlem10  16918  4sqlem15  16930  4sqlem16  16931  blhalf  24293  metustexhalf  24444  cfilucfil  24447  nlmvscnlem2  24573  ioo2bl  24681  ioo2blex  24682  reperflem  24707  metnrmlem3  24750  ipcnlem2  25144  iscau3  25178  minveclem4  25332  ovolunlem1a  25397  dvferm1lem  25888  dvferm2lem  25890  lhop1lem  25918  ulmdvlem1  26309  radcnvle  26329  psercnlem1  26335  pserdvlem1  26337  pilem3  26363  coseq00topi  26411  cosordlem  26439  logtayl  26569  cxpcn3lem  26657  isosctrlem1  26728  chordthmlem4  26745  heron  26748  birthdaylem3  26863  cxp2limlem  26886  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamucov  26948  ftalem2  26984  chtub  27123  bcmono  27188  lgsqrlem2  27258  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a2  27301  2lgslem1c  27304  2sqlem8  27337  chpo1ubb  27392  dchrisum0fno1  27422  logdivsum  27444  mulog2sumlem1  27445  mulog2sumlem2  27446  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  selberg4lem1  27471  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntpbnd1a  27496  pntibndlem2  27502  pntibndlem3  27503  pntlemg  27509  pntlemh  27510  minvecolem4  30809  nmcexi  31955  lt2addrd  32674  le2halvesd  32679  constrresqrtcl  33767  sqsscirc1  33898  tpr2rico  33902  dnibndlem12  36477  knoppndvlem21  36520  iooelexlt  37350  sin2h  37604  cos2h  37605  tan2h  37606  mblfinlem4  37654  itg2addnclem  37665  ftc1anclem7  37693  ftc1anc  37695  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p7  42062  sqrtcvallem3  43627  sqrtcvallem5  43629  sqrtcval  43630  oddfl  45276  dstregt0  45280  suplesup  45335  infleinflem1  45366  ioomidp  45512  lptre2pt  45638  0ellimcdiv  45647  limsupgtlem  45775  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem14  46012  stoweidlem24  46022  stoweidlem49  46047  stoweidlem52  46050  stoweidlem62  46060  dirker2re  46090  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem5  46110  fourierdlem10  46115  fourierdlem43  46148  fourierdlem56  46160  fourierdlem58  46162  fourierdlem62  46166  fourierdlem66  46170  fourierdlem68  46172  fourierdlem72  46176  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem83  46187  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  sge0xaddlem1  46431  smflimlem4  46772  2ltceilhalf  47329  ceilhalfgt1  47330  ceilhalfelfzo1  47331  2tceilhalfelfzo1  47333  ceilhalfnn  47337  gpgusgralem  48047  gpg3nbgrvtx0ALT  48068  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  flnn0div2ge  48522  dignn0flhalflem2  48605  dignn0flhalf  48607