Theorem 2re 12217

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 12206	. 2 ⊢ 2 = (1 + 1)
2		1re 11130	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11145	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2830	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023  1c1 11025   + caddc 11027  2c2 12198

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-ext 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206

This theorem is referenced by:  2cnALT  12219  3re  12223  3pos  12248  2lt3  12310  1lt3  12311  2lt4  12313  1lt4  12314  2lt5  12317  2lt6  12322  1lt6  12323  2lt7  12328  1lt7  12329  2lt8  12335  1lt8  12336  2lt9  12343  1lt9  12344  1le2  12347  2rene0  12349  halfre  12352  halfgt0  12354  halflt1  12356  rehalfcl  12366  halfpos2  12368  halfnneg2  12370  addltmul  12375  nominpos  12376  avglt1  12377  avglt2  12378  div4p1lem1div2  12394  nn0lele2xi  12455  nn0n0n1ge2b  12468  nn0ge2m1nn  12469  nn0le2is012  12554  halfnz  12568  3halfnz  12569  2lt10  12743  1lt10  12744  uzuzle23  12795  uzuzle24  12796  uz3m2nn  12805  2rp  12908  ge2halflem1  13020  xnn0n0n1ge2b  13044  fztpval  13500  fz0to4untppr  13544  fz0to5un2tp  13545  fzo0to42pr  13667  flhalf  13748  fldiv4p1lem1div2  13753  2txmodxeq0  13852  expubnd  14099  expmulnbnd  14156  nn0opthlem2  14190  faclbnd2  14212  faclbnd4lem1  14214  faclbnd5  14219  4bc2eq6  14250  hashgt23el  14345  hashfun  14358  hashge2el2dif  14401  hashge2el2difr  14402  hash3tpde  14414  wrdlenge2n0  14473  f1oun2prg  14838  01sqrexlem7  15169  sqrt4  15193  sqrt2gt1lt2  15195  abstri  15252  sqreulem  15281  amgm2  15291  caucvgrlem  15594  climcndslem1  15770  climcndslem2  15771  climcnds  15772  efcllem  15998  ege2le3  16011  ef01bndlem  16107  cos01bnd  16109  cos2bnd  16111  cos01gt0  16114  sin02gt0  16115  sincos2sgn  16117  sin4lt0  16118  eirrlem  16127  egt2lt3  16129  epos  16130  ene1  16133  sqrt2re  16173  mod2eq1n2dvds  16272  oddge22np1  16274  evennn2n  16276  nn0o1gt2  16306  nno  16307  nn0o  16308  nnoddm1d2  16311  bitsp1o  16358  bitsfzolem  16359  bitsfzo  16360  bitsfi  16362  6gcd4e2  16463  2mulprm  16618  ge2nprmge4  16626  isprm7  16633  3lcm2e6  16657  prmreclem2  16843  prmreclem6  16847  4sqlem11  16881  4sqlem12  16882  prmgaplem7  16983  2expltfac  17018  plusgndxnmulrndx  17215  starvndxnplusgndx  17223  scandxnplusgndx  17235  vscandxnplusgndx  17240  ipndxnplusgndx  17251  tsetndxnplusgndx  17275  plendxnplusgndx  17289  dsndxnplusgndx  17308  slotsdifunifndx  17319  efgredleme  19670  zringndrg  21421  chfacfscmul0  22800  chfacfpmmul0  22804  psmetge0  24254  xmetge0  24286  bl2in  24342  metnrmlem3  24804  iihalf1  24879  iihalf2  24882  pcoass  24978  tcphcphlem1  25189  csbren  25353  trirn  25354  minveclem2  25380  minveclem4  25386  pjthlem1  25391  ovolunlem1a  25451  dyadss  25549  opnmbllem  25556  vitalilem2  25564  vitalilem4  25566  mbfi1fseqlem5  25674  lhop1lem  25972  aaliou3lem2  26305  aaliou3lem8  26307  pilem2  26416  pilem3  26417  pipos  26422  sinhalfpilem  26426  sincosq1lem  26460  sincosq4sgn  26464  tangtx  26468  sinq12gt0  26470  sincos4thpi  26476  tan4thpi  26477  tan4thpiOLD  26478  sincos6thpi  26479  sineq0  26487  cos02pilt1  26489  cosq34lt1  26490  cosordlem  26493  cos0pilt1  26495  tanord1  26500  efif1olem1  26505  efif1olem2  26506  efif1olem4  26508  efif1o  26509  efifo  26510  2irrexpq  26694  cxpcn3lem  26711  root1id  26718  root1eq1  26719  root1cj  26720  cxpeq  26721  2logb9irr  26759  2logb3irr  26761  ang180lem1  26773  ang180lem2  26774  chordthmlem2  26797  1cubrlem  26805  atancj  26874  atantan  26887  atanbndlem  26889  atans2  26895  leibpi  26906  log2tlbnd  26909  log2ublem2  26911  log2ub  26913  divsqrtsumlem  26944  harmonicbnd3  26972  zetacvg  26979  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem4  26996  lgamgulmlem6  26998  lgamucov  27002  basellem1  27045  basellem2  27046  basellem3  27047  basellem5  27049  chtdif  27122  ppidif  27127  ppinncl  27138  chtrpcl  27139  ppieq0  27140  ppiltx  27141  ppiublem1  27167  ppiub  27169  chpeq0  27173  chteq0  27174  chtublem  27176  chtub  27177  chpval2  27183  chpub  27185  mersenne  27192  perfectlem1  27194  perfectlem2  27195  dchrptlem1  27229  dchrptlem2  27230  bcmono  27242  bclbnd  27245  bpos1lem  27247  bposlem1  27249  bposlem2  27250  bposlem3  27251  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem7  27255  bposlem8  27256  bposlem9  27257  lgslem1  27262  lgsdirprm  27296  gausslemma2dlem0c  27323  gausslemma2dlem1a  27330  gausslemma2dlem2  27332  gausslemma2dlem3  27333  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  m1lgs  27353  2lgslem1a1  27354  2lgslem1a2  27355  2lgslem1c  27358  2lgslem4  27371  2sqlem11  27394  2sq2  27398  2sqreultlem  27412  2sqreunnltlem  27415  chebbnd1lem1  27434  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chto1ub  27441  chebbnd2  27442  chto1lb  27443  chpchtlim  27444  chpo1ub  27445  chpo1ubb  27446  rplogsumlem1  27449  rplogsumlem2  27450  dchrisumlem2  27455  dchrisumlem3  27456  dchrvmasumiflem1  27466  dchrisum0fno1  27476  dchrisum0re  27478  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2  27483  rplogsum  27492  mulog2sumlem1  27499  mulog2sumlem2  27500  log2sumbnd  27509  selberglem2  27511  selbergb  27514  selberg2b  27517  chpdifbndlem1  27518  logdivbnd  27521  selberg3lem1  27522  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrmax  27529  pntrsumbnd2  27532  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntpbnd  27553  pntibndlem2  27556  pntibndlem3  27557  pntibnd  27558  pntlemb  27562  pntlemg  27563  pntlemh  27564  pntlemr  27567  pntlemk  27571  pntlemo  27572  pnt2  27578  pnt  27579  ostth2lem1  27583  ostth3  27603  slotsinbpsd  28462  slotslnbpsd  28463  istrkg3ld  28482  tgldimor  28523  trgcgrg  28536  tgcgr4  28552  axlowdimlem6  28969  axlowdimlem16  28979  axlowdimlem17  28980  axlowdim  28983  upgrfi  29113  umgrupgr  29125  umgrislfupgrlem  29144  umgrislfupgr  29145  lfgrnloop  29147  usgruspgr  29202  usgrislfuspgr  29209  lfuhgr1v0e  29276  usgrexmpldifpr  29280  usgrexmplef  29281  nbusgrvtxm1  29401  vdegp1bi  29560  upgrewlkle2  29629  lfgrwlkprop  29708  upgr2pthnlp  29754  usgr2pthlem  29785  pthdlem1  29788  wwlksm1edg  29903  wwlksnextwrd  29919  wwlksnextfun  29920  wwlksnextinj  29921  wwlksnextproplem3  29933  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a2  30017  clwlkclwwlklem2fv1  30019  clwlkclwwlklem2fv2  30020  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlk2  30027  clwlkclwwlkf  30032  clwwlkext2edg  30080  konigsbergiedgw  30272  konigsbergssiedgw  30274  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  konigsberg  30281  frgrreggt1  30417  ex-pss  30452  ex-res  30465  ex-fv  30467  ex-fl  30471  ex-mod  30473  ex-abs  30479  nrt2irr  30497  ipidsq  30734  minvecolem2  30899  minvecolem4  30904  normlem7  31140  norm-ii-i  31161  norm3lemt  31176  normpar2i  31180  bcsiALT  31203  pjhthlem1  31415  opsqrlem6  32169  cdj3lem1  32458  addltmulALT  32470  nexple  32874  2exple2exp  32875  threehalves  32945  pfx1s2  32970  wrdt2ind  32984  cyc3conja  33188  drngidlhash  33464  evl1deg3  33608  rtelextdg2lem  33832  fldext2chn  33834  constraddcl  33868  iconstr  33872  2sqr3minply  33886  2sqr3nconstr  33887  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  sqsscirc1  34014  dya2iocucvr  34390  omssubadd  34406  oddpwdc  34460  eulerpartlemgc  34468  fibp1  34507  coinfliplem  34585  coinflipspace  34587  ballotlem2  34595  signstfveq0  34683  prodfzo03  34709  hgt750lemd  34754  logdivsqrle  34756  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  lfuhgr2  35262  usgrcyclgt2v  35274  acycgr2v  35293  subfacp1lem1  35322  subfacp1lem5  35327  subfacval3  35332  problem2  35809  problem5  35812  circum  35817  nn0prpwlem  36465  dnibndlem10  36630  knoppcnlem2  36637  knoppcnlem4  36639  knoppcnlem10  36645  unbdqndv2lem1  36652  knoppndvlem1  36655  knoppndvlem10  36664  knoppndvlem11  36665  knoppndvlem12  36666  knoppndvlem14  36668  knoppndvlem15  36669  knoppndvlem17  36671  knoppndvlem18  36672  knoppndvlem19  36673  knoppndvlem20  36674  knoppndvlem21  36675  cnndvlem1  36680  taupi  37467  iccioo01  37471  relowlpssretop  37508  sin2h  37750  cos2h  37751  tan2h  37752  poimirlem7  37767  poimirlem9  37769  opnmbllem0  37796  mblfinlem1  37797  mblfinlem2  37798  itg2addnclem  37811  isbnd2  37923  isbnd3  37924  heiborlem7  37957  12gcd5e1  42196  lcm2un  42207  lcmineqlem19  42240  lcmineqlem20  42241  lcmineqlem22  42243  3lexlogpow5ineq2  42248  3lexlogpow5ineq4  42249  3lexlogpow5ineq3  42250  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1lem1  42255  aks4d1p1p3  42262  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  aks4d1p9  42281  posbezout  42293  aks6d1c3  42316  2np3bcnp1  42337  2ap1caineq  42338  aks6d1c6lem4  42366  aks6d1c7lem1  42373  aks6d1c7lem2  42374  oexpreposd  42519  asin1half  42554  remul02  42602  sn-0ne2  42603  remul01  42604  flt4lem7  42844  rabren3dioph  42999  pellexlem2  43014  pellexlem5  43017  pell14qrgapw  43060  pellfundex  43070  rmspecsqrtnq  43090  jm2.24nn  43143  jm2.17a  43144  jm2.17b  43145  jm2.17c  43146  acongrep  43164  acongeq  43167  jm2.22  43179  jm2.23  43180  jm2.20nn  43181  jm3.1lem2  43202  expdiophlem1  43205  sqrtcval  43824  imo72b2lem0  44348  lhe4.4ex1a  44512  isosctrlem1ALT  45116  sineq0ALT  45119  lt3addmuld  45491  suplesup  45526  infleinflem2  45557  infleinf  45558  sumnnodd  45818  0ellimcdiv  45835  sinaover2ne0  46054  stoweidlem13  46199  stoweidlem14  46200  stoweidlem26  46212  stoweidlem49  46235  stoweidlem52  46238  wallispilem4  46254  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem1  46260  stirlinglem3  46262  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem10  46269  stirlinglem11  46270  stirlinglem15  46274  stirlingr  46276  dirker2re  46278  dirkerval2  46280  dirkerre  46281  dirkerper  46282  dirkertrigeqlem1  46284  dirkertrigeqlem3  46286  dirkercncflem1  46289  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem24  46317  fourierdlem43  46336  fourierdlem44  46337  fourierdlem57  46349  fourierdlem58  46350  fourierdlem62  46354  fourierdlem66  46358  fourierdlem68  46360  fourierdlem72  46364  fourierdlem76  46368  fourierdlem78  46370  fourierdlem79  46371  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem113  46405  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  etransclem23  46443  salexct2  46525  salexct3  46528  salgencntex  46529  salgensscntex  46530  sge0ad2en  46617  ovnsubaddlem1  46756  smfmullem4  46980  smf2id  46987  nthrucw  47072  2leaddle2  47486  p1lep2  47488  2ltceilhalf  47516  ceilhalfgt1  47517  2tceilhalfelfzo1  47520  rehalfge1  47523  ceilhalfnn  47524  ceil5half3  47528  difmodm1lt  47547  fmtnoge3  47718  fmtnof1  47723  fmtnoprmfac2lem1  47754  fmtno4prmfac  47760  fmtno4prm  47763  2pwp1prm  47777  31prm  47785  sfprmdvdsmersenne  47791  lighneallem2  47794  lighneallem4a  47796  lighneallem4b  47797  requad01  47809  requad1  47810  requad2  47811  dfodd4  47847  nn0o1gt2ALTV  47882  nnoALTV  47883  nn0oALTV  47884  nn0e  47885  nneven  47886  perfectALTVlem1  47909  perfectALTVlem2  47910  341fppr2  47922  9fppr8  47925  fpprel2  47929  nfermltl2rev  47931  gbowgt5  47950  sbgoldbalt  47969  sgoldbeven3prm  47971  mogoldbb  47973  nnsum3primes4  47976  nnsum3primesgbe  47980  nnsum3primesle9  47982  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  cycl3grtri  48135  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb2  48221  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  gpgprismgrusgra  48246  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  gpg3kgrtriexlem1  48271  cznnring  48450  ply1mulgsumlem2  48575  zlmodzxznm  48685  zlmodzxzldeplem  48686  nn0eo  48716  flnn0div2ge  48721  rege1logbzge0  48747  fldivexpfllog2  48753  logbpw2m1  48755  fllog2  48756  blenpw2m1  48767  nnpw2blen  48768  nnolog2flm1  48778  blennngt2o2  48780  dig2nn1st  48793  dig2nn0  48799  dig2bits  48802  dignn0flhalflem1  48803  dignn0flhalflem2  48804  dignn0flhalf  48806  nn0sumshdiglemA  48807  ackval42  48884  rrx2xpref1o  48906  itscnhlc0yqe  48947  itsclquadb  48964  2itscp  48969  itscnhlinecirc02p  48973  sepfsepc  49115