Theorem 2z 10896

Description: Two 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 10693	. 2 |- 2 e. NN
2	1	nnzi 10888	1 |- 2 e. ZZ

Syntax hints:   e. wcel 1767   2c2 10585   ZZcz 10864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-recs 7042  df-rdg 7076  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-2 10594  df-z 10865

This theorem is referenced by:  nn0lt2  10925  zadd2cl  10973  uzuzle23  11122  2eluzge0  11126  2eluzge1  11127  eluz2b1  11153  nn01to3  11175  nn0ge2m1nnALT  11176  ige2m1fz  11767  fzctr  11784  4fvwrd4  11790  fzo0to2pr  11867  fzo0to42pr  11869  flhalf  11930  2txmodxeq0  12015  f13idfv  12074  sq1  12230  expnass  12241  sqrecd  12282  bcn2m1  12370  bcn2p1  12371  hashtpg  12489  ccat2s1p2  12596  ccatw2s1p1  12603  swrdtrcfv0  12632  swrdtrcfvl  12638  iseraltlem2  13468  iseraltlem3  13469  climcndslem1  13624  climcnds  13626  efgt0  13699  tanval3  13730  cos01bnd  13782  cos01gt0  13787  n2dvds1  13894  odd2np1  13905  oddm1even  13906  oddp1even  13907  oexpneg  13908  bits0e  13938  bits0o  13939  bitsp1e  13941  bitsp1o  13942  bitsfzo  13944  bitsmod  13945  bitscmp  13947  bitsinv1lem  13950  bitsinv1  13951  isprm3  14085  2prm  14092  3prm  14093  prmn2uzge3  14096  divgcdodd  14119  opoe  14194  omoe  14195  opeo  14196  omeo  14197  oddprm  14198  pythagtriplem4  14202  pythagtriplem11  14208  pythagtriplem13  14210  iserodd  14218  dec2dvds  14408  prmlem0  14449  4001lem1  14481  psgnunilem4  16328  efgredleme  16567  lt6abl  16700  znidomb  18395  chfacfscmulfsupp  19155  chfacfpmmulfsupp  19159  minveclem2  21604  minveclem3  21607  pjthlem1  21615  dyaddisjlem  21767  mbfi1fseqlem5  21889  iblcnlem1  21957  dvexp3  22142  aaliou3lem6  22506  tanregt0  22687  efif1olem4  22693  tanarg  22760  cubic2  22935  asinlem3  22958  atantayl2  23025  cxp2limlem  23061  basellem2  23111  basellem3  23112  basellem4  23113  basellem5  23114  basellem8  23117  basellem9  23118  ppisval  23133  ppiprm  23181  ppinprm  23182  chtprm  23183  chtnprm  23184  chtdif  23188  ppidif  23193  ppi1  23194  cht1  23195  cht3  23203  ppieq0  23206  ppiublem1  23233  ppiublem2  23234  chpeq0  23239  chtub  23243  chpval2  23249  chpub  23251  mersenne  23258  perfect1  23259  perfectlem1  23260  perfectlem2  23261  bposlem1  23315  bposlem2  23316  bposlem3  23317  bposlem5  23319  bposlem6  23320  lgslem1  23327  lgsdir2lem2  23355  lgsdir2lem3  23356  lgsdir2  23359  lgsqr  23377  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem3  23382  lgseisenlem4  23383  lgsquadlem1  23385  lgsquadlem2  23386  lgsquad2lem1  23389  lgsquad2lem2  23390  lgsquad2  23391  lgsquad3  23392  m1lgs  23393  2sqblem  23408  chebbnd1lem1  23410  chebbnd1lem3  23412  chebbnd1  23413  dchrisum0lem1a  23427  dchrvmasumiflem1  23442  dchrisum0flblem1  23449  dchrisum0flblem2  23450  dchrisum0lem1b  23456  dchrisum0lem1  23457  dchrisum0lem2a  23458  dchrisum0lem2  23459  dchrisum0lem3  23460  mulog2sumlem2  23476  pntlemd  23535  pntlema  23537  pntlemb  23538  pntlemh  23540  pntlemr  23543  pntlemf  23546  pntlemo  23548  istrkg2ld  23614  axlowdimlem3  23951  axlowdimlem6  23954  axlowdimlem16  23964  axlowdimlem17  23965  axlowdim  23968  usgraexvlem  24099  usgraexmpldifpr  24104  usgraexmpl  24105  cusgrasizeindb1  24175  2wlklemC  24262  2trllemD  24263  2trllemG  24264  wlkntrllem2  24266  constr2spthlem1  24300  2pthon  24308  usgra2adedgwlkonALT  24320  usgra2wlkspthlem2  24324  3v3e3cycl1  24348  constr3lem4  24351  constr3trllem2  24355  constr3trllem3  24356  constr3trllem5  24358  constr3pthlem1  24359  constr3pthlem2  24360  4cycl4v4e  24370  4cycl4dv4e  24372  clwlkisclwwlklem2a1  24483  clwlkisclwwlklem2fv1  24486  clwlkisclwwlklem2fv2  24487  clwlkisclwwlklem2a4  24488  clwlkisclwwlklem2a  24489  clwwisshclwwlem  24510  eupath2lem3  24683  eupath2  24684  frgrawopreglem2  24750  extwwlkfablem2  24783  numclwwlkovf2ex  24791  numclwwlk2lem1  24807  numclwlk2lem2f  24808  frgrareggt1  24821  ex-fl  24873  ex-dvds  24874  minvecolem3  25496  pjhthlem1  26013  archirngz  27423  archiabllem2c  27429  rnlogblem  27683  dya2ub  27909  dya2icoseg  27916  oddpwdc  27961  eulerpartlemd  27973  eulerpartlemt  27978  ballotlem2  28095  ballotlemfc0  28099  ballotlemfcc  28100  signslema  28187  lgamgulmlem3  28241  lgamgulmlem4  28242  4bc2eq6  28615  bpolydiflem  29421  nn0prpwlem  29745  acongrep  30550  acongeq  30553  jm2.18  30562  jm2.22  30569  jm2.23  30570  jm2.20nn  30571  jm2.26a  30574  jm2.26  30576  jm2.15nn0  30577  jm2.27a  30579  jm2.27c  30581  rmydioph  30588  jm3.1lem1  30591  jm3.1lem3  30593  expdiophlem1  30595  expdiophlem2  30596  isprm7  30823  3lcm2e6  30847  hashnzfz2  30854  sumnnodd  31200  coskpi2  31230  cosknegpi  31233  dvrecg  31268  dvdivbd  31281  stoweidlem26  31354  wallispilem4  31396  wallispi2lem1  31399  wallispi2lem2  31400  wallispi2  31401  stirlinglem1  31402  stirlinglem3  31404  stirlinglem7  31408  stirlinglem8  31409  stirlinglem10  31411  stirlinglem11  31412  stirlinglem15  31416  dirkertrigeqlem1  31426  dirkercncflem2  31432  fourierdlem54  31489  fourierdlem56  31491  fourierdlem57  31492  fourierdlem102  31537  fourierdlem114  31549  fourierswlem  31559  fouriersw  31560  nn0le2is012  32053  zlmodzxzequa  32196  zlmodzxznm  32197  zlmodzxzequap  32199  zlmodzxzldeplem1  32200  zlmodzxzldeplem3  32202  zlmodzxzldep  32204  ldepsnlinclem1  32205  ldepsnlinc  32208