Theorem rehalfcld 11633

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 6924  ℝcr 10273   / cdiv 11034  2c2 11434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-po 5276  df-so 5277  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-2 11442

This theorem is referenced by:  div4p1lem1div2  11641  flhalf  12954  fldiv4p1lem1div2  12959  fldiv4lem1div2uz2  12960  facavg  13410  recl  14261  crre  14265  geomulcvg  15015  resin4p  15274  recos4p  15275  resinhcl  15292  cos01bnd  15322  rpnnen2lem11  15361  ruclem1  15368  ruclem2  15369  ruclem3  15370  nno  15516  bitsp1  15563  prmreclem5  16032  4sqlem5  16054  4sqlem6  16055  4sqlem10  16059  4sqlem15  16071  4sqlem16  16072  blhalf  22622  metustexhalf  22773  cfilucfil  22776  nlmvscnlem2  22901  ioo2bl  23008  ioo2blex  23009  reperflem  23033  metnrmlem3  23076  ipcnlem2  23454  iscau3  23488  minveclem4  23642  ovolunlem1a  23704  dvferm1lem  24188  dvferm2lem  24190  lhop1lem  24217  ulmdvlem1  24595  radcnvle  24615  psercnlem1  24620  pserdvlem1  24622  pilem3  24648  pilem3OLD  24649  coseq00topi  24696  cosordlem  24719  logtayl  24847  cxpcn3lem  24932  isosctrlem1  25000  chordthmlem4  25017  heron  25020  birthdaylem3  25136  cxp2limlem  25158  lgamgulmlem2  25212  lgamgulmlem3  25213  lgamucov  25220  ftalem2  25256  chtub  25393  bcmono  25458  lgsqrlem2  25528  gausslemma2dlem1a  25546  gausslemma2dlem2  25548  gausslemma2dlem3  25549  lgsquadlem1  25561  lgsquadlem2  25562  2lgslem1a2  25571  2lgslem1c  25574  2sqlem8  25607  chpo1ubb  25626  dchrisum0fno1  25656  logdivsum  25678  mulog2sumlem1  25679  mulog2sumlem2  25680  vmalogdivsum2  25683  vmalogdivsum  25684  2vmadivsumlem  25685  selberg4lem1  25705  selberg3r  25714  selberg4r  25715  selberg34r  25716  pntpbnd1a  25730  pntibndlem2  25736  pntibndlem3  25737  pntlemg  25743  pntlemh  25744  minvecolem4  28312  nmcexi  29461  lt2addrd  30085  le2halvesd  30089  sqsscirc1  30556  tpr2rico  30560  dnibndlem12  33066  knoppndvlem21  33109  iooelexlt  33808  sin2h  34029  cos2h  34030  tan2h  34031  mblfinlem4  34080  itg2addnclem  34091  ftc1anclem7  34121  ftc1anc  34123  oddfl  40409  dstregt0  40413  suplesup  40473  infleinflem1  40504  ioomidp  40659  lptre2pt  40790  0ellimcdiv  40799  limsupgtlem  40927  dvbdfbdioolem2  41082  dvbdfbdioo  41083  ioodvbdlimc1lem2  41085  ioodvbdlimc2lem  41087  stoweidlem14  41168  stoweidlem24  41178  stoweidlem49  41203  stoweidlem52  41206  stoweidlem62  41216  dirker2re  41246  dirkertrigeqlem3  41254  dirkertrigeq  41255  dirkercncflem1  41257  dirkercncflem2  41258  dirkercncflem4  41260  fourierdlem5  41266  fourierdlem10  41271  fourierdlem43  41304  fourierdlem56  41316  fourierdlem58  41318  fourierdlem62  41322  fourierdlem66  41326  fourierdlem68  41328  fourierdlem72  41332  fourierdlem76  41336  fourierdlem78  41338  fourierdlem79  41339  fourierdlem83  41343  fourierdlem87  41347  fourierdlem103  41363  fourierdlem104  41364  fourierdlem112  41372  sge0xaddlem1  41584  smflimlem4  41919  flnn0div2ge  43352  dignn0flhalflem2  43435  dignn0flhalf  43437