Theorem 2z 12732

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

This proof depends on syntax axioms:   ∈ wcel 2144  2c2 12401  ℤcz 12697

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-i2m1 11272  ax-1ne0 11273  ax-rrecex 11276  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-neg 11548  df-nn 12340  df-2 12409  df-z 12698

This theorem is used by:  nn0lt2  12766  nn0le2is012  12767  zadd2cl  12815  2eluzge1  13013  uzuzle23  13015  uzuzle24  13016  eluz2b1  13050  nn01to3  13072  nn0ge2m1nnALT  13073  ige2m1fz  13755  fz0to3un2pr  13767  fz0to4untppr  13768  fz0to5un2tp  13769  fzctr  13778  fzo0to2pr  13889  fzo0to42pr  13892  2tnp1ge0ge0  13973  flhalf  13974  m1modge3gt1  14065  2txmodxeq0  14078  f13idfv  14147  sqrecd  14297  znsqcld  14309  sq1  14342  expnass  14356  sqoddm1div8  14391  bcn2m1  14472  bcn2p1  14473  4bc2eq6  14477  hashtpg  14634  ccat2s1p2  14783  pfxtrcfv0  14848  pfxtrcfvl  14851  eqwrds3  15120  iseraltlem2  15856  iseraltlem3  15857  climcndslem1  16024  climcnds  16026  bpolydiflem  16226  efgt0  16277  tanval3  16308  cos01bnd  16360  cos01gt0  16365  odd2np1  16517  even2n  16518  oddm1even  16519  oddp1even  16520  oexpneg  16521  mod2eq1n2dvds  16523  2tp1odd  16528  2teven  16531  evend2  16533  oddp1d2  16534  ltoddhalfle  16537  opoe  16539  omoe  16540  opeo  16541  omeo  16542  z0even  16543  z2even  16546  z4even  16548  4dvdseven  16549  m1expo  16551  m1exp1  16552  nn0o  16559  sumeven  16563  flodddiv4  16591  bits0e  16605  bits0o  16606  bitsp1e  16608  bitsp1o  16609  bitsfzo  16611  bitsmod  16612  bitscmp  16614  bitsinv1lem  16617  bitsinv1  16618  6gcd4e2  16717  3lcm2e6woprm  16796  lcmf2a3a4e12  16828  isprm3  16864  dvdsnprmd  16871  2prm  16873  2mulprm  16874  oddprmge3  16882  ge2nprmge4  16883  isprm7  16890  divgcdodd  16892  oddprm  16994  pythagtriplem4  17003  pythagtriplem11  17009  pythagtriplem13  17011  iserodd  17019  prmgaplem3  17237  prmgaplem7  17241  dec2dvds  17247  prmlem0  17289  4001lem1  17325  ex-chn1  18817  psgnunilem4  19717  efgredleme  19963  lt6abl  20115  ablsimpgfindlem1  20329  ablsimpgfindlem2  20330  zringndrg  21780  znidomb  21873  chfacfscmulfsupp  23183  chfacfpmmulfsupp  23187  minveclem2  25753  minveclem3  25756  pjthlem1  25764  dyaddisjlem  25922  mbfi1fseqlem5  26046  dvrecg  26299  dvexp3  26304  aaliou3lem6  26681  tanregt0  26873  efif1olem4  26879  tanarg  26953  cxpsqrtth  27064  2irrexpq  27065  2logb9irr  27129  2logb9irrALT  27132  sqrt2cxp2logb9e3  27133  cubic2  27182  asinlem3  27205  atantayl2  27272  cxp2limlem  27309  lgamgulmlem3  27364  lgamgulmlem4  27365  basellem2  27415  basellem3  27416  basellem4  27417  basellem5  27418  basellem8  27421  basellem9  27422  ppisval  27437  ppiprm  27484  ppinprm  27485  chtprm  27486  chtnprm  27487  chtdif  27491  ppidif  27496  ppi1  27497  cht1  27498  cht3  27506  ppieq0  27509  ppiublem1  27535  chpeq0  27541  chtub  27545  chpval2  27551  chpub  27553  mersenne  27560  perfect1  27561  perfectlem1  27562  perfectlem2  27563  bposlem1  27617  bposlem2  27618  bposlem3  27619  bposlem5  27621  bposlem6  27622  lgslem1  27630  lgsdir2lem2  27659  lgsdir2  27663  lgsqr  27684  gausslemma2dlem0i  27697  gausslemma2dlem1a  27698  gausslemma2dlem5a  27703  gausslemma2dlem5  27704  gausslemma2dlem6  27705  gausslemma2dlem7  27706  gausslemma2d  27707  lgseisenlem1  27708  lgseisenlem2  27709  lgseisenlem3  27710  lgseisenlem4  27711  lgsquadlem1  27713  lgsquadlem2  27714  lgsquad2lem1  27717  lgsquad2lem2  27718  lgsquad2  27719  lgsquad3  27720  m1lgs  27721  2lgslem1a1  27722  2lgslem1a2  27723  2lgslem1b  27725  2lgslem3b1  27734  2lgslem3c1  27735  2lgs2  27738  2lgs  27740  2lgsoddprmlem2  27742  2lgsoddprmlem3  27747  2lgsoddprm  27749  2sqblem  27764  2sqmod  27769  chebbnd1lem1  27802  chebbnd1lem3  27804  chebbnd1  27805  dchrisum0lem1a  27819  dchrvmasumiflem1  27834  dchrisum0flblem1  27841  dchrisum0flblem2  27842  dchrisum0lem1b  27848  dchrisum0lem1  27849  dchrisum0lem2a  27850  dchrisum0lem2  27851  dchrisum0lem3  27852  mulog2sumlem2  27868  pntlemd  27927  pntlema  27929  pntlemb  27930  pntlemh  27932  pntlemr  27935  pntlemf  27938  pntlemo  27940  flt4lem5  27986  flt4lem5e  27992  flt4lem7  27995  fltoprmlem2  28000  fltoprmgt3  28002  istrkg2ld  28928  istrkg3ld  28929  axlowdimlem3  29528  axlowdimlem6  29531  axlowdimlem16  29541  axlowdimlem17  29542  axlowdim  29545  usgrexmpldifpr  29845  usgrexmplef  29846  cusgrsizeindb1  30037  pthdlem1  30358  clwlkclwwlklem2a1  30589  clwlkclwwlklem2fv1  30592  clwlkclwwlklem2fv2  30593  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwwisshclwwslem  30611  eupth2lem3lem3  30837  konigsberglem5  30863  2clwwlk2  30955  numclwwlk2lem1  30983  numclwlk2lem2f  30984  frgrreggt1  31000  ex-fl  31054  ex-mod  31056  ex-hash  31060  ex-dvds  31063  ex-ind-dvds  31068  minvecolem3  31484  pjhthlem1  31999  wrdt2ind  33563  archirngz  33797  archiabllem2c  33803  evl1deg2  34156  rtelextdg2  34406  constrext2chnlem  34429  constrresqrtcl  34456  2sqr3minply  34459  cos9thpiminplylem2  34462  cos9thpiminplylem5  34465  lmat22det  34501  dya2ub  34949  dya2icoseg  34956  oddpwdc  35033  eulerpartlemd  35045  eulerpartlemt  35050  ballotlem2  35168  signslema  35238  prodfzo03  35279  hgt750leme  35334  tgoldbachgtde  35336  nn0prpwlem  37203  knoppndvlem2  37472  knoppndvlem8  37478  irrdifflemf  38340  qdiff  38342  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  logblebd  43121  lcm2un  43158  lcm3un  43159  lcmineqlem18  43190  lcmineqlem19  43191  lcmineqlem21  43193  lcmineqlem22  43194  3lexlogpow5ineq2  43199  3lexlogpow2ineq1  43202  aks4d1p1p3  43213  aks4d1p1p4  43215  aks4d1p1p6  43217  aks4d1p1p7  43218  aks4d1p1p5  43219  aks4d1p1  43220  aks4d1p3  43222  aks4d1p6  43225  aks4d1p7d1  43226  aks4d1p7  43227  aks4d1p8  43231  aks4d1p9  43232  posbezout  43244  5bc2eq10  43286  2np3bcnp1  43288  2ap1caineq  43289  aks6d1c6lem4  43317  aks6d1c7lem1  43324  aks6d1c7lem2  43325  acongrep  44081  acongeq  44084  jm2.18  44089  jm2.22  44096  jm2.23  44097  jm2.20nn  44098  jm2.26a  44101  jm2.26  44103  jm2.15nn0  44104  jm2.27a  44106  jm2.27c  44108  rmydioph  44115  jm3.1lem1  44118  jm3.1lem3  44120  expdiophlem1  44122  expdiophlem2  44123  hashnzfz2  45399  sumnnodd  46736  coskpi2  46970  cosknegpi  46973  dvdivbd  47027  stoweidlem26  47130  wallispilem4  47172  wallispi2lem1  47175  wallispi2lem2  47176  wallispi2  47177  stirlinglem1  47178  stirlinglem3  47180  stirlinglem7  47184  stirlinglem8  47185  stirlinglem10  47187  stirlinglem11  47188  stirlinglem15  47192  dirkertrigeqlem1  47202  dirkercncflem2  47208  fourierdlem54  47264  fourierdlem56  47266  fourierdlem57  47267  fourierdlem102  47312  fourierdlem114  47324  fourierswlem  47334  fouriersw  47335  smfmullem4  47898  evenwodadd  48005  sqrtnpoly  48037  nnmul2  48494  ceil5half3  48510  addmodne  48514  m1modnep2mod  48522  minusmodnep2tmod  48523  modmkpkne  48531  modmknepk  48532  modm2nep1  48536  modp2nep1  48537  modm1nep2  48538  modm1nem2  48539  2timesltsq  48542  2timesltsqm1  48543  fmtnorec1  48716  goldbachthlem2  48725  odz2prm2pw  48742  fmtnoprmfac1  48744  fmtnoprmfac2lem1  48745  fmtnoprmfac2  48746  fmtno4prmfac  48751  31prm  48776  sfprmdvdsmersenne  48782  lighneallem1  48784  lighneallem4a  48787  lighneallem4b  48788  lighneallem4  48789  proththdlem  48792  proththd  48793  3exp4mod41  48795  41prothprmlem2  48797  nprmdvdsfacm1lem1  48799  nprmdvdsfacm1lem2  48800  nprmdvdsfacm1lem4  48802  ppivalnnnprmge6  48805  ppivalnn  48811  m1expevenALTV  48839  dfeven2  48841  m2even  48846  gcd2odd1  48860  oexpnegALTV  48869  oexpnegnz  48870  2evenALTV  48884  2noddALTV  48885  nn0o1gt2ALTV  48886  nnpw2evenALTV  48894  perfectALTVlem1  48913  perfectALTVlem2  48914  fppr2odd  48923  341fppr2  48926  9fppr8  48929  nfermltl2rev  48935  sbgoldbalt  48973  mogoldbb  48977  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  wtgoldbnnsum4prm  48994  bgoldbnnsum3prm  48996  gpg5order  49252  gpg5nbgrvtx13starlem2  49264  gpg3nbgrvtx0ALT  49269  gpg3kgrtriexlem5  49279  gpg5gricstgr3  49282  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  gpg5edgnedg  49322  2even  49430  zlmodzxzequa  49702  zlmodzxznm  49703  zlmodzxzequap  49705  zlmodzxzldeplem1  49706  zlmodzxzldeplem3  49708  zlmodzxzldep  49710  ldepsnlinclem1  49711  ldepsnlinc  49714  pw2m1lepw2m1  49726  fldivexpfllog2  49771  nnlog2ge0lt1  49772  logbpw2m1  49773  fllog2  49774  blennnelnn  49782  blenpw2  49784  nnpw2blenfzo  49787  blennnt2  49795  nnolog2flm1  49796  dig2nn0ld  49810  dig2nn1st  49811  0dig2pr01  49816  0dig2nn0o  49819  ackval42  49902  itsclc0xyqsolr  49975  crosspdotsumlem  51133  veronesev2lem  51143