Theorem 2z 12637

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

This proof depends on syntax axioms:   ∈ wcel 2146  2c2 12306  ℤcz 12602

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-i2m1 11179  ax-1ne0 11180  ax-rrecex 11183  ax-cnre 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11455  df-nn 12245  df-2 12314  df-z 12603

This theorem is used by:  nn0lt2  12670  nn0le2is012  12671  zadd2cl  12719  2eluzge1  12917  uzuzle23  12919  uzuzle24  12920  eluz2b1  12954  nn01to3  12976  nn0ge2m1nnALT  12977  ige2m1fz  13657  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  fzctr  13680  fzo0to2pr  13791  fzo0to42pr  13794  2tnp1ge0ge0  13875  flhalf  13876  m1modge3gt1  13967  2txmodxeq0  13980  f13idfv  14049  sqrecd  14199  znsqcld  14211  sq1  14244  expnass  14257  sqoddm1div8  14292  bcn2m1  14373  bcn2p1  14374  4bc2eq6  14378  hashtpg  14535  ccat2s1p2  14683  pfxtrcfv0  14748  pfxtrcfvl  14751  eqwrds3  15017  iseraltlem2  15753  iseraltlem3  15754  climcndslem1  15921  climcnds  15923  bpolydiflem  16125  efgt0  16176  tanval3  16207  cos01bnd  16259  cos01gt0  16264  odd2np1  16416  even2n  16417  oddm1even  16418  oddp1even  16419  oexpneg  16420  mod2eq1n2dvds  16422  2tp1odd  16427  2teven  16430  evend2  16432  oddp1d2  16433  ltoddhalfle  16436  opoe  16438  omoe  16439  opeo  16440  omeo  16441  z0even  16442  z2even  16445  z4even  16447  4dvdseven  16448  m1expo  16450  m1exp1  16451  nn0o  16458  sumeven  16462  flodddiv4  16490  bits0e  16504  bits0o  16505  bitsp1e  16507  bitsp1o  16508  bitsfzo  16510  bitsmod  16511  bitscmp  16513  bitsinv1lem  16516  bitsinv1  16517  6gcd4e2  16613  3lcm2e6woprm  16690  lcmf2a3a4e12  16722  isprm3  16758  dvdsnprmd  16765  2prm  16767  2mulprm  16768  oddprmge3  16776  ge2nprmge4  16777  isprm7  16784  divgcdodd  16786  oddprm  16887  pythagtriplem4  16896  pythagtriplem11  16902  pythagtriplem13  16904  iserodd  16912  prmgaplem3  17130  prmgaplem7  17134  dec2dvds  17140  prmlem0  17182  4001lem1  17218  ex-chn1  18710  psgnunilem4  19590  efgredleme  19836  lt6abl  19988  ablsimpgfindlem1  20202  ablsimpgfindlem2  20203  zringndrg  21647  znidomb  21740  chfacfscmulfsupp  23045  chfacfpmmulfsupp  23049  minveclem2  25614  minveclem3  25617  pjthlem1  25625  dyaddisjlem  25783  mbfi1fseqlem5  25907  dvrecg  26161  dvexp3  26166  aaliou3lem6  26540  tanregt0  26733  efif1olem4  26739  tanarg  26813  cxpsqrtth  26924  2irrexpq  26925  2logb9irr  26989  2logb9irrALT  26992  sqrt2cxp2logb9e3  26993  cubic2  27042  asinlem3  27065  atantayl2  27132  cxp2limlem  27169  lgamgulmlem3  27224  lgamgulmlem4  27225  basellem2  27275  basellem3  27276  basellem4  27277  basellem5  27278  basellem8  27281  basellem9  27282  ppisval  27297  ppiprm  27344  ppinprm  27345  chtprm  27346  chtnprm  27347  chtdif  27351  ppidif  27356  ppi1  27357  cht1  27358  cht3  27366  ppieq0  27369  ppiublem1  27395  chpeq0  27401  chtub  27405  chpval2  27411  chpub  27413  mersenne  27420  perfect1  27421  perfectlem1  27422  perfectlem2  27423  bposlem1  27477  bposlem2  27478  bposlem3  27479  bposlem5  27481  bposlem6  27482  lgslem1  27490  lgsdir2lem2  27519  lgsdir2  27523  lgsqr  27544  gausslemma2dlem0i  27557  gausslemma2dlem1a  27558  gausslemma2dlem5a  27563  gausslemma2dlem5  27564  gausslemma2dlem6  27565  gausslemma2dlem7  27566  gausslemma2d  27567  lgseisenlem1  27568  lgseisenlem2  27569  lgseisenlem3  27570  lgseisenlem4  27571  lgsquadlem1  27573  lgsquadlem2  27574  lgsquad2lem1  27577  lgsquad2lem2  27578  lgsquad2  27579  lgsquad3  27580  m1lgs  27581  2lgslem1a1  27582  2lgslem1a2  27583  2lgslem1b  27585  2lgslem3b1  27594  2lgslem3c1  27595  2lgs2  27598  2lgs  27600  2lgsoddprmlem2  27602  2lgsoddprmlem3  27607  2lgsoddprm  27609  2sqblem  27624  2sqmod  27629  chebbnd1lem1  27662  chebbnd1lem3  27664  chebbnd1  27665  dchrisum0lem1a  27679  dchrvmasumiflem1  27694  dchrisum0flblem1  27701  dchrisum0flblem2  27702  dchrisum0lem1b  27708  dchrisum0lem1  27709  dchrisum0lem2a  27710  dchrisum0lem2  27711  dchrisum0lem3  27712  mulog2sumlem2  27728  pntlemd  27787  pntlema  27789  pntlemb  27790  pntlemh  27792  pntlemr  27795  pntlemf  27798  pntlemo  27800  istrkg2ld  28758  istrkg3ld  28759  axlowdimlem3  29323  axlowdimlem6  29326  axlowdimlem16  29336  axlowdimlem17  29337  axlowdim  29340  usgrexmpldifpr  29637  usgrexmplef  29638  cusgrsizeindb1  29829  pthdlem1  30144  clwlkclwwlklem2a1  30372  clwlkclwwlklem2fv1  30375  clwlkclwwlklem2fv2  30376  clwlkclwwlklem2a4  30377  clwlkclwwlklem2a  30378  clwwisshclwwslem  30394  eupth2lem3lem3  30610  konigsberglem5  30636  2clwwlk2  30728  numclwwlk2lem1  30756  numclwlk2lem2f  30757  frgrreggt1  30773  ex-fl  30827  ex-mod  30829  ex-hash  30833  ex-dvds  30836  ex-ind-dvds  30841  minvecolem3  31257  pjhthlem1  31772  wrdt2ind  33298  archirngz  33532  archiabllem2c  33538  evl1deg2  33890  rtelextdg2  34140  constrext2chnlem  34163  constrresqrtcl  34190  2sqr3minply  34193  cos9thpiminplylem2  34196  cos9thpiminplylem5  34199  lmat22det  34235  dya2ub  34684  dya2icoseg  34691  oddpwdc  34768  eulerpartlemd  34780  eulerpartlemt  34785  ballotlem2  34903  signslema  34973  prodfzo03  35014  hgt750leme  35069  tgoldbachgtde  35071  nn0prpwlem  36866  knoppndvlem2  37135  knoppndvlem8  37141  irrdifflemf  38002  qdiff  38004  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem28  38332  logblebd  42777  lcm2un  42814  lcm3un  42815  lcmineqlem18  42846  lcmineqlem19  42847  lcmineqlem21  42849  lcmineqlem22  42850  3lexlogpow5ineq2  42855  3lexlogpow2ineq1  42858  aks4d1p1p3  42869  aks4d1p1p4  42871  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p3  42878  aks4d1p6  42881  aks4d1p7d1  42882  aks4d1p7  42883  aks4d1p8  42887  aks4d1p9  42888  posbezout  42900  5bc2eq10  42942  2np3bcnp1  42944  2ap1caineq  42945  aks6d1c6lem4  42973  aks6d1c7lem1  42980  aks6d1c7lem2  42981  flt4lem2  43412  flt4lem5  43415  flt4lem7  43424  nna4b4nsq  43425  acongrep  43740  acongeq  43743  jm2.18  43748  jm2.22  43755  jm2.23  43756  jm2.20nn  43757  jm2.26a  43760  jm2.26  43762  jm2.15nn0  43763  jm2.27a  43765  jm2.27c  43767  rmydioph  43774  jm3.1lem1  43777  jm3.1lem3  43779  expdiophlem1  43781  expdiophlem2  43782  hashnzfz2  45064  sumnnodd  46379  coskpi2  46613  cosknegpi  46616  dvdivbd  46670  stoweidlem26  46773  wallispilem4  46815  wallispi2lem1  46818  wallispi2lem2  46819  wallispi2  46820  stirlinglem1  46821  stirlinglem3  46823  stirlinglem7  46827  stirlinglem8  46828  stirlinglem10  46830  stirlinglem11  46831  stirlinglem15  46835  dirkertrigeqlem1  46845  dirkercncflem2  46851  fourierdlem54  46907  fourierdlem56  46909  fourierdlem57  46910  fourierdlem102  46955  fourierdlem114  46967  fourierswlem  46977  fouriersw  46978  smfmullem4  47541  evenwodadd  47635  nnmul2  48100  ceil5half3  48116  addmodne  48120  m1modnep2mod  48128  minusmodnep2tmod  48129  modmkpkne  48137  modmknepk  48138  modm2nep1  48142  modp2nep1  48143  modm1nep2  48144  modm1nem2  48145  2timesltsq  48148  2timesltsqm1  48149  fmtnorec1  48322  goldbachthlem2  48331  odz2prm2pw  48348  fmtnoprmfac1  48350  fmtnoprmfac2lem1  48351  fmtnoprmfac2  48352  fmtno4prmfac  48357  31prm  48382  sfprmdvdsmersenne  48388  lighneallem1  48390  lighneallem4a  48393  lighneallem4b  48394  lighneallem4  48395  proththdlem  48398  proththd  48399  3exp4mod41  48401  41prothprmlem2  48403  nprmdvdsfacm1lem1  48405  nprmdvdsfacm1lem2  48406  nprmdvdsfacm1lem4  48408  ppivalnnnprmge6  48411  ppivalnn  48417  m1expevenALTV  48445  dfeven2  48447  m2even  48452  gcd2odd1  48466  oexpnegALTV  48475  oexpnegnz  48476  2evenALTV  48490  2noddALTV  48491  nn0o1gt2ALTV  48492  nnpw2evenALTV  48500  perfectALTVlem1  48519  perfectALTVlem2  48520  fppr2odd  48529  341fppr2  48532  9fppr8  48535  nfermltl2rev  48541  sbgoldbalt  48579  mogoldbb  48583  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  wtgoldbnnsum4prm  48600  bgoldbnnsum3prm  48602  gpg5order  48858  gpg5nbgrvtx13starlem2  48870  gpg3nbgrvtx0ALT  48875  gpg3kgrtriexlem5  48885  gpg5gricstgr3  48888  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  gpg5edgnedg  48928  2even  49037  zlmodzxzequa  49309  zlmodzxznm  49310  zlmodzxzequap  49312  zlmodzxzldeplem1  49313  zlmodzxzldeplem3  49315  zlmodzxzldep  49317  ldepsnlinclem1  49318  ldepsnlinc  49321  pw2m1lepw2m1  49333  fldivexpfllog2  49378  nnlog2ge0lt1  49379  logbpw2m1  49380  fllog2  49381  blennnelnn  49389  blenpw2  49391  nnpw2blenfzo  49394  blennnt2  49402  nnolog2flm1  49403  dig2nn0ld  49417  dig2nn1st  49418  0dig2pr01  49423  0dig2nn0o  49426  ackval42  49509  itsclc0xyqsolr  49582  2elfz13  50659  crosspdotsumi  50679