Theorem 2re 12339

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 12327	. 2 ⊢ 2 = (1 + 1)
2		1re 11232	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11248	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2856	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7413  ℝcr 11123  1c1 11125   + caddc 11127  2c2 12319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rrecex 11196  ax-cnre 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-2 12327

This theorem is used by:  2cnALT  12341  3re  12345  0le2  12367  2lt3  12438  2le3  12439  1lt3  12440  2lt4  12442  1lt4  12443  2lt5  12446  2lt6  12451  1lt6  12452  2lt7  12457  1lt7  12458  2lt8  12464  1lt8  12465  2lt9  12472  1lt9  12473  1le2  12476  2rene0  12478  halfre  12481  halfgt0  12483  halflt1  12485  rehalfcl  12495  halfpos2  12497  halfnneg2  12499  addltmul  12504  nominpos  12505  avglt1  12506  avglt2  12507  div4p1lem1div2  12523  nn0lele2xi  12584  nn0n0n1ge2b  12597  nn0ge2m1nn  12598  nn0le2is012  12685  halfnz  12699  3halfnz  12700  2lt10  12880  1lt10OLD  12882  uzuzle23  12933  uzuzle24  12934  uz3m2nn  12943  2rp  13047  ge2halflem1  13159  xnn0n0n1ge2b  13183  fztpval  13641  fz0to4untppr  13685  fz0to5un2tp  13686  fzo0to42pr  13809  flhalf  13891  fldiv4p1lem1div2  13896  2txmodxeq0  13995  expubnd  14242  expmulnbnd  14299  nn0opthlem2  14333  faclbnd2  14355  faclbnd4lem1  14357  faclbnd5  14362  4bc2eq6  14393  hashgt23el  14489  hashfun  14502  hashge2el2dif  14545  hashge2el2difr  14546  hash3tpde  14558  wrdlenge2n0  14617  f1oun2prg  14988  01sqrexlem7  15335  sqrt4  15359  sqrt2gt1lt2  15361  abstri  15418  sqreulem  15447  amgm2  15457  caucvgrlem  15760  climcndslem1  15938  climcndslem2  15939  climcnds  15940  efcllem  16163  ege2le3  16176  ef01bndlem  16272  cos01bnd  16274  cos2bnd  16276  cos01gt0  16279  sin02gt0  16280  sincos2sgn  16282  sin4lt0  16283  eirrlem  16292  egt2lt3  16294  epos  16295  ene1  16298  sqrt2re  16338  mod2eq1n2dvds  16437  oddge22np1  16439  evennn2n  16441  nn0o1gt2  16471  nno  16472  nn0o  16473  nnoddm1d2  16476  bitsp1o  16523  bitsfzolem  16524  bitsfzo  16525  bitsfi  16527  6gcd4e2  16628  2mulprm  16783  ge2nprmge4  16792  isprm7  16799  3lcm2e6  16823  prmreclem2  17009  prmreclem6  17013  4sqlem11  17047  4sqlem12  17048  prmgaplem7  17149  2expltfac  17184  plusgndxnmulrndx  17382  starvndxnplusgndx  17390  scandxnplusgndx  17402  vscandxnplusgndx  17407  ipndxnplusgndx  17418  tsetndxnplusgndx  17442  plendxnplusgndx  17456  dsndxnplusgndx  17475  slotsdifunifndx  17486  efgredleme  19870  zringndrg  21681  chfacfscmul0  23083  chfacfpmmul0  23087  psmetge0  24538  xmetge0  24570  bl2in  24626  metnrmlem3  25088  iihalf1  25159  iihalf2  25161  pcoass  25252  tcphcphlem1  25463  csbren  25627  trirn  25628  minveclem2  25654  minveclem4  25660  pjthlem1  25665  ovolunlem1a  25724  dyadss  25822  opnmbllem  25829  vitalilem2  25837  vitalilem4  25839  mbfi1fseqlem5  25947  lhop1lem  26240  aaliou3lem2  26579  aaliou3lem8  26581  pilem2  26688  pilem3  26689  2pire  26693  pipos  26696  sinhalfpilem  26701  sincosq1lem  26735  sincosq4sgn  26739  tangtx  26743  sinq12gt0  26745  sincos4thpi  26751  tan4thpi  26752  sincos6thpi  26753  sineq0  26761  cos02pilt1  26763  cosq34lt1  26764  cosordlem  26767  cos0pilt1  26769  tanord1  26774  efif1olem1  26779  efif1olem2  26780  efif1olem4  26782  efif1o  26783  efifo  26784  2irrexpq  26968  cxpcn3lem  26984  root1id  26991  root1eq1  26992  root1cj  26993  cxpeq  26994  2logb9irr  27032  2logb3irr  27034  ang180lem1  27046  ang180lem2  27047  chordthmlem2  27070  1cubrlem  27078  atancj  27147  atantan  27160  atanbndlem  27162  atans2  27168  leibpi  27179  log2tlbnd  27182  log2ublem2  27184  log2ub  27186  divsqrtsumlem  27216  harmonicbnd3  27244  zetacvg  27251  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem4  27268  lgamgulmlem6  27270  lgamucov  27274  basellem1  27317  basellem2  27318  basellem3  27319  basellem5  27321  chtdif  27394  ppidif  27399  ppinncl  27410  chtrpcl  27411  ppieq0  27412  ppiltx  27413  ppiublem1  27438  ppiub  27440  chpeq0  27444  chteq0  27445  chtublem  27447  chtub  27448  chpval2  27454  chpub  27456  mersenne  27463  perfectlem1  27465  perfectlem2  27466  dchrptlem1  27500  dchrptlem2  27501  bcmono  27513  bclbnd  27516  bpos1lem  27518  bposlem1  27520  bposlem2  27521  bposlem3  27522  bposlem4  27523  bposlem5  27524  bposlem6  27525  bposlem7  27526  bposlem8  27527  bposlem9  27528  lgslem1  27533  lgsdirprm  27567  gausslemma2dlem0c  27594  gausslemma2dlem1a  27601  gausslemma2dlem2  27603  gausslemma2dlem3  27604  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisen  27615  lgsquadlem1  27616  lgsquadlem2  27617  m1lgs  27624  2lgslem1a1  27625  2lgslem1a2  27626  2lgslem1c  27629  2lgslem4  27642  2sqlem11  27665  2sq2  27669  2sqreultlem  27683  2sqreunnltlem  27686  chebbnd1lem1  27705  chebbnd1lem2  27706  chebbnd1lem3  27707  chebbnd1  27708  chtppilimlem1  27709  chtppilimlem2  27710  chtppilim  27711  chto1ub  27712  chebbnd2  27713  chto1lb  27714  chpchtlim  27715  chpo1ub  27716  chpo1ubb  27717  rplogsumlem1  27720  rplogsumlem2  27721  dchrisumlem2  27726  dchrisumlem3  27727  dchrvmasumiflem1  27737  dchrisum0fno1  27747  dchrisum0re  27749  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2  27754  rplogsum  27763  mulog2sumlem1  27770  mulog2sumlem2  27771  log2sumbnd  27780  selberglem2  27782  selbergb  27785  selberg2b  27788  chpdifbndlem1  27789  logdivbnd  27792  selberg3lem1  27793  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrmax  27800  pntrsumbnd2  27803  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntrlog2bnd  27820  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntpbnd  27824  pntibndlem2  27827  pntibndlem3  27828  pntibnd  27829  pntlemb  27833  pntlemg  27834  pntlemh  27835  pntlemr  27838  pntlemk  27842  pntlemo  27843  pnt2  27849  pnt  27850  ostth2lem1  27854  ostth3  27874  slotsinbpsd  28782  slotslnbpsd  28783  istrkg3ld  28802  tgldimor  28844  trgcgrg  28857  tgcgr4  28873  axlowdimlem6  29404  axlowdimlem16  29414  axlowdimlem17  29415  axlowdim  29418  upgrfi  29548  umgrupgr  29560  umgrislfupgrlem  29579  umgrislfupgr  29580  lfgrnloop  29582  lfuhgr2  29606  usgruspgr  29640  usgrislfuspgr  29647  lfuhgr1v0e  29714  usgrexmpldifpr  29718  usgrexmplef  29719  nbusgrvtxm1  29839  vdegp1bi  29997  upgrewlkle2  30066  lfgrwlkprop  30149  upgr2pthnlp  30197  usgr2pthlem  30228  pthdlem1  30231  wwlksm1edg  30349  wwlksnextwrd  30365  wwlksnextfun  30366  wwlksnextinj  30367  wwlksnextproplem3  30379  clwlkclwwlklem2a1  30462  clwlkclwwlklem2a2  30463  clwlkclwwlklem2fv1  30465  clwlkclwwlklem2fv2  30466  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlklem2  30470  clwlkclwwlk2  30473  clwlkclwwlkf  30478  clwwlkext2edg  30526  konigsbergiedgw  30728  konigsbergssiedgw  30730  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  konigsberg  30737  frgrreggt1  30873  ex-pss  30908  ex-res  30921  ex-fv  30923  ex-fl  30927  ex-mod  30929  ex-abs  30935  nrt2irr  30953  ipidsq  31191  minvecolem2  31356  minvecolem4  31361  normlem7  31597  norm-ii-i  31618  norm3lemt  31633  normpar2i  31637  bcsiALT  31660  pjhthlem1  31872  opsqrlem6  32626  cdj3lem1  32915  addltmulALT  32927  nexple  33303  2exple2exp  33304  threehalves  33360  pfx1s2  33385  wrdt2ind  33395  cyc3conja  33597  drngidlhash  33861  evl1deg3  33988  rtelextdg2lem  34236  fldext2chn  34238  constraddcl  34272  iconstr  34276  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  sqsscirc1  34418  dya2iocucvr  34795  omssubadd  34811  oddpwdc  34865  eulerpartlemgc  34873  fibp1  34912  coinfliplem  34990  coinflipspace  34992  ballotlem2  35000  signstfveq0  35085  prodfzo03  35111  hgt750lemd  35156  logdivsqrle  35158  hgt750lem  35159  hgt750lem2  35160  hgt750leme  35166  usgrcyclgt2v  35724  acycgr2v  35729  subfacp1lem1  35758  subfacp1lem5  35763  subfacval3  35768  problem2  36245  problem5  36248  circum  36253  nn0prpwlem  36941  dnibndlem10  37184  knoppcnlem2  37191  knoppcnlem4  37193  knoppcnlem10  37199  unbdqndv2lem1  37206  knoppndvlem1  37209  knoppndvlem10  37218  knoppndvlem11  37219  knoppndvlem12  37220  knoppndvlem14  37222  knoppndvlem15  37223  knoppndvlem17  37225  knoppndvlem18  37226  knoppndvlem19  37227  knoppndvlem20  37228  knoppndvlem21  37229  cnndvlem1  37234  taupi  38075  iccioo01  38081  relowlpssretop  38118  sin2h  38364  cos2h  38365  tan2h  38366  poimirlem7  38376  poimirlem9  38378  opnmbllem0  38405  mblfinlem1  38406  mblfinlem2  38407  itg2addnclem  38420  isbnd2  38533  isbnd3  38534  heiborlem7  38567  12gcd5e1  42869  lcm2un  42880  lcmineqlem19  42913  lcmineqlem20  42914  lcmineqlem22  42916  3lexlogpow5ineq2  42921  3lexlogpow5ineq4  42922  3lexlogpow5ineq3  42923  3lexlogpow2ineq1  42924  3lexlogpow2ineq2  42925  3lexlogpow5ineq5  42926  aks4d1lem1  42928  aks4d1p1p3  42935  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  aks6d1c3  42989  2np3bcnp1  43010  2ap1caineq  43011  aks6d1c6lem4  43039  aks6d1c7lem1  43046  aks6d1c7lem2  43047  oexpreposd  43197  asin1half  43232  remul02  43280  sn-0ne2  43281  remul01  43282  flt4lem7  43505  rabren3dioph  43656  pellexlem2  43671  pellexlem5  43674  pell14qrgapw  43717  pellfundex  43727  rmspecsqrtnq  43747  jm2.24nn  43800  jm2.17a  43801  jm2.17b  43802  jm2.17c  43803  acongrep  43821  acongeq  43824  jm2.22  43836  jm2.23  43837  jm3.1lem2  43859  expdiophlem1  43862  sqrtcval  44481  imo72b2lem0  45005  lhe4.4ex1a  45153  isosctrlem1ALT  45756  sineq0ALT  45759  lt3addmuld  46134  suplesup  46169  infleinflem2  46200  infleinf  46201  sumnnodd  46460  0ellimcdiv  46477  sinaover2ne0  46696  stoweidlem13  46841  stoweidlem14  46842  stoweidlem26  46854  stoweidlem49  46877  stoweidlem52  46880  wallispilem4  46896  wallispilem5  46897  wallispi  46898  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  stirlinglem5  46906  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  stirlinglem11  46912  stirlinglem15  46916  stirlingr  46918  dirker2re  46920  dirkerval2  46922  dirkerre  46923  dirkertrigeqlem1  46926  dirkertrigeqlem3  46928  dirkercncflem1  46931  dirkercncflem4  46934  fourierdlem24  46959  fourierdlem43  46978  fourierdlem44  46979  fourierdlem57  46991  fourierdlem58  46992  fourierdlem62  46996  fourierdlem66  47000  fourierdlem68  47002  fourierdlem72  47006  fourierdlem76  47010  fourierdlem78  47012  fourierdlem79  47013  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  etransclem23  47085  salexct2  47167  salexct3  47170  salgencntex  47171  salgensscntex  47172  sge0ad2en  47259  ovnsubaddlem1  47398  smfmullem4  47622  smf2id  47629  goldrarr  47746  goldrapos  47748  goldratmolem4  47753  goldratval  47754  2leaddle2  48186  p1lep2  48188  2ltceilhalf  48220  ceilhalfgt1  48221  2tceilhalfelfzo1  48224  rehalfge1  48227  ceilhalfnn  48228  ceil5half3  48234  difmodm1lt  48253  2timesltsq  48266  2timesltsqm1  48267  fmtnoge3  48433  fmtnof1  48438  fmtnoprmfac2lem1  48469  fmtno4prmfac  48475  fmtno4prm  48478  2pwp1prm  48492  31prm  48500  sfprmdvdsmersenne  48506  lighneallem2  48509  lighneallem4a  48511  lighneallem4b  48512  nprmdvdsfacm1lem2  48524  nprmdvdsfacm1lem4  48526  ppivalnnnprmge6  48529  requad01  48537  requad1  48538  requad2  48539  dfodd4  48575  nn0o1gt2ALTV  48610  nnoALTV  48611  nn0oALTV  48612  nn0e  48613  nneven  48614  perfectALTVlem1  48637  perfectALTVlem2  48638  341fppr2  48650  9fppr8  48653  fpprel2  48657  nfermltl2rev  48659  gbowgt5  48678  sbgoldbalt  48697  sgoldbeven3prm  48699  mogoldbb  48701  nnsum3primes4  48704  nnsum3primesgbe  48708  nnsum3primesle9  48710  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  cycl3grtri  48863  usgrexmpl1lem  48937  usgrexmpl2lem  48942  usgrexmpl2nb2  48949  usgrexmpl2nb3  48950  usgrexmpl2nb4  48951  usgrexmpl2nb5  48952  usgrexmpl2trifr  48953  gpgprismgrusgra  48974  gpg5nbgrvtx13starlem2  48988  gpg3nbgrvtx0  48992  gpg3kgrtriexlem1  48999  cznnring  49177  ply1mulgsumlem2  49317  zlmodzxznm  49427  zlmodzxzldeplem  49428  nn0eo  49458  flnn0div2ge  49463  rege1logbzge0  49489  fldivexpfllog2  49495  logbpw2m1  49497  fllog2  49498  blenpw2m1  49509  nnpw2blen  49510  nnolog2flm1  49520  blennngt2o2  49522  dig2nn1st  49535  dig2nn0  49541  dig2bits  49544  dignn0flhalflem1  49545  dignn0flhalflem2  49546  dignn0flhalf  49548  nn0sumshdiglemA  49549  ackval42  49626  rrx2xpref1o  49648  itscnhlc0yqe  49689  itsclquadb  49706  2itscp  49711  itscnhlinecirc02p  49715  sepfsepc  49854  2ne3  50775  veronesev2lem  50807  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811  veronesevrowd  50812  veroquadgsumlem  50816