Theorem 2re 12314

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 12302	. 2 ⊢ 2 = (1 + 1)
2		1re 11207	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11223	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2865	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11098  1c1 11100   + caddc 11102  2c2 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302

This theorem is referenced by:  2cnALT  12316  3re  12320  0le2  12342  2lt3  12413  2le3  12414  1lt3  12415  2lt4  12417  1lt4  12418  2lt5  12421  2lt6  12426  1lt6  12427  2lt7  12432  1lt7  12433  2lt8  12439  1lt8  12440  2lt9  12447  1lt9  12448  1le2  12451  2rene0  12453  halfre  12456  halfgt0  12458  halflt1  12460  rehalfcl  12470  halfpos2  12472  halfnneg2  12474  addltmul  12479  nominpos  12480  avglt1  12481  avglt2  12482  div4p1lem1div2  12498  nn0lele2xi  12559  nn0n0n1ge2b  12572  nn0ge2m1nn  12573  nn0le2is012  12659  halfnz  12673  3halfnz  12674  2lt10  12854  1lt10OLD  12856  uzuzle23  12907  uzuzle24  12908  uz3m2nn  12917  2rp  13020  ge2halflem1  13132  xnn0n0n1ge2b  13156  fztpval  13613  fz0to4untppr  13657  fz0to5un2tp  13658  fzo0to42pr  13781  flhalf  13862  fldiv4p1lem1div2  13867  2txmodxeq0  13966  expubnd  14213  expmulnbnd  14270  nn0opthlem2  14304  faclbnd2  14326  faclbnd4lem1  14328  faclbnd5  14333  4bc2eq6  14364  hashgt23el  14460  hashfun  14473  hashge2el2dif  14516  hashge2el2difr  14517  hash3tpde  14529  wrdlenge2n0  14588  f1oun2prg  14953  01sqrexlem7  15298  sqrt4  15322  sqrt2gt1lt2  15324  abstri  15381  sqreulem  15410  amgm2  15420  caucvgrlem  15723  climcndslem1  15902  climcndslem2  15903  climcnds  15904  efcllem  16130  ege2le3  16143  ef01bndlem  16239  cos01bnd  16241  cos2bnd  16243  cos01gt0  16246  sin02gt0  16247  sincos2sgn  16249  sin4lt0  16250  eirrlem  16259  egt2lt3  16261  epos  16262  ene1  16265  sqrt2re  16305  mod2eq1n2dvds  16404  oddge22np1  16406  evennn2n  16408  nn0o1gt2  16438  nno  16439  nn0o  16440  nnoddm1d2  16443  bitsp1o  16490  bitsfzolem  16491  bitsfzo  16492  bitsfi  16494  6gcd4e2  16595  2mulprm  16750  ge2nprmge4  16759  isprm7  16766  3lcm2e6  16790  prmreclem2  16976  prmreclem6  16980  4sqlem11  17014  4sqlem12  17015  prmgaplem7  17116  2expltfac  17151  plusgndxnmulrndx  17349  starvndxnplusgndx  17357  scandxnplusgndx  17369  vscandxnplusgndx  17374  ipndxnplusgndx  17385  tsetndxnplusgndx  17409  plendxnplusgndx  17423  dsndxnplusgndx  17442  slotsdifunifndx  17453  efgredleme  19812  zringndrg  21586  chfacfscmul0  22983  chfacfpmmul0  22987  psmetge0  24437  xmetge0  24469  bl2in  24525  metnrmlem3  24987  iihalf1  25058  iihalf2  25060  pcoass  25151  tcphcphlem1  25362  csbren  25526  trirn  25527  minveclem2  25553  minveclem4  25559  pjthlem1  25564  ovolunlem1a  25623  dyadss  25721  opnmbllem  25728  vitalilem2  25736  vitalilem4  25738  mbfi1fseqlem5  25846  lhop1lem  26140  aaliou3lem2  26472  aaliou3lem8  26474  pilem2  26580  pilem3  26581  2pire  26585  pipos  26588  sinhalfpilem  26593  sincosq1lem  26627  sincosq4sgn  26631  tangtx  26635  sinq12gt0  26637  sincos4thpi  26643  tan4thpi  26644  tan4thpiOLD  26645  sincos6thpi  26646  sineq0  26654  cos02pilt1  26656  cosq34lt1  26657  cosordlem  26660  cos0pilt1  26662  tanord1  26667  efif1olem1  26672  efif1olem2  26673  efif1olem4  26675  efif1o  26676  efifo  26677  2irrexpq  26861  cxpcn3lem  26877  root1id  26884  root1eq1  26885  root1cj  26886  cxpeq  26887  2logb9irr  26925  2logb3irr  26927  ang180lem1  26939  ang180lem2  26940  chordthmlem2  26963  1cubrlem  26971  atancj  27040  atantan  27053  atanbndlem  27055  atans2  27061  leibpi  27072  log2tlbnd  27075  log2ublem2  27077  log2ub  27079  divsqrtsumlem  27109  harmonicbnd3  27137  zetacvg  27144  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem4  27161  lgamgulmlem6  27163  lgamucov  27167  basellem1  27210  basellem2  27211  basellem3  27212  basellem5  27214  chtdif  27287  ppidif  27292  ppinncl  27303  chtrpcl  27304  ppieq0  27305  ppiltx  27306  ppiublem1  27331  ppiub  27333  chpeq0  27337  chteq0  27338  chtublem  27340  chtub  27341  chpval2  27347  chpub  27349  mersenne  27356  perfectlem1  27358  perfectlem2  27359  dchrptlem1  27393  dchrptlem2  27394  bcmono  27406  bclbnd  27409  bpos1lem  27411  bposlem1  27413  bposlem2  27414  bposlem3  27415  bposlem4  27416  bposlem5  27417  bposlem6  27418  bposlem7  27419  bposlem8  27420  bposlem9  27421  lgslem1  27426  lgsdirprm  27460  gausslemma2dlem0c  27487  gausslemma2dlem1a  27494  gausslemma2dlem2  27496  gausslemma2dlem3  27497  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisen  27508  lgsquadlem1  27509  lgsquadlem2  27510  m1lgs  27517  2lgslem1a1  27518  2lgslem1a2  27519  2lgslem1c  27522  2lgslem4  27535  2sqlem11  27558  2sq2  27562  2sqreultlem  27576  2sqreunnltlem  27579  chebbnd1lem1  27598  chebbnd1lem2  27599  chebbnd1lem3  27600  chebbnd1  27601  chtppilimlem1  27602  chtppilimlem2  27603  chtppilim  27604  chto1ub  27605  chebbnd2  27606  chto1lb  27607  chpchtlim  27608  chpo1ub  27609  chpo1ubb  27610  rplogsumlem1  27613  rplogsumlem2  27614  dchrisumlem2  27619  dchrisumlem3  27620  dchrvmasumiflem1  27630  dchrisum0fno1  27640  dchrisum0re  27642  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2  27647  rplogsum  27656  mulog2sumlem1  27663  mulog2sumlem2  27664  log2sumbnd  27673  selberglem2  27675  selbergb  27678  selberg2b  27681  chpdifbndlem1  27682  logdivbnd  27685  selberg3lem1  27686  selberg3  27688  selberg4lem1  27689  selberg4  27690  pntrmax  27693  pntrsumbnd2  27696  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd1a  27714  pntpbnd1  27715  pntpbnd2  27716  pntpbnd  27717  pntibndlem2  27720  pntibndlem3  27721  pntibnd  27722  pntlemb  27726  pntlemg  27727  pntlemh  27728  pntlemr  27731  pntlemk  27735  pntlemo  27736  pnt2  27742  pnt  27743  ostth2lem1  27747  ostth3  27767  slotsinbpsd  28675  slotslnbpsd  28676  istrkg3ld  28695  tgldimor  28736  trgcgrg  28749  tgcgr4  28765  axlowdimlem6  29237  axlowdimlem16  29247  axlowdimlem17  29248  axlowdim  29251  upgrfi  29381  umgrupgr  29393  umgrislfupgrlem  29412  umgrislfupgr  29413  lfgrnloop  29415  usgruspgr  29470  usgrislfuspgr  29477  lfuhgr1v0e  29544  usgrexmpldifpr  29548  usgrexmplef  29549  nbusgrvtxm1  29669  vdegp1bi  29827  upgrewlkle2  29896  lfgrwlkprop  29975  upgr2pthnlp  30021  usgr2pthlem  30052  pthdlem1  30055  wwlksm1edg  30170  wwlksnextwrd  30186  wwlksnextfun  30187  wwlksnextinj  30188  wwlksnextproplem3  30200  clwlkclwwlklem2a1  30283  clwlkclwwlklem2a2  30284  clwlkclwwlklem2fv1  30286  clwlkclwwlklem2fv2  30287  clwlkclwwlklem2a4  30288  clwlkclwwlklem2a  30289  clwlkclwwlklem2  30291  clwlkclwwlk2  30294  clwlkclwwlkf  30299  clwwlkext2edg  30347  konigsbergiedgw  30539  konigsbergssiedgw  30541  konigsberglem1  30543  konigsberglem2  30544  konigsberglem3  30545  konigsberg  30548  frgrreggt1  30684  ex-pss  30719  ex-res  30732  ex-fv  30734  ex-fl  30738  ex-mod  30740  ex-abs  30746  nrt2irr  30764  ipidsq  31002  minvecolem2  31167  minvecolem4  31172  normlem7  31408  norm-ii-i  31429  norm3lemt  31444  normpar2i  31448  bcsiALT  31471  pjhthlem1  31683  opsqrlem6  32437  cdj3lem1  32726  addltmulALT  32738  nexple  33117  2exple2exp  33118  threehalves  33174  pfx1s2  33199  wrdt2ind  33213  cyc3conja  33417  drngidlhash  33685  evl1deg3  33812  rtelextdg2lem  34060  fldext2chn  34062  constraddcl  34096  iconstr  34100  2sqr3minply  34114  2sqr3nconstr  34115  cos9thpinconstrlem1  34123  cos9thpinconstrlem2  34124  sqsscirc1  34242  dya2iocucvr  34618  omssubadd  34634  oddpwdc  34688  eulerpartlemgc  34696  fibp1  34735  coinfliplem  34813  coinflipspace  34815  ballotlem2  34823  signstfveq0  34908  prodfzo03  34934  hgt750lemd  34979  logdivsqrle  34981  hgt750lem  34982  hgt750lem2  34983  hgt750leme  34989  lfuhgr2  35509  usgrcyclgt2v  35521  acycgr2v  35540  subfacp1lem1  35569  subfacp1lem5  35574  subfacval3  35579  problem2  36056  problem5  36059  circum  36064  nn0prpwlem  36721  dnibndlem10  36964  knoppcnlem2  36971  knoppcnlem4  36973  knoppcnlem10  36979  unbdqndv2lem1  36986  knoppndvlem1  36989  knoppndvlem10  36998  knoppndvlem11  36999  knoppndvlem12  37000  knoppndvlem14  37002  knoppndvlem15  37003  knoppndvlem17  37005  knoppndvlem18  37006  knoppndvlem19  37007  knoppndvlem20  37008  knoppndvlem21  37009  cnndvlem1  37014  taupi  37854  iccioo01  37860  relowlpssretop  37897  sin2h  38148  cos2h  38149  tan2h  38150  poimirlem7  38165  poimirlem9  38167  opnmbllem0  38194  mblfinlem1  38195  mblfinlem2  38196  itg2addnclem  38209  isbnd2  38321  isbnd3  38322  heiborlem7  38355  12gcd5e1  42659  lcm2un  42670  lcmineqlem19  42703  lcmineqlem20  42704  lcmineqlem22  42706  3lexlogpow5ineq2  42711  3lexlogpow5ineq4  42712  3lexlogpow5ineq3  42713  3lexlogpow2ineq1  42714  3lexlogpow2ineq2  42715  3lexlogpow5ineq5  42716  aks4d1lem1  42718  aks4d1p1p3  42725  aks4d1p1p2  42726  aks4d1p1p4  42727  aks4d1p1p6  42729  aks4d1p1p7  42730  aks4d1p1p5  42731  aks4d1p1  42732  aks4d1p2  42733  aks4d1p3  42734  aks4d1p5  42736  aks4d1p6  42737  aks4d1p7d1  42738  aks4d1p7  42739  aks4d1p8  42743  aks4d1p9  42744  posbezout  42756  aks6d1c3  42779  2np3bcnp1  42800  2ap1caineq  42801  aks6d1c6lem4  42829  aks6d1c7lem1  42836  aks6d1c7lem2  42837  oexpreposd  42972  asin1half  43007  remul02  43055  sn-0ne2  43056  remul01  43057  flt4lem7  43282  rabren3dioph  43433  pellexlem2  43448  pellexlem5  43451  pell14qrgapw  43494  pellfundex  43504  rmspecsqrtnq  43524  jm2.24nn  43577  jm2.17a  43578  jm2.17b  43579  jm2.17c  43580  acongrep  43598  acongeq  43601  jm2.22  43613  jm2.23  43614  jm3.1lem2  43636  expdiophlem1  43639  sqrtcval  44258  imo72b2lem0  44782  lhe4.4ex1a  44930  isosctrlem1ALT  45533  sineq0ALT  45536  lt3addmuld  45911  suplesup  45946  infleinflem2  45977  infleinf  45978  sumnnodd  46237  0ellimcdiv  46254  sinaover2ne0  46473  stoweidlem13  46618  stoweidlem14  46619  stoweidlem26  46631  stoweidlem49  46654  stoweidlem52  46657  wallispilem4  46673  wallispilem5  46674  wallispi  46675  wallispi2lem1  46676  wallispi2lem2  46677  wallispi2  46678  stirlinglem1  46679  stirlinglem3  46681  stirlinglem5  46683  stirlinglem6  46684  stirlinglem7  46685  stirlinglem10  46688  stirlinglem11  46689  stirlinglem15  46693  stirlingr  46695  dirker2re  46697  dirkerval2  46699  dirkerre  46700  dirkertrigeqlem1  46703  dirkertrigeqlem3  46705  dirkercncflem1  46708  dirkercncflem4  46711  fourierdlem24  46736  fourierdlem43  46755  fourierdlem44  46756  fourierdlem57  46768  fourierdlem58  46769  fourierdlem62  46773  fourierdlem66  46777  fourierdlem68  46779  fourierdlem72  46783  fourierdlem76  46787  fourierdlem78  46789  fourierdlem79  46790  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  sqwvfoura  46833  sqwvfourb  46834  fourierswlem  46835  fouriersw  46836  etransclem23  46862  salexct2  46944  salexct3  46947  salgencntex  46948  salgensscntex  46949  sge0ad2en  47036  ovnsubaddlem1  47175  smfmullem4  47399  smf2id  47406  nthrucw  47493  goldrarr  47506  goldrapos  47508  2leaddle2  47923  p1lep2  47925  2ltceilhalf  47957  ceilhalfgt1  47958  2tceilhalfelfzo1  47961  rehalfge1  47964  ceilhalfnn  47965  ceil5half3  47971  difmodm1lt  47990  2timesltsq  48003  2timesltsqm1  48004  fmtnoge3  48170  fmtnof1  48175  fmtnoprmfac2lem1  48206  fmtno4prmfac  48212  fmtno4prm  48215  2pwp1prm  48229  31prm  48237  sfprmdvdsmersenne  48243  lighneallem2  48246  lighneallem4a  48248  lighneallem4b  48249  nprmdvdsfacm1lem2  48261  nprmdvdsfacm1lem4  48263  ppivalnnnprmge6  48266  requad01  48274  requad1  48275  requad2  48276  dfodd4  48312  nn0o1gt2ALTV  48347  nnoALTV  48348  nn0oALTV  48349  nn0e  48350  nneven  48351  perfectALTVlem1  48374  perfectALTVlem2  48375  341fppr2  48387  9fppr8  48390  fpprel2  48394  nfermltl2rev  48396  gbowgt5  48415  sbgoldbalt  48434  sgoldbeven3prm  48436  mogoldbb  48438  nnsum3primes4  48441  nnsum3primesgbe  48445  nnsum3primesle9  48447  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  cycl3grtri  48600  usgrexmpl1lem  48674  usgrexmpl2lem  48679  usgrexmpl2nb2  48686  usgrexmpl2nb3  48687  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  usgrexmpl2trifr  48690  gpgprismgrusgra  48711  gpg5nbgrvtx13starlem2  48725  gpg3nbgrvtx0  48729  gpg3kgrtriexlem1  48736  cznnring  48915  ply1mulgsumlem2  49051  zlmodzxznm  49161  zlmodzxzldeplem  49162  nn0eo  49192  flnn0div2ge  49197  rege1logbzge0  49223  fldivexpfllog2  49229  logbpw2m1  49231  fllog2  49232  blenpw2m1  49243  nnpw2blen  49244  nnolog2flm1  49254  blennngt2o2  49256  dig2nn1st  49269  dig2nn0  49275  dig2bits  49278  dignn0flhalflem1  49279  dignn0flhalflem2  49280  dignn0flhalf  49282  nn0sumshdiglemA  49283  ackval42  49360  rrx2xpref1o  49382  itscnhlc0yqe  49423  itsclquadb  49440  2itscp  49445  itscnhlinecirc02p  49449  sepfsepc  49590