Theorem rehalfcld 12488

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7405  ℝcr 11128   / cdiv 11894  2c2 12295

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303

This theorem is referenced by:  div4p1lem1div2  12496  flhalf  13847  fldiv4p1lem1div2  13852  fldiv4lem1div2uz2  13853  facavg  14319  recl  15129  crre  15133  geomulcvg  15892  resin4p  16156  recos4p  16157  resinhcl  16174  cos01bnd  16204  rpnnen2lem11  16242  ruclem1  16249  ruclem2  16250  ruclem3  16251  nno  16401  bitsp1  16450  prmreclem5  16940  4sqlem5  16962  4sqlem6  16963  4sqlem10  16967  4sqlem15  16979  4sqlem16  16980  blhalf  24344  metustexhalf  24495  cfilucfil  24498  nlmvscnlem2  24624  ioo2bl  24732  ioo2blex  24733  reperflem  24758  metnrmlem3  24801  ipcnlem2  25196  iscau3  25230  minveclem4  25384  ovolunlem1a  25449  dvferm1lem  25940  dvferm2lem  25942  lhop1lem  25970  ulmdvlem1  26361  radcnvle  26381  psercnlem1  26387  pserdvlem1  26389  pilem3  26415  coseq00topi  26463  cosordlem  26491  logtayl  26621  cxpcn3lem  26709  isosctrlem1  26780  chordthmlem4  26797  heron  26800  birthdaylem3  26915  cxp2limlem  26938  lgamgulmlem2  26992  lgamgulmlem3  26993  lgamucov  27000  ftalem2  27036  chtub  27175  bcmono  27240  lgsqrlem2  27310  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a2  27353  2lgslem1c  27356  2sqlem8  27389  chpo1ubb  27444  dchrisum0fno1  27474  logdivsum  27496  mulog2sumlem1  27497  mulog2sumlem2  27498  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  selberg4lem1  27523  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntpbnd1a  27548  pntibndlem2  27554  pntibndlem3  27555  pntlemg  27561  pntlemh  27562  minvecolem4  30861  nmcexi  32007  lt2addrd  32728  le2halvesd  32733  constrresqrtcl  33811  sqsscirc1  33939  tpr2rico  33943  dnibndlem12  36507  knoppndvlem21  36550  iooelexlt  37380  sin2h  37634  cos2h  37635  tan2h  37636  mblfinlem4  37684  itg2addnclem  37695  ftc1anclem7  37723  ftc1anc  37725  3lexlogpow2ineq1  42071  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  aks4d1p1p2  42083  aks4d1p1p4  42084  aks4d1p1p7  42087  sqrtcvallem3  43662  sqrtcvallem5  43664  sqrtcval  43665  oddfl  45306  dstregt0  45310  suplesup  45366  infleinflem1  45397  ioomidp  45543  lptre2pt  45669  0ellimcdiv  45678  limsupgtlem  45806  dvbdfbdioolem2  45958  dvbdfbdioo  45959  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweidlem14  46043  stoweidlem24  46053  stoweidlem49  46078  stoweidlem52  46081  stoweidlem62  46091  dirker2re  46121  dirkertrigeqlem3  46129  dirkertrigeq  46130  dirkercncflem1  46132  dirkercncflem2  46133  dirkercncflem4  46135  fourierdlem5  46141  fourierdlem10  46146  fourierdlem43  46179  fourierdlem56  46191  fourierdlem58  46193  fourierdlem62  46197  fourierdlem66  46201  fourierdlem68  46203  fourierdlem72  46207  fourierdlem76  46211  fourierdlem78  46213  fourierdlem79  46214  fourierdlem83  46218  fourierdlem87  46222  fourierdlem103  46238  fourierdlem104  46239  fourierdlem112  46247  sge0xaddlem1  46462  smflimlem4  46803  2ltceilhalf  47357  ceilhalfgt1  47358  ceilhalfelfzo1  47359  2tceilhalfelfzo1  47361  ceilhalfnn  47365  gpgusgralem  48060  gpg3nbgrvtx0ALT  48079  gpg3kgrtriexlem1  48085  gpg3kgrtriexlem4  48088  gpg3kgrtriexlem6  48090  flnn0div2ge  48513  dignn0flhalflem2  48596  dignn0flhalf  48598