Theorem 2z 10969

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 10767	. 2 |- 2 e. NN
2	1	nnzi 10961	1 |- 2 e. ZZ

Syntax hints:   e. wcel 1870   2c2 10659   ZZcz 10937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-2 10668  df-z 10938

This theorem is referenced by:  nn0lt2  11000  zadd2cl  11048  uzuzle23  11199  2eluzge0OLD  11204  2eluzge1  11205  eluz2b1  11230  nn01to3  11257  nn0ge2m1nnALT  11258  ige2m1fz  11882  fzctr  11901  fzo0to2pr  11995  fzo0to42pr  11997  flhalf  12059  2txmodxeq0  12147  f13idfv  12209  sq1  12366  expnass  12377  sqrecd  12417  bcn2m1  12506  bcn2p1  12507  4bc2eq6  12511  hashtpg  12632  ccat2s1p2  12747  swrdtrcfv0  12783  swrdtrcfvl  12791  iseraltlem2  13727  iseraltlem3  13728  climcndslem1  13885  climcnds  13887  bpolydiflem  14085  efgt0  14135  tanval3  14166  cos01bnd  14218  cos01gt0  14223  n2dvds1  14332  odd2np1  14343  oddm1even  14344  oddp1even  14345  oexpneg  14346  bits0e  14377  bits0o  14378  bitsp1e  14380  bitsp1o  14381  bitsfzo  14383  bitsmod  14384  bitscmp  14386  bitsinv1lem  14389  bitsinv1  14390  6gcd4e2  14476  3lcm2e6woprm  14545  lcmf2a3a4e12  14582  isprm3  14595  2prm  14602  3prm  14603  prmn2uzge3  14606  divgcdodd  14615  opoe  14715  omoe  14716  opeo  14717  omeo  14718  oddprm  14719  pythagtriplem4  14723  pythagtriplem11  14729  pythagtriplem13  14731  iserodd  14739  prmgaplem3  14977  prmgaplem7  14981  dec2dvds  14989  prmlem0  15031  4001lem1  15066  psgnunilem4  17080  efgredleme  17319  lt6abl  17455  znidomb  19054  chfacfscmulfsupp  19805  chfacfpmmulfsupp  19809  minveclem2  22252  minveclem3  22255  pjthlem1  22263  dyaddisjlem  22421  mbfi1fseqlem5  22545  iblcnlem1  22613  dvexp3  22798  aaliou3lem6  23160  tanregt0  23344  efif1olem4  23350  tanarg  23424  cubic2  23630  asinlem3  23653  atantayl2  23720  cxp2limlem  23757  lgamgulmlem3  23812  lgamgulmlem4  23813  basellem2  23862  basellem3  23863  basellem4  23864  basellem5  23865  basellem8  23868  basellem9  23869  ppisval  23884  ppiprm  23932  ppinprm  23933  chtprm  23934  chtnprm  23935  chtdif  23939  ppidif  23944  ppi1  23945  cht1  23946  cht3  23954  ppieq0  23957  ppiublem1  23984  ppiublem2  23985  chpeq0  23990  chtub  23994  chpval2  24000  chpub  24002  mersenne  24009  perfect1  24010  perfectlem1  24011  perfectlem2  24012  bposlem1  24066  bposlem2  24067  bposlem3  24068  bposlem5  24070  bposlem6  24071  lgslem1  24078  lgsdir2lem2  24106  lgsdir2lem3  24107  lgsdir2  24110  lgsqr  24128  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem3  24133  lgseisenlem4  24134  lgsquadlem1  24136  lgsquadlem2  24137  lgsquad2lem1  24140  lgsquad2lem2  24141  lgsquad2  24142  lgsquad3  24143  m1lgs  24144  2sqblem  24159  chebbnd1lem1  24161  chebbnd1lem3  24163  chebbnd1  24164  dchrisum0lem1a  24178  dchrvmasumiflem1  24193  dchrisum0flblem1  24200  dchrisum0flblem2  24201  dchrisum0lem1b  24207  dchrisum0lem1  24208  dchrisum0lem2a  24209  dchrisum0lem2  24210  dchrisum0lem3  24211  mulog2sumlem2  24227  pntlemd  24286  pntlema  24288  pntlemb  24289  pntlemh  24291  pntlemr  24294  pntlemf  24297  pntlemo  24299  istrkg2ld  24362  istrkg3ld  24363  axlowdimlem3  24811  axlowdimlem6  24814  axlowdimlem16  24824  axlowdimlem17  24825  axlowdim  24828  usgraexvlem  24959  usgraexmpldifpr  24964  usgraexmpl  24965  cusgrasizeindb1  25035  2wlklemC  25122  2trllemD  25123  2trllemG  25124  wlkntrllem2  25126  constr2spthlem1  25160  2pthon  25168  usgra2adedgwlkonALT  25180  usgra2wlkspthlem2  25184  3v3e3cycl1  25208  constr3lem4  25211  constr3trllem2  25215  constr3trllem3  25216  constr3trllem5  25218  constr3pthlem1  25219  constr3pthlem2  25220  4cycl4v4e  25230  4cycl4dv4e  25232  clwlkisclwwlklem2a1  25343  clwlkisclwwlklem2fv1  25346  clwlkisclwwlklem2fv2  25347  clwlkisclwwlklem2a4  25348  clwlkisclwwlklem2a  25349  clwwisshclwwlem  25370  eupath2lem3  25543  eupath2  25544  frgrawopreglem2  25609  extwwlkfablem2  25642  numclwwlkovf2ex  25650  numclwwlk2lem1  25666  numclwlk2lem2f  25667  frgrareggt1  25680  ex-fl  25733  ex-dvds  25734  ex-ind-dvds  25735  minvecolem3  26354  pjhthlem1  26870  znsqcld  28157  2sqmod  28238  archirngz  28335  archiabllem2c  28341  lmat22det  28478  dya2ub  28922  dya2icoseg  28929  oddpwdc  29004  eulerpartlemd  29016  eulerpartlemt  29021  ballotlem2  29138  signslema  29230  nn0prpwlem  30754  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  acongrep  35526  acongeq  35529  jm2.18  35539  jm2.22  35546  jm2.23  35547  jm2.20nn  35548  jm2.26a  35551  jm2.26  35553  jm2.15nn0  35554  jm2.27a  35556  jm2.27c  35558  rmydioph  35565  jm3.1lem1  35568  jm3.1lem3  35570  expdiophlem1  35572  expdiophlem2  35573  isprm7  36287  hashnzfz2  36297  sumnnodd  37272  coskpi2  37303  cosknegpi  37306  dvrecg  37344  dvdivbd  37357  stoweidlem26  37445  wallispilem4  37489  wallispi2lem1  37492  wallispi2lem2  37493  wallispi2  37494  stirlinglem1  37495  stirlinglem3  37497  stirlinglem7  37501  stirlinglem8  37502  stirlinglem10  37504  stirlinglem11  37505  stirlinglem15  37509  dirkertrigeqlem1  37519  dirkercncflem2  37525  fourierdlem54  37582  fourierdlem56  37584  fourierdlem57  37585  fourierdlem102  37630  fourierdlem114  37642  fourierswlem  37652  fouriersw  37653  mod2eq1n2dvds  38105  m1expevenALTV  38157  dfeven2  38159  oexpnegALTV  38186  oexpnegnz  38187  2evenALTV  38201  2noddALTV  38202  nn0o1gt2ALTV  38203  nnpw2evenALTV  38209  perfectALTVlem1  38223  perfectALTVlem2  38224  sgoldbalt  38262  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  wtgoldbnnsum4prm  38277  bgoldbnnsum3prm  38279  proththdlem  38293  proththd  38294  3exp4mod41  38296  41prothprmlem2  38298  pfxtrcfv0  38323  pfxtrcfvl  38326  2even  38681  nn0le2is012  38898  zlmodzxzequa  39039  zlmodzxznm  39040  zlmodzxzequap  39042  zlmodzxzldeplem1  39043  zlmodzxzldeplem3  39045  zlmodzxzldep  39047  ldepsnlinclem1  39048  ldepsnlinc  39051  pw2m1lepw2m1  39069  nn0o  39080  fldivexpfllog2  39127  nnlog2ge0lt1  39128  logbpw2m1  39129  fllog2  39130  blennnelnn  39138  blenpw2  39140  nnpw2blenfzo  39143  blennnt2  39151  nnolog2flm1  39152  dig2nn0ld  39166  dig2nn1st  39167  0dig2pr01  39172  0dig2nn0o  39175