Theorem rehalfcld 12492

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  ℝcr 11139   / cdiv 11903  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-2 12308

This theorem is referenced by:  div4p1lem1div2  12500  flhalf  13831  fldiv4p1lem1div2  13836  fldiv4lem1div2uz2  13837  facavg  14296  recl  15093  crre  15097  geomulcvg  15858  resin4p  16118  recos4p  16119  resinhcl  16136  cos01bnd  16166  rpnnen2lem11  16204  ruclem1  16211  ruclem2  16212  ruclem3  16213  nno  16362  bitsp1  16409  prmreclem5  16892  4sqlem5  16914  4sqlem6  16915  4sqlem10  16919  4sqlem15  16931  4sqlem16  16932  blhalf  24355  metustexhalf  24509  cfilucfil  24512  nlmvscnlem2  24646  ioo2bl  24753  ioo2blex  24754  reperflem  24778  metnrmlem3  24821  ipcnlem2  25216  iscau3  25250  minveclem4  25404  ovolunlem1a  25469  dvferm1lem  25960  dvferm2lem  25962  lhop1lem  25990  ulmdvlem1  26381  radcnvle  26401  psercnlem1  26407  pserdvlem1  26409  pilem3  26435  coseq00topi  26482  cosordlem  26509  logtayl  26639  cxpcn3lem  26727  isosctrlem1  26795  chordthmlem4  26812  heron  26815  birthdaylem3  26930  cxp2limlem  26953  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamucov  27015  ftalem2  27051  chtub  27190  bcmono  27255  lgsqrlem2  27325  gausslemma2dlem1a  27343  gausslemma2dlem2  27345  gausslemma2dlem3  27346  lgsquadlem1  27358  lgsquadlem2  27359  2lgslem1a2  27368  2lgslem1c  27371  2sqlem8  27404  chpo1ubb  27459  dchrisum0fno1  27489  logdivsum  27511  mulog2sumlem1  27512  mulog2sumlem2  27513  vmalogdivsum2  27516  vmalogdivsum  27517  2vmadivsumlem  27518  selberg4lem1  27538  selberg3r  27547  selberg4r  27548  selberg34r  27549  pntpbnd1a  27563  pntibndlem2  27569  pntibndlem3  27570  pntlemg  27576  pntlemh  27577  minvecolem4  30762  nmcexi  31908  lt2addrd  32603  le2halvesd  32607  sqsscirc1  33637  tpr2rico  33641  dnibndlem12  36092  knoppndvlem21  36135  iooelexlt  36969  sin2h  37211  cos2h  37212  tan2h  37213  mblfinlem4  37261  itg2addnclem  37272  ftc1anclem7  37300  ftc1anc  37302  3lexlogpow2ineq1  41658  3lexlogpow2ineq2  41659  3lexlogpow5ineq5  41660  aks4d1p1p2  41670  aks4d1p1p4  41671  aks4d1p1p7  41674  sqrtcvallem3  43207  sqrtcvallem5  43209  sqrtcval  43210  oddfl  44794  dstregt0  44798  suplesup  44856  infleinflem1  44887  ioomidp  45034  lptre2pt  45163  0ellimcdiv  45172  limsupgtlem  45300  dvbdfbdioolem2  45452  dvbdfbdioo  45453  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  stoweidlem14  45537  stoweidlem24  45547  stoweidlem49  45572  stoweidlem52  45575  stoweidlem62  45585  dirker2re  45615  dirkertrigeqlem3  45623  dirkertrigeq  45624  dirkercncflem1  45626  dirkercncflem2  45627  dirkercncflem4  45629  fourierdlem5  45635  fourierdlem10  45640  fourierdlem43  45673  fourierdlem56  45685  fourierdlem58  45687  fourierdlem62  45691  fourierdlem66  45695  fourierdlem68  45697  fourierdlem72  45701  fourierdlem76  45705  fourierdlem78  45707  fourierdlem79  45708  fourierdlem83  45712  fourierdlem87  45716  fourierdlem103  45732  fourierdlem104  45733  fourierdlem112  45741  sge0xaddlem1  45956  smflimlem4  46297  flnn0div2ge  47789  dignn0flhalflem2  47872  dignn0flhalf  47874