Theorem 2z 10998

Description: 2 is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
2z	|- 2 e. ZZ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 10796	. 2 |- 2 e. NN
2	1	nnzi 10990	1 |- 2 e. ZZ

Syntax hints:   e. wcel 1898   2c2 10687   ZZcz 10966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-z 10967

This theorem is referenced by:  nn0lt2  11029  zadd2cl  11077  uzuzle23  11228  2eluzge0OLD  11233  2eluzge1  11234  eluz2b1  11259  nn01to3  11286  nn0ge2m1nnALT  11287  ige2m1fz  11913  fz0to3un2pr  11923  fzctr  11933  fzo0to2pr  12029  fzo0to42pr  12031  flhalf  12094  2txmodxeq0  12182  f13idfv  12244  sq1  12401  expnass  12412  sqrecd  12452  bcn2m1  12541  bcn2p1  12542  4bc2eq6  12546  hashtpg  12674  ccat2s1p2  12799  swrdtrcfv0  12835  swrdtrcfvl  12843  iseraltlem2  13798  iseraltlem3  13799  climcndslem1  13956  climcnds  13958  bpolydiflem  14156  efgt0  14206  tanval3  14237  cos01bnd  14289  cos01gt0  14294  n2dvds1  14403  odd2np1  14414  oddm1even  14415  oddp1even  14416  oexpneg  14417  bits0e  14451  bits0o  14452  bitsp1e  14454  bitsp1o  14455  bitsfzo  14458  bitsmod  14459  bitscmp  14461  bitsinv1lem  14464  bitsinv1  14465  6gcd4e2  14551  3lcm2e6woprm  14629  lcmf2a3a4e12  14669  isprm3  14682  2prm  14689  3prm  14690  prmn2uzge3  14693  divgcdodd  14702  opoe  14810  omoe  14811  opeo  14812  omeo  14813  oddprm  14814  pythagtriplem4  14818  pythagtriplem11  14824  pythagtriplem13  14826  iserodd  14834  prmgaplem3  15072  prmgaplem7  15076  dec2dvds  15084  prmlem0  15126  4001lem1  15161  psgnunilem4  17187  efgredleme  17442  lt6abl  17578  znidomb  19181  chfacfscmulfsupp  19932  chfacfpmmulfsupp  19936  minveclem2  22417  minveclem3  22420  minveclem2OLD  22429  minveclem3OLD  22432  pjthlem1  22440  dyaddisjlem  22602  mbfi1fseqlem5  22726  iblcnlem1  22794  dvexp3  22979  aaliou3lem6  23353  tanregt0  23537  efif1olem4  23543  tanarg  23617  cubic2  23823  asinlem3  23846  atantayl2  23913  cxp2limlem  23950  lgamgulmlem3  24005  lgamgulmlem4  24006  basellem2  24057  basellem3  24058  basellem4  24059  basellem5  24060  basellem8  24063  basellem9  24064  ppisval  24079  ppiprm  24127  ppinprm  24128  chtprm  24129  chtnprm  24130  chtdif  24134  ppidif  24139  ppi1  24140  cht1  24141  cht3  24149  ppieq0  24152  ppiublem1  24179  ppiublem2  24180  chpeq0  24185  chtub  24189  chpval2  24195  chpub  24197  mersenne  24204  perfect1  24205  perfectlem1  24206  perfectlem2  24207  bposlem1  24261  bposlem2  24262  bposlem3  24263  bposlem5  24265  bposlem6  24266  lgslem1  24273  lgsdir2lem2  24301  lgsdir2lem3  24302  lgsdir2  24305  lgsqr  24323  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem3  24328  lgseisenlem4  24329  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2lem1  24335  lgsquad2lem2  24336  lgsquad2  24337  lgsquad3  24338  m1lgs  24339  2sqblem  24354  chebbnd1lem1  24356  chebbnd1lem3  24358  chebbnd1  24359  dchrisum0lem1a  24373  dchrvmasumiflem1  24388  dchrisum0flblem1  24395  dchrisum0flblem2  24396  dchrisum0lem1b  24402  dchrisum0lem1  24403  dchrisum0lem2a  24404  dchrisum0lem2  24405  dchrisum0lem3  24406  mulog2sumlem2  24422  pntlemd  24481  pntlema  24483  pntlemb  24484  pntlemh  24486  pntlemr  24489  pntlemf  24492  pntlemo  24494  istrkg2ld  24557  istrkg3ld  24558  axlowdimlem3  25023  axlowdimlem6  25026  axlowdimlem16  25036  axlowdimlem17  25037  axlowdim  25040  usgraexmplvtxlem  25171  usgraexmpldifpr  25176  usgraexmplef  25177  cusgrasizeindb1  25248  2wlklemC  25335  2trllemD  25336  2trllemG  25337  wlkntrllem2  25339  constr2spthlem1  25373  2pthon  25381  usgra2adedgwlkonALT  25393  usgra2wlkspthlem2  25397  3v3e3cycl1  25421  constr3lem4  25424  constr3trllem2  25428  constr3trllem3  25429  constr3trllem5  25431  constr3pthlem1  25432  constr3pthlem2  25433  4cycl4v4e  25443  4cycl4dv4e  25445  clwlkisclwwlklem2a1  25556  clwlkisclwwlklem2fv1  25559  clwlkisclwwlklem2fv2  25560  clwlkisclwwlklem2a4  25561  clwlkisclwwlklem2a  25562  clwwisshclwwlem  25583  eupath2lem3  25756  eupath2  25757  frgrawopreglem2  25822  extwwlkfablem2  25855  numclwwlkovf2ex  25863  numclwwlk2lem1  25879  numclwlk2lem2f  25880  frgrareggt1  25893  ex-fl  25946  ex-dvds  25947  ex-ind-dvds  25948  minvecolem3  26567  minvecolem3OLD  26577  pjhthlem1  27093  znsqcld  28372  2sqmod  28458  archirngz  28555  archiabllem2c  28561  lmat22det  28697  dya2ub  29141  dya2icoseg  29148  oddpwdc  29236  eulerpartlemd  29248  eulerpartlemt  29253  ballotlem2  29370  signslema  29500  nn0prpwlem  31027  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  poimirlem28  32013  acongrep  35875  acongeq  35878  jm2.18  35888  jm2.22  35895  jm2.23  35896  jm2.20nn  35897  jm2.26a  35900  jm2.26  35902  jm2.15nn0  35903  jm2.27a  35905  jm2.27c  35907  rmydioph  35914  jm3.1lem1  35917  jm3.1lem3  35919  expdiophlem1  35921  expdiophlem2  35922  isprm7  36704  hashnzfz2  36714  sumnnodd  37748  coskpi2  37779  cosknegpi  37782  dvrecg  37820  dvdivbd  37833  stoweidlem26  37924  wallispilem4  37968  wallispi2lem1  37971  wallispi2lem2  37972  wallispi2  37973  stirlinglem1  37974  stirlinglem3  37976  stirlinglem7  37980  stirlinglem8  37981  stirlinglem10  37983  stirlinglem11  37984  stirlinglem15  37988  dirkertrigeqlem1  37998  dirkercncflem2  38004  fourierdlem54  38062  fourierdlem56  38064  fourierdlem57  38065  fourierdlem102  38110  fourierdlem114  38122  fourierswlem  38132  fouriersw  38133  mod2eq1n2dvds  38763  m1expevenALTV  38815  dfeven2  38817  oexpnegALTV  38844  oexpnegnz  38845  2evenALTV  38859  2noddALTV  38860  nn0o1gt2ALTV  38861  nnpw2evenALTV  38867  perfectALTVlem1  38881  perfectALTVlem2  38882  sgoldbalt  38920  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  wtgoldbnnsum4prm  38935  bgoldbnnsum3prm  38937  proththdlem  38951  proththd  38952  3exp4mod41  38954  41prothprmlem2  38956  pfxtrcfv0  38983  pfxtrcfvl  38986  cusgrsizeindb1  39561  pthdlem1  39792  2even  40206  nn0le2is012  40421  zlmodzxzequa  40562  zlmodzxznm  40563  zlmodzxzequap  40565  zlmodzxzldeplem1  40566  zlmodzxzldeplem3  40568  zlmodzxzldep  40570  ldepsnlinclem1  40571  ldepsnlinc  40574  pw2m1lepw2m1  40591  nn0o  40602  fldivexpfllog2  40649  nnlog2ge0lt1  40650  logbpw2m1  40651  fllog2  40652  blennnelnn  40660  blenpw2  40662  nnpw2blenfzo  40665  blennnt2  40673  nnolog2flm1  40674  dig2nn0ld  40688  dig2nn1st  40689  0dig2pr01  40694  0dig2nn0o  40697