Theorem halfre 12345

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 12210	. 2 ⊢ 2 ∈ ℝ
2		2ne0 12240	. 2 ⊢ 2 ≠ 0
3	1, 2	rereccli 11897	1 ⊢ (1 / 2) ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7355  ℝcr 11016  1c1 11018   / cdiv 11785  2c2 12191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-div 11786  df-nn 12137  df-2 12199

This theorem is referenced by:  halfge0  12348  2tnp1ge0ge0  13740  rddif  15255  absrdbnd  15256  geo2sum  15787  geo2lim  15789  geoihalfsum  15796  efcllem  15991  ege2le3  16004  rpnnen2lem12  16141  oddge22np1  16267  ltoddhalfle  16279  halfleoddlt  16280  bitsp1o  16351  prmreclem5  16839  prmreclem6  16840  iihalf1  24872  iihalf1cn  24873  iihalf1cnOLD  24874  iihalf2  24875  iihalf2cn  24876  iihalf2cnOLD  24877  elii1  24878  elii2  24879  htpycc  24926  pcoval1  24960  pco0  24961  pco1  24962  pcoval2  24963  pcocn  24964  pcohtpylem  24966  pcopt  24969  pcopt2  24970  pcoass  24971  pcorevlem  24973  iscmet3lem3  25237  mbfi1fseqlem6  25668  itg2monolem3  25700  aaliou3lem1  26297  aaliou3lem2  26298  aaliou3lem3  26299  cxpsqrtlem  26658  cxpsqrt  26659  logsqrt  26660  sqrt2cxp2logb9e3  26756  ang180lem1  26766  asinsin  26849  birthday  26911  gausslemma2dlem1a  27323  chebbnd1  27430  chtppilim  27433  mulog2sumlem2  27493  opsqrlem4  32144  constrrecl  33854  logdivsqrle  34735  subfacval3  35305  dnicld1  36588  dnizeq0  36591  dnizphlfeqhlf  36592  rddif2  36593  dnibndlem2  36595  dnibndlem3  36596  dnibndlem4  36597  dnibndlem5  36598  dnibndlem6  36599  dnibndlem7  36600  dnibndlem8  36601  dnibndlem9  36602  dnibndlem10  36603  dnibndlem11  36604  dnibndlem12  36605  dnibndlem13  36606  dnibnd  36607  knoppcnlem4  36612  cnndvlem1  36653  iccioo01  37444  cntotbnd  37909  halffl  45460  stoweidlem5  46165  stoweidlem14  46174  stoweidlem28  46188  dirkertrigeqlem2  46259  dirkeritg  46262  dirkercncflem2  46264  fourierdlem18  46285  fourierdlem66  46332  fourierdlem78  46344  fourierdlem83  46349  fourierdlem87  46353  fourierdlem104  46370  ceilhalf1  47496  zofldiv2ALTV  47824  zofldiv2  48693  sepfsepc  49089