Theorem 2z 12768

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

This proof depends on syntax axioms:   ∈ wcel 2147  2c2 12437  ℤcz 12733

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-neg 11583  df-nn 12376  df-2 12445  df-z 12734

This theorem is used by:  nn0lt2  12802  nn0le2is012  12803  zadd2cl  12851  2eluzge1  13049  uzuzle23  13051  uzuzle24  13052  eluz2b1  13086  nn01to3  13108  nn0ge2m1nnALT  13109  ige2m1fz  13791  fz0to3un2pr  13803  fz0to4untppr  13804  fz0to5un2tp  13805  fzctr  13814  fzo0to2pr  13925  fzo0to42pr  13928  2tnp1ge0ge0  14009  flhalf  14010  m1modge3gt1  14101  2txmodxeq0  14114  f13idfv  14183  sqrecd  14333  znsqcld  14345  sq1  14378  expnass  14392  sqoddm1div8  14428  bcn2m1  14509  bcn2p1  14510  4bc2eq6  14514  hashtpg  14671  ccat2s1p2  14820  pfxtrcfv0  14885  pfxtrcfvl  14888  eqwrds3  15157  iseraltlem2  15894  iseraltlem3  15895  climcndslem1  16062  climcnds  16064  bpolydiflem  16264  efgt0  16315  tanval3  16346  cos01bnd  16398  cos01gt0  16403  odd2np1  16555  even2n  16556  oddm1even  16557  oddp1even  16558  oexpneg  16559  mod2eq1n2dvds  16561  2tp1odd  16566  2teven  16569  evend2  16571  oddp1d2  16572  ltoddhalfle  16575  opoe  16577  omoe  16578  opeo  16579  omeo  16580  z0even  16581  z2even  16584  z4even  16586  4dvdseven  16587  m1expo  16589  m1exp1  16590  nn0o  16597  sumeven  16601  flodddiv4  16629  bits0e  16643  bits0o  16644  bitsp1e  16646  bitsp1o  16647  bitsfzo  16649  bitsmod  16650  bitscmp  16652  bitsinv1lem  16655  bitsinv1  16656  6gcd4e2  16755  3lcm2e6woprm  16834  lcmf2a3a4e12  16866  isprm3  16902  dvdsnprmd  16909  2prm  16911  2mulprm  16912  oddprmge3  16920  ge2nprmge4  16921  isprm7  16928  divgcdodd  16930  oddprm  17032  pythagtriplem4  17041  pythagtriplem11  17047  pythagtriplem13  17049  iserodd  17057  prmgaplem3  17275  prmgaplem7  17279  dec2dvds  17285  prmlem0  17327  4001lem1  17363  ex-chn1  18861  psgnunilem4  19762  efgredleme  20008  lt6abl  20160  ablsimpgfindlem1  20374  ablsimpgfindlem2  20375  zringndrg  21829  znidomb  21922  chfacfscmulfsupp  23232  chfacfpmmulfsupp  23236  minveclem2  25802  minveclem3  25805  pjthlem1  25813  dyaddisjlem  25971  mbfi1fseqlem5  26095  dvrecg  26348  dvexp3  26353  aaliou3lem6  26732  tanregt0  26924  efif1olem4  26930  tanarg  27004  cxpsqrtth  27115  2irrexpq  27116  2logb9irr  27180  2logb9irrALT  27183  sqrt2cxp2logb9e3  27184  cubic2  27233  asinlem3  27256  atantayl2  27323  cxp2limlem  27360  lgamgulmlem3  27415  lgamgulmlem4  27416  basellem2  27466  basellem3  27467  basellem4  27468  basellem5  27469  basellem8  27472  basellem9  27473  ppisval  27488  ppiprm  27535  ppinprm  27536  chtprm  27537  chtnprm  27538  chtdif  27542  ppidif  27547  ppi1  27548  cht1  27549  cht3  27557  ppieq0  27560  ppiublem1  27586  chpeq0  27592  chtub  27596  chpval2  27602  chpub  27604  mersenne  27611  perfect1  27612  perfectlem1  27613  perfectlem2  27614  bposlem1  27668  bposlem2  27669  bposlem3  27670  bposlem5  27672  bposlem6  27673  lgslem1  27681  lgsdir2lem2  27710  lgsdir2  27714  lgsqr  27735  gausslemma2dlem0i  27748  gausslemma2dlem1a  27749  gausslemma2dlem5a  27754  gausslemma2dlem5  27755  gausslemma2dlem6  27756  gausslemma2dlem7  27757  gausslemma2d  27758  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgsquadlem1  27764  lgsquadlem2  27765  lgsquad2lem1  27768  lgsquad2lem2  27769  lgsquad2  27770  lgsquad3  27771  m1lgs  27772  2lgslem1a1  27773  2lgslem1a2  27774  2lgslem1b  27776  2lgslem3b1  27785  2lgslem3c1  27786  2lgs2  27789  2lgs  27791  2lgsoddprmlem2  27793  2lgsoddprmlem3  27798  2lgsoddprm  27800  2sqblem  27815  2sqmod  27820  chebbnd1lem1  27853  chebbnd1lem3  27855  chebbnd1  27856  dchrisum0lem1a  27870  dchrvmasumiflem1  27885  dchrisum0flblem1  27892  dchrisum0flblem2  27893  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  dchrisum0lem3  27903  mulog2sumlem2  27919  pntlemd  27978  pntlema  27980  pntlemb  27981  pntlemh  27983  pntlemr  27986  pntlemf  27989  pntlemo  27991  flt4lem5  28037  flt4lem5e  28043  flt4lem7  28046  fltoprmlem2  28051  fltoprmgt3  28053  istrkg2ld  28979  istrkg3ld  28980  axlowdimlem3  29579  axlowdimlem6  29582  axlowdimlem16  29592  axlowdimlem17  29593  axlowdim  29596  usgrexmpldifpr  29896  usgrexmplef  29897  cusgrsizeindb1  30088  pthdlem1  30409  clwlkclwwlklem2a1  30640  clwlkclwwlklem2fv1  30643  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwwisshclwwslem  30662  eupth2lem3lem3  30888  konigsberglem5  30914  2clwwlk2  31006  numclwwlk2lem1  31034  numclwlk2lem2f  31035  frgrreggt1  31051  ex-fl  31105  ex-mod  31107  ex-hash  31111  ex-dvds  31114  ex-ind-dvds  31119  minvecolem3  31535  pjhthlem1  32050  wrdt2ind  33612  archirngz  33849  archiabllem2c  33855  evl1deg2  34212  rtelextdg2  34470  constrext2chnlem  34493  constrresqrtcl  34520  2sqr3minply  34523  cos9thpiminplylem2  34526  cos9thpiminplylem5  34529  lmat22det  34565  dya2ub  35013  dya2icoseg  35020  oddpwdc  35097  eulerpartlemd  35109  eulerpartlemt  35114  ballotlem2  35232  signslema  35302  prodfzo03  35343  hgt750leme  35398  tgoldbachgtde  35400  nn0prpwlem  37325  knoppndvlem2  37594  knoppndvlem8  37600  irrdifflemf  38514  qdiff  38516  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem28  38834  logblebd  43293  lcm2un  43330  lcm3un  43331  lcmineqlem18  43362  lcmineqlem19  43363  lcmineqlem21  43365  lcmineqlem22  43366  3lexlogpow5ineq2  43371  3lexlogpow2ineq1  43374  aks4d1p1p3  43385  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  aks4d1p3  43394  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  5bc2eq10  43458  2np3bcnp1  43460  2ap1caineq  43461  aks6d1c6lem4  43489  aks6d1c7lem1  43496  aks6d1c7lem2  43497  acongrep  44253  acongeq  44256  jm2.18  44261  jm2.22  44268  jm2.23  44269  jm2.20nn  44270  jm2.26a  44273  jm2.26  44275  jm2.15nn0  44276  jm2.27a  44278  jm2.27c  44280  rmydioph  44287  jm3.1lem1  44290  jm3.1lem3  44292  expdiophlem1  44294  expdiophlem2  44295  hashnzfz2  45566  sumnnodd  46915  coskpi2  47149  cosknegpi  47152  dvdivbd  47206  stoweidlem26  47309  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem7  47363  stirlinglem8  47364  stirlinglem10  47366  stirlinglem11  47367  stirlinglem15  47371  dirkertrigeqlem1  47381  dirkercncflem2  47387  fourierdlem54  47443  fourierdlem56  47445  fourierdlem57  47446  fourierdlem102  47491  fourierdlem114  47503  fourierswlem  47513  fouriersw  47514  smfmullem4  48077  evenwodadd  48184  sqrtnpoly  48216  nnmul2  48673  ceil5half3  48689  addmodne  48693  m1modnep2mod  48701  minusmodnep2tmod  48702  modmkpkne  48710  modmknepk  48711  modm2nep1  48715  modp2nep1  48716  modm1nep2  48717  modm1nem2  48718  2timesltsq  48721  2timesltsqm1  48722  fmtnorec1  48895  goldbachthlem2  48904  odz2prm2pw  48921  fmtnoprmfac1  48923  fmtnoprmfac2lem1  48924  fmtnoprmfac2  48925  fmtno4prmfac  48930  31prm  48955  sfprmdvdsmersenne  48961  lighneallem1  48963  lighneallem4a  48966  lighneallem4b  48967  lighneallem4  48968  proththdlem  48971  proththd  48972  3exp4mod41  48974  41prothprmlem2  48976  nprmdvdsfacm1lem1  48978  nprmdvdsfacm1lem2  48979  nprmdvdsfacm1lem4  48981  ppivalnnnprmge6  48984  ppivalnn  48990  m1expevenALTV  49018  dfeven2  49020  m2even  49025  gcd2odd1  49039  oexpnegALTV  49048  oexpnegnz  49049  2evenALTV  49063  2noddALTV  49064  nn0o1gt2ALTV  49065  nnpw2evenALTV  49073  perfectALTVlem1  49092  perfectALTVlem2  49093  fppr2odd  49102  341fppr2  49105  9fppr8  49108  nfermltl2rev  49114  sbgoldbalt  49152  mogoldbb  49156  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  gpg5order  49431  gpg5nbgrvtx13starlem2  49443  gpg3nbgrvtx0ALT  49448  gpg3kgrtriexlem5  49458  gpg5gricstgr3  49461  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  gpg5edgnedg  49501  2even  49609  bru1  49750  zlmodzxzequa  49939  zlmodzxznm  49940  zlmodzxzequap  49942  zlmodzxzldeplem1  49943  zlmodzxzldeplem3  49945  zlmodzxzldep  49947  ldepsnlinclem1  49948  ldepsnlinc  49951  pw2m1lepw2m1  49963  fldivexpfllog2  50008  nnlog2ge0lt1  50009  logbpw2m1  50010  fllog2  50011  blennnelnn  50019  blenpw2  50021  nnpw2blenfzo  50024  blennnt2  50032  nnolog2flm1  50033  dig2nn0ld  50047  dig2nn1st  50048  0dig2pr01  50053  0dig2nn0o  50056  ackval42  50139  itsclc0xyqsolr  50212  crosspdotsumlem  51392  veronesev2lem  51402