Theorem halfre 12233

Description: One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
halfre	⊢ (1 / 2) ∈ ℝ

Proof of Theorem halfre

Step	Hyp	Ref	Expression
1		2re 12093	. 2 ⊢ 2 ∈ ℝ
2		2ne0 12123	. 2 ⊢ 2 ≠ 0
3	1, 2	rereccli 11786	1 ⊢ (1 / 2) ∈ ℝ

Syntax hints:   ∈ wcel 2104  (class class class)co 7307  ℝcr 10916  1c1 10918   / cdiv 11678  2c2 12074

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993  ax-pre-mulgt0 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061  df-sub 11253  df-neg 11254  df-div 11679  df-2 12082

This theorem is referenced by:  halfge0  12236  2tnp1ge0ge0  13595  rddif  15097  absrdbnd  15098  geo2sum  15630  geo2lim  15632  geoihalfsum  15639  efcllem  15832  ege2le3  15844  rpnnen2lem12  15979  oddge22np1  16103  ltoddhalfle  16115  halfleoddlt  16116  bitsp1o  16185  prmreclem5  16666  prmreclem6  16667  iihalf1  24139  iihalf1cn  24140  iihalf2  24141  iihalf2cn  24142  elii1  24143  elii2  24144  htpycc  24188  pcoval1  24221  pco0  24222  pco1  24223  pcoval2  24224  pcocn  24225  pcohtpylem  24227  pcopt  24230  pcopt2  24231  pcoass  24232  pcorevlem  24234  iscmet3lem3  24499  mbfi1fseqlem6  24930  itg2monolem3  24962  aaliou3lem1  25547  aaliou3lem2  25548  aaliou3lem3  25549  cxpsqrtlem  25902  cxpsqrt  25903  logsqrt  25904  sqrt2cxp2logb9e3  25994  ang180lem1  26004  asinsin  26087  birthday  26149  gausslemma2dlem1a  26558  chebbnd1  26665  chtppilim  26668  mulog2sumlem2  26728  opsqrlem4  30550  logdivsqrle  32675  subfacval3  33196  dnicld1  34697  dnizeq0  34700  dnizphlfeqhlf  34701  rddif2  34702  dnibndlem2  34704  dnibndlem3  34705  dnibndlem4  34706  dnibndlem5  34707  dnibndlem6  34708  dnibndlem7  34709  dnibndlem8  34710  dnibndlem9  34711  dnibndlem10  34712  dnibndlem11  34713  dnibndlem12  34714  dnibndlem13  34715  dnibnd  34716  knoppcnlem4  34721  cnndvlem1  34762  iccioo01  35542  cntotbnd  35998  halffl  42883  stoweidlem5  43595  stoweidlem14  43604  stoweidlem28  43618  dirkertrigeqlem2  43689  dirkeritg  43692  dirkercncflem2  43694  fourierdlem18  43715  fourierdlem66  43762  fourierdlem78  43774  fourierdlem83  43779  fourierdlem87  43783  fourierdlem104  43800  zofldiv2ALTV  45172  zofldiv2  45935  sepfsepc  46279