Theorem 2z 12174

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 11868	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 12166	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2112  2c2 11850  ℤcz 12141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-neg 11030  df-nn 11796  df-2 11858  df-z 12142

This theorem is referenced by:  nn0lt2  12205  nn0le2is012  12206  zadd2cl  12255  eluz4eluz2  12446  uzuzle23  12450  2eluzge1  12455  eluz2b1  12480  nn01to3  12502  nn0ge2m1nnALT  12503  ige2m1fz  13167  fz0to3un2pr  13179  fz0to4untppr  13180  fzctr  13189  fzo0to2pr  13292  fzo0to42pr  13294  2tnp1ge0ge0  13369  flhalf  13370  m1modge3gt1  13456  2txmodxeq0  13469  f13idfv  13538  sqrecd  13685  znsqcld  13697  sq1  13729  expnass  13741  sqoddm1div8  13775  bcn2m1  13855  bcn2p1  13856  4bc2eq6  13860  hashtpg  14016  ccat2s1p2  14154  ccat2s1p2OLD  14156  pfxtrcfv0  14224  pfxtrcfvl  14227  eqwrds3  14493  iseraltlem2  15211  iseraltlem3  15212  climcndslem1  15376  climcnds  15378  bpolydiflem  15579  efgt0  15627  tanval3  15658  cos01bnd  15710  cos01gt0  15715  odd2np1  15865  even2n  15866  oddm1even  15867  oddp1even  15868  oexpneg  15869  mod2eq1n2dvds  15871  2tp1odd  15876  2teven  15879  evend2  15881  oddp1d2  15882  ltoddhalfle  15885  opoe  15887  omoe  15888  opeo  15889  omeo  15890  z0even  15891  z2even  15894  z4even  15896  4dvdseven  15897  m1expo  15899  m1exp1  15900  nn0o  15907  sumeven  15911  flodddiv4  15937  bits0e  15951  bits0o  15952  bitsp1e  15954  bitsp1o  15955  bitsfzo  15957  bitsmod  15958  bitscmp  15960  bitsinv1lem  15963  bitsinv1  15964  6gcd4e2  16061  3lcm2e6woprm  16135  lcmf2a3a4e12  16167  isprm3  16203  dvdsnprmd  16210  2prm  16212  2mulprm  16213  oddprmge3  16220  ge2nprmge4  16221  isprm7  16228  divgcdodd  16230  oddprm  16326  pythagtriplem4  16335  pythagtriplem11  16341  pythagtriplem13  16343  iserodd  16351  prmgaplem3  16569  prmgaplem7  16573  dec2dvds  16579  prmlem0  16622  4001lem1  16657  psgnunilem4  18843  efgredleme  19087  lt6abl  19234  ablsimpgfindlem1  19448  ablsimpgfindlem2  19449  zringndrg  20409  znidomb  20480  chfacfscmulfsupp  21710  chfacfpmmulfsupp  21714  minveclem2  24277  minveclem3  24280  pjthlem1  24288  dyaddisjlem  24446  mbfi1fseqlem5  24571  dvrecg  24824  dvexp3  24829  aaliou3lem6  25195  tanregt0  25382  efif1olem4  25388  tanarg  25461  cxpsqrtth  25571  2irrexpq  25572  2logb9irr  25632  2logb9irrALT  25635  sqrt2cxp2logb9e3  25636  cubic2  25685  asinlem3  25708  atantayl2  25775  cxp2limlem  25812  lgamgulmlem3  25867  lgamgulmlem4  25868  basellem2  25918  basellem3  25919  basellem4  25920  basellem5  25921  basellem8  25924  basellem9  25925  ppisval  25940  ppiprm  25987  ppinprm  25988  chtprm  25989  chtnprm  25990  chtdif  25994  ppidif  25999  ppi1  26000  cht1  26001  cht3  26009  ppieq0  26012  ppiublem1  26037  chpeq0  26043  chtub  26047  chpval2  26053  chpub  26055  mersenne  26062  perfect1  26063  perfectlem1  26064  perfectlem2  26065  bposlem1  26119  bposlem2  26120  bposlem3  26121  bposlem5  26123  bposlem6  26124  lgslem1  26132  lgsdir2lem2  26161  lgsdir2  26165  lgsqr  26186  gausslemma2dlem0i  26199  gausslemma2dlem1a  26200  gausslemma2dlem5a  26205  gausslemma2dlem5  26206  gausslemma2dlem6  26207  gausslemma2dlem7  26208  gausslemma2d  26209  lgseisenlem1  26210  lgseisenlem2  26211  lgseisenlem3  26212  lgseisenlem4  26213  lgsquadlem1  26215  lgsquadlem2  26216  lgsquad2lem1  26219  lgsquad2lem2  26220  lgsquad2  26221  lgsquad3  26222  m1lgs  26223  2lgslem1a1  26224  2lgslem1a2  26225  2lgslem1b  26227  2lgslem3b1  26236  2lgslem3c1  26237  2lgs2  26240  2lgs  26242  2lgsoddprmlem2  26244  2lgsoddprmlem3  26249  2lgsoddprm  26251  2sqblem  26266  2sqmod  26271  chebbnd1lem1  26304  chebbnd1lem3  26306  chebbnd1  26307  dchrisum0lem1a  26321  dchrvmasumiflem1  26336  dchrisum0flblem1  26343  dchrisum0flblem2  26344  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  dchrisum0lem3  26354  mulog2sumlem2  26370  pntlemd  26429  pntlema  26431  pntlemb  26432  pntlemh  26434  pntlemr  26437  pntlemf  26440  pntlemo  26442  istrkg2ld  26505  istrkg3ld  26506  axlowdimlem3  26989  axlowdimlem6  26992  axlowdimlem16  27002  axlowdimlem17  27003  axlowdim  27006  usgrexmpldifpr  27300  usgrexmplef  27301  cusgrsizeindb1  27492  pthdlem1  27807  clwlkclwwlklem2a1  28029  clwlkclwwlklem2fv1  28032  clwlkclwwlklem2fv2  28033  clwlkclwwlklem2a4  28034  clwlkclwwlklem2a  28035  clwwisshclwwslem  28051  eupth2lem3lem3  28267  konigsberglem5  28293  2clwwlk2  28385  numclwwlk2lem1  28413  numclwlk2lem2f  28414  frgrreggt1  28430  ex-fl  28484  ex-mod  28486  ex-hash  28490  ex-dvds  28493  ex-ind-dvds  28498  minvecolem3  28911  pjhthlem1  29426  wrdt2ind  30899  archirngz  31116  archiabllem2c  31122  lmat22det  31440  dya2ub  31903  dya2icoseg  31910  oddpwdc  31987  eulerpartlemd  31999  eulerpartlemt  32004  ballotlem2  32121  signslema  32207  prodfzo03  32249  hgt750leme  32304  tgoldbachgtde  32306  nn0prpwlem  34197  knoppndvlem2  34379  knoppndvlem8  34385  irrdifflemf  35179  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  poimirlem28  35491  logblebd  39666  lcm2un  39705  lcm3un  39706  lcmineqlem18  39737  lcmineqlem19  39738  lcmineqlem21  39740  lcmineqlem22  39741  3lexlogpow5ineq2  39746  3lexlogpow2ineq1  39749  aks4d1p1p3  39759  aks4d1p1p4  39761  aks4d1p1p6  39763  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  5bc2eq10  39767  2np3bcnp1  39769  2ap1caineq  39770  flt4lem2  40128  flt4lem5  40131  flt4lem7  40140  nna4b4nsq  40141  acongrep  40446  acongeq  40449  jm2.18  40454  jm2.22  40461  jm2.23  40462  jm2.20nn  40463  jm2.26a  40466  jm2.26  40468  jm2.15nn0  40469  jm2.27a  40471  jm2.27c  40473  rmydioph  40480  jm3.1lem1  40483  jm3.1lem3  40485  expdiophlem1  40487  expdiophlem2  40488  hashnzfz2  41553  sumnnodd  42789  coskpi2  43025  cosknegpi  43028  dvdivbd  43082  stoweidlem26  43185  wallispilem4  43227  wallispi2lem1  43230  wallispi2lem2  43231  wallispi2  43232  stirlinglem1  43233  stirlinglem3  43235  stirlinglem7  43239  stirlinglem8  43240  stirlinglem10  43242  stirlinglem11  43243  stirlinglem15  43247  dirkertrigeqlem1  43257  dirkercncflem2  43263  fourierdlem54  43319  fourierdlem56  43321  fourierdlem57  43322  fourierdlem102  43367  fourierdlem114  43379  fourierswlem  43389  fouriersw  43390  smfmullem4  43943  fmtnorec1  44605  goldbachthlem2  44614  odz2prm2pw  44631  fmtnoprmfac1  44633  fmtnoprmfac2lem1  44634  fmtnoprmfac2  44635  fmtno4prmfac  44640  31prm  44665  sfprmdvdsmersenne  44671  lighneallem1  44673  lighneallem4a  44676  lighneallem4b  44677  lighneallem4  44678  proththdlem  44681  proththd  44682  3exp4mod41  44684  41prothprmlem2  44686  m1expevenALTV  44715  dfeven2  44717  m2even  44722  gcd2odd1  44736  oexpnegALTV  44745  oexpnegnz  44746  2evenALTV  44760  2noddALTV  44761  nn0o1gt2ALTV  44762  nnpw2evenALTV  44770  perfectALTVlem1  44789  perfectALTVlem2  44790  fppr2odd  44799  341fppr2  44802  9fppr8  44805  nfermltl2rev  44811  sbgoldbalt  44849  mogoldbb  44853  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  2even  45107  zlmodzxzequa  45453  zlmodzxznm  45454  zlmodzxzequap  45456  zlmodzxzldeplem1  45457  zlmodzxzldeplem3  45459  zlmodzxzldep  45461  ldepsnlinclem1  45462  ldepsnlinc  45465  pw2m1lepw2m1  45477  fldivexpfllog2  45527  nnlog2ge0lt1  45528  logbpw2m1  45529  fllog2  45530  blennnelnn  45538  blenpw2  45540  nnpw2blenfzo  45543  blennnt2  45551  nnolog2flm1  45552  dig2nn0ld  45566  dig2nn1st  45567  0dig2pr01  45572  0dig2nn0o  45575  ackval42  45658  itsclc0xyqsolr  45731