Theorem halfre 11845

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 11705	. 2 ⊢ 2 ∈ ℝ
2		2ne0 11735	. 2 ⊢ 2 ≠ 0
3	1, 2	rereccli 11398	1 ⊢ (1 / 2) ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7149  ℝcr 10529  1c1 10531   / cdiv 11290  2c2 11686

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-er 8282  df-en 8503  df-dom 8504  df-sdom 8505  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-2 11694

This theorem is referenced by:  halfge0  11848  2tnp1ge0ge0  13196  rddif  14695  absrdbnd  14696  geo2sum  15224  geo2lim  15226  geoihalfsum  15233  efcllem  15426  ege2le3  15438  rpnnen2lem12  15573  oddge22np1  15693  ltoddhalfle  15705  halfleoddlt  15706  bitsp1o  15777  prmreclem5  16251  prmreclem6  16252  iihalf1  23530  iihalf1cn  23531  iihalf2  23532  iihalf2cn  23533  elii1  23534  elii2  23535  htpycc  23579  pcoval1  23612  pco0  23613  pco1  23614  pcoval2  23615  pcocn  23616  pcohtpylem  23618  pcopt  23621  pcopt2  23622  pcoass  23623  pcorevlem  23625  iscmet3lem3  23888  mbfi1fseqlem6  24316  itg2monolem3  24348  aaliou3lem1  24929  aaliou3lem2  24930  aaliou3lem3  24931  cxpsqrtlem  25283  cxpsqrt  25284  logsqrt  25285  sqrt2cxp2logb9e3  25375  ang180lem1  25385  asinsin  25468  birthday  25530  gausslemma2dlem1a  25939  chebbnd1  26046  chtppilim  26049  mulog2sumlem2  26109  opsqrlem4  29918  logdivsqrle  31942  subfacval3  32457  dnicld1  33832  dnizeq0  33835  dnizphlfeqhlf  33836  rddif2  33837  dnibndlem2  33839  dnibndlem3  33840  dnibndlem4  33841  dnibndlem5  33842  dnibndlem6  33843  dnibndlem7  33844  dnibndlem8  33845  dnibndlem9  33846  dnibndlem10  33847  dnibndlem11  33848  dnibndlem12  33849  dnibndlem13  33850  dnibnd  33851  knoppcnlem4  33856  cnndvlem1  33897  cntotbnd  35107  halffl  41637  stoweidlem5  42364  stoweidlem14  42373  stoweidlem28  42387  dirkertrigeqlem2  42458  dirkeritg  42461  dirkercncflem2  42463  fourierdlem18  42484  fourierdlem66  42531  fourierdlem78  42543  fourierdlem83  42548  fourierdlem87  42552  fourierdlem104  42569  zofldiv2ALTV  43901  zofldiv2  44665