Theorem 2z 11868

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

Assertion

Ref	Expression
2z	⊢ 2 ∈ ℤ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 11564	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 11860	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2083  2c2 11546  ℤcz 11835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-i2m1 10458  ax-1ne0 10459  ax-rrecex 10462  ax-cnre 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-neg 10726  df-nn 11493  df-2 11554  df-z 11836

This theorem is referenced by:  nn0lt2  11899  nn0le2is012  11900  zadd2cl  11949  eluz4eluz2  12138  uzuzle23  12142  2eluzge1  12147  eluz2b1  12172  nn01to3  12194  nn0ge2m1nnALT  12195  ige2m1fz  12851  fz0to3un2pr  12863  fz0to4untppr  12864  fzctr  12873  fzo0to2pr  12976  fzo0to42pr  12978  2tnp1ge0ge0  13053  flhalf  13054  m1modge3gt1  13140  2txmodxeq0  13153  f13idfv  13222  sqrecd  13368  znsqcld  13380  sq1  13412  expnass  13424  sqoddm1div8  13458  bcn2m1  13538  bcn2p1  13539  4bc2eq6  13543  hashtpg  13693  ccat2s1p2  13832  pfxtrcfv0  13896  pfxtrcfvl  13899  eqwrds3  14163  iseraltlem2  14877  iseraltlem3  14878  climcndslem1  15041  climcnds  15043  bpolydiflem  15245  efgt0  15293  tanval3  15324  cos01bnd  15376  cos01gt0  15381  odd2np1  15527  even2n  15528  oddm1even  15529  oddp1even  15530  oexpneg  15531  mod2eq1n2dvds  15533  2tp1odd  15538  2teven  15541  evend2  15543  oddp1d2  15544  ltoddhalfle  15547  opoe  15549  omoe  15550  opeo  15551  omeo  15552  z0even  15553  n2dvds1OLD  15555  z2even  15557  n2dvds3OLD  15559  z4even  15560  4dvdseven  15561  m1expo  15563  m1exp1  15564  nn0o  15571  sumeven  15575  flodddiv4  15601  bits0e  15615  bits0o  15616  bitsp1e  15618  bitsp1o  15619  bitsfzo  15621  bitsmod  15622  bitscmp  15624  bitsinv1lem  15627  bitsinv1  15628  6gcd4e2  15719  3lcm2e6woprm  15792  lcmf2a3a4e12  15824  isprm3  15860  dvdsnprmd  15867  2prm  15869  2mulprm  15870  oddprmge3  15877  ge2nprmge4  15878  isprm7  15885  divgcdodd  15887  oddprm  15980  pythagtriplem4  15989  pythagtriplem11  15995  pythagtriplem13  15997  iserodd  16005  prmgaplem3  16222  prmgaplem7  16226  dec2dvds  16232  prmlem0  16272  4001lem1  16307  psgnunilem4  18360  efgredleme  18600  lt6abl  18740  zringndrg  20323  znidomb  20394  chfacfscmulfsupp  21155  chfacfpmmulfsupp  21159  minveclem2  23716  minveclem3  23719  pjthlem1  23727  dyaddisjlem  23883  mbfi1fseqlem5  24007  dvrecg  24257  dvexp3  24262  aaliou3lem6  24624  tanregt0  24808  efif1olem4  24814  tanarg  24887  cxpsqrtth  24997  2irrexpq  24998  2logb9irr  25058  2logb9irrALT  25061  sqrt2cxp2logb9e3  25062  cubic2  25111  asinlem3  25134  atantayl2  25201  cxp2limlem  25239  lgamgulmlem3  25294  lgamgulmlem4  25295  basellem2  25345  basellem3  25346  basellem4  25347  basellem5  25348  basellem8  25351  basellem9  25352  ppisval  25367  ppiprm  25414  ppinprm  25415  chtprm  25416  chtnprm  25417  chtdif  25421  ppidif  25426  ppi1  25427  cht1  25428  cht3  25436  ppieq0  25439  ppiublem1  25464  chpeq0  25470  chtub  25474  chpval2  25480  chpub  25482  mersenne  25489  perfect1  25490  perfectlem1  25491  perfectlem2  25492  bposlem1  25546  bposlem2  25547  bposlem3  25548  bposlem5  25550  bposlem6  25551  lgslem1  25559  lgsdir2lem2  25588  lgsdir2  25592  lgsqr  25613  gausslemma2dlem0i  25626  gausslemma2dlem1a  25627  gausslemma2dlem5a  25632  gausslemma2dlem5  25633  gausslemma2dlem6  25634  gausslemma2dlem7  25635  gausslemma2d  25636  lgseisenlem1  25637  lgseisenlem2  25638  lgseisenlem3  25639  lgseisenlem4  25640  lgsquadlem1  25642  lgsquadlem2  25643  lgsquad2lem1  25646  lgsquad2lem2  25647  lgsquad2  25648  lgsquad3  25649  m1lgs  25650  2lgslem1a1  25651  2lgslem1a2  25652  2lgslem1b  25654  2lgslem3b1  25663  2lgslem3c1  25664  2lgs2  25667  2lgs  25669  2lgsoddprmlem2  25671  2lgsoddprmlem3  25676  2lgsoddprm  25678  2sqblem  25693  2sqmod  25698  chebbnd1lem1  25731  chebbnd1lem3  25733  chebbnd1  25734  dchrisum0lem1a  25748  dchrvmasumiflem1  25763  dchrisum0flblem1  25770  dchrisum0flblem2  25771  dchrisum0lem1b  25777  dchrisum0lem1  25778  dchrisum0lem2a  25779  dchrisum0lem2  25780  dchrisum0lem3  25781  mulog2sumlem2  25797  pntlemd  25856  pntlema  25858  pntlemb  25859  pntlemh  25861  pntlemr  25864  pntlemf  25867  pntlemo  25869  istrkg2ld  25932  istrkg3ld  25933  axlowdimlem3  26417  axlowdimlem6  26420  axlowdimlem16  26430  axlowdimlem17  26431  axlowdim  26434  usgrexmpldifpr  26727  usgrexmplef  26728  cusgrsizeindb1  26919  pthdlem1  27233  clwlkclwwlklem2a1  27456  clwlkclwwlklem2fv1  27459  clwlkclwwlklem2fv2  27460  clwlkclwwlklem2a4  27461  clwlkclwwlklem2a  27462  clwwisshclwwslem  27478  eupth2lem3lem3  27695  konigsberglem5  27721  2clwwlk2  27815  numclwwlk2lem1  27843  numclwlk2lem2f  27844  frgrreggt1  27860  ex-fl  27914  ex-mod  27916  ex-hash  27920  ex-dvds  27923  ex-ind-dvds  27928  minvecolem3  28340  pjhthlem1  28855  wrdt2ind  30302  archirngz  30452  archiabllem2c  30458  lmat22det  30698  dya2ub  31141  dya2icoseg  31148  oddpwdc  31225  eulerpartlemd  31237  eulerpartlemt  31242  ballotlem2  31359  signslema  31445  prodfzo03  31487  hgt750leme  31542  tgoldbachgtde  31544  nn0prpwlem  33281  knoppndvlem2  33463  knoppndvlem8  33469  poimirlem25  34469  poimirlem26  34470  poimirlem27  34471  poimirlem28  34472  acongrep  39083  acongeq  39086  jm2.18  39091  jm2.22  39098  jm2.23  39099  jm2.20nn  39100  jm2.26a  39103  jm2.26  39105  jm2.15nn0  39106  jm2.27a  39108  jm2.27c  39110  rmydioph  39117  jm3.1lem1  39120  jm3.1lem3  39122  expdiophlem1  39124  expdiophlem2  39125  ablsimpgfindlem1  40186  ablsimpgfindlem2  40187  hashnzfz2  40212  sumnnodd  41474  coskpi2  41710  cosknegpi  41713  dvdivbd  41771  stoweidlem26  41875  wallispilem4  41917  wallispi2lem1  41920  wallispi2lem2  41921  wallispi2  41922  stirlinglem1  41923  stirlinglem3  41925  stirlinglem7  41929  stirlinglem8  41930  stirlinglem10  41932  stirlinglem11  41933  stirlinglem15  41937  dirkertrigeqlem1  41947  dirkercncflem2  41953  fourierdlem54  42009  fourierdlem56  42011  fourierdlem57  42012  fourierdlem102  42057  fourierdlem114  42069  fourierswlem  42079  fouriersw  42080  smfmullem4  42633  fmtnorec1  43203  goldbachthlem2  43212  odz2prm2pw  43229  fmtnoprmfac1  43231  fmtnoprmfac2lem1  43232  fmtnoprmfac2  43233  fmtno4prmfac  43238  31prm  43264  sfprmdvdsmersenne  43272  lighneallem1  43274  lighneallem4a  43277  lighneallem4b  43278  lighneallem4  43279  proththdlem  43282  proththd  43283  3exp4mod41  43285  41prothprmlem2  43287  m1expevenALTV  43316  dfeven2  43318  m2even  43323  gcd2odd1  43337  oexpnegALTV  43346  oexpnegnz  43347  2evenALTV  43361  2noddALTV  43362  nn0o1gt2ALTV  43363  nnpw2evenALTV  43371  perfectALTVlem1  43390  perfectALTVlem2  43391  fppr2odd  43400  341fppr2  43403  9fppr8  43406  nfermltl2rev  43412  sbgoldbalt  43450  mogoldbb  43454  nnsum4primesodd  43465  nnsum4primesoddALTV  43466  wtgoldbnnsum4prm  43471  bgoldbnnsum3prm  43473  2even  43704  zlmodzxzequa  44053  zlmodzxznm  44054  zlmodzxzequap  44056  zlmodzxzldeplem1  44057  zlmodzxzldeplem3  44059  zlmodzxzldep  44061  ldepsnlinclem1  44062  ldepsnlinc  44065  pw2m1lepw2m1  44078  fldivexpfllog2  44128  nnlog2ge0lt1  44129  logbpw2m1  44130  fllog2  44131  blennnelnn  44139  blenpw2  44141  nnpw2blenfzo  44144  blennnt2  44152  nnolog2flm1  44153  dig2nn0ld  44167  dig2nn1st  44168  0dig2pr01  44173  0dig2nn0o  44176  itsclc0xyqsolr  44259