Theorem rehalfcld 12415

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028   / cdiv 11798  2c2 12227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235

This theorem is referenced by:  div4p1lem1div2  12423  flhalf  13780  fldiv4p1lem1div2  13785  fldiv4lem1div2uz2  13786  facavg  14254  recl  15063  crre  15067  geomulcvg  15832  resin4p  16096  recos4p  16097  resinhcl  16114  cos01bnd  16144  rpnnen2lem11  16182  ruclem1  16189  ruclem2  16190  ruclem3  16191  nno  16342  bitsp1  16391  prmreclem5  16882  4sqlem5  16904  4sqlem6  16905  4sqlem10  16909  4sqlem15  16921  4sqlem16  16922  blhalf  24388  metustexhalf  24539  cfilucfil  24542  nlmvscnlem2  24668  ioo2bl  24776  ioo2blex  24777  reperflem  24802  metnrmlem3  24845  ipcnlem2  25229  iscau3  25263  minveclem4  25417  ovolunlem1a  25481  dvferm1lem  25969  dvferm2lem  25971  lhop1lem  25998  ulmdvlem1  26383  radcnvle  26403  psercnlem1  26408  pserdvlem1  26410  pilem3  26436  coseq00topi  26484  cosordlem  26512  logtayl  26642  cxpcn3lem  26729  isosctrlem1  26800  chordthmlem4  26817  heron  26820  birthdaylem3  26935  cxp2limlem  26957  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamucov  27019  ftalem2  27055  chtub  27193  bcmono  27258  lgsqrlem2  27328  gausslemma2dlem1a  27346  gausslemma2dlem2  27348  gausslemma2dlem3  27349  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1a2  27371  2lgslem1c  27374  2sqlem8  27407  chpo1ubb  27462  dchrisum0fno1  27492  logdivsum  27514  mulog2sumlem1  27515  mulog2sumlem2  27516  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selberg4lem1  27541  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntpbnd1a  27566  pntibndlem2  27572  pntibndlem3  27573  pntlemg  27579  pntlemh  27580  minvecolem4  30969  nmcexi  32115  lt2addrd  32842  le2halvesd  32848  constrresqrtcl  33961  sqsscirc1  34092  tpr2rico  34096  dnibndlem12  36795  knoppndvlem21  36838  iooelexlt  37724  sin2h  37977  cos2h  37978  tan2h  37979  mblfinlem4  38027  itg2addnclem  38038  ftc1anclem7  38066  ftc1anc  38068  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p7  42559  sqrtcvallem3  44082  sqrtcvallem5  44084  sqrtcval  44085  oddfl  45726  dstregt0  45730  suplesup  45784  infleinflem1  45814  ioomidp  45959  lptre2pt  46083  0ellimcdiv  46092  limsupgtlem  46220  dvbdfbdioolem2  46372  dvbdfbdioo  46373  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem14  46457  stoweidlem24  46467  stoweidlem49  46492  stoweidlem52  46495  stoweidlem62  46505  dirker2re  46535  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem5  46555  fourierdlem10  46560  fourierdlem43  46593  fourierdlem56  46605  fourierdlem58  46607  fourierdlem62  46611  fourierdlem66  46615  fourierdlem68  46617  fourierdlem72  46621  fourierdlem76  46625  fourierdlem78  46627  fourierdlem79  46628  fourierdlem83  46632  fourierdlem87  46636  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  sge0xaddlem1  46876  smflimlem4  47217  2ltceilhalf  47795  ceilhalfgt1  47796  ceilhalfelfzo1  47797  2tceilhalfelfzo1  47799  ceilhalfnn  47803  gpgusgralem  48547  gpg3nbgrvtx0ALT  48568  gpg3kgrtriexlem1  48574  gpg3kgrtriexlem4  48577  gpg3kgrtriexlem6  48579  flnn0div2ge  49024  dignn0flhalflem2  49107  dignn0flhalf  49109