Theorem 2z 12597

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

Syntax hints:   ∈ wcel 2141  2c2 12266  ℤcz 12562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-i2m1 11135  ax-1ne0 11136  ax-rrecex 11139  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-neg 11411  df-nn 12205  df-2 12274  df-z 12563

This theorem is referenced by:  nn0lt2  12630  nn0le2is012  12631  zadd2cl  12679  2eluzge1  12877  uzuzle23  12879  uzuzle24  12880  eluz2b1  12914  nn01to3  12936  nn0ge2m1nnALT  12937  ige2m1fz  13616  fz0to3un2pr  13628  fz0to4untppr  13629  fz0to5un2tp  13630  fzctr  13639  fzo0to2pr  13750  fzo0to42pr  13753  2tnp1ge0ge0  13833  flhalf  13834  m1modge3gt1  13925  2txmodxeq0  13938  f13idfv  14007  sqrecd  14157  znsqcld  14169  sq1  14202  expnass  14215  sqoddm1div8  14250  bcn2m1  14331  bcn2p1  14332  4bc2eq6  14336  hashtpg  14492  ccat2s1p2  14638  pfxtrcfv0  14701  pfxtrcfvl  14704  eqwrds3  14968  iseraltlem2  15701  iseraltlem3  15702  climcndslem1  15870  climcnds  15872  bpolydiflem  16075  efgt0  16126  tanval3  16157  cos01bnd  16209  cos01gt0  16214  odd2np1  16366  even2n  16367  oddm1even  16368  oddp1even  16369  oexpneg  16370  mod2eq1n2dvds  16372  2tp1odd  16377  2teven  16380  evend2  16382  oddp1d2  16383  ltoddhalfle  16386  opoe  16388  omoe  16389  opeo  16390  omeo  16391  z0even  16392  z2even  16395  z4even  16397  4dvdseven  16398  m1expo  16400  m1exp1  16401  nn0o  16408  sumeven  16412  flodddiv4  16440  bits0e  16454  bits0o  16455  bitsp1e  16457  bitsp1o  16458  bitsfzo  16460  bitsmod  16461  bitscmp  16463  bitsinv1lem  16466  bitsinv1  16467  6gcd4e2  16563  3lcm2e6woprm  16640  lcmf2a3a4e12  16672  isprm3  16708  dvdsnprmd  16715  2prm  16717  2mulprm  16718  oddprmge3  16726  ge2nprmge4  16727  isprm7  16734  divgcdodd  16736  oddprm  16837  pythagtriplem4  16846  pythagtriplem11  16852  pythagtriplem13  16854  iserodd  16862  prmgaplem3  17080  prmgaplem7  17084  dec2dvds  17090  prmlem0  17132  4001lem1  17168  ex-chn1  18660  psgnunilem4  19528  efgredleme  19774  lt6abl  19926  ablsimpgfindlem1  20140  ablsimpgfindlem2  20141  zringndrg  21508  znidomb  21601  chfacfscmulfsupp  22907  chfacfpmmulfsupp  22911  minveclem2  25476  minveclem3  25479  pjthlem1  25487  dyaddisjlem  25645  mbfi1fseqlem5  25769  dvrecg  26023  dvexp3  26028  aaliou3lem6  26400  tanregt0  26592  efif1olem4  26598  tanarg  26672  cxpsqrtth  26783  2irrexpq  26784  2logb9irr  26848  2logb9irrALT  26851  sqrt2cxp2logb9e3  26852  cubic2  26901  asinlem3  26924  atantayl2  26991  cxp2limlem  27028  lgamgulmlem3  27083  lgamgulmlem4  27084  basellem2  27134  basellem3  27135  basellem4  27136  basellem5  27137  basellem8  27140  basellem9  27141  ppisval  27156  ppiprm  27203  ppinprm  27204  chtprm  27205  chtnprm  27206  chtdif  27210  ppidif  27215  ppi1  27216  cht1  27217  cht3  27225  ppieq0  27228  ppiublem1  27254  chpeq0  27260  chtub  27264  chpval2  27270  chpub  27272  mersenne  27279  perfect1  27280  perfectlem1  27281  perfectlem2  27282  bposlem1  27336  bposlem2  27337  bposlem3  27338  bposlem5  27340  bposlem6  27341  lgslem1  27349  lgsdir2lem2  27378  lgsdir2  27382  lgsqr  27403  gausslemma2dlem0i  27416  gausslemma2dlem1a  27417  gausslemma2dlem5a  27422  gausslemma2dlem5  27423  gausslemma2dlem6  27424  gausslemma2dlem7  27425  gausslemma2d  27426  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgseisenlem4  27430  lgsquadlem1  27432  lgsquadlem2  27433  lgsquad2lem1  27436  lgsquad2lem2  27437  lgsquad2  27438  lgsquad3  27439  m1lgs  27440  2lgslem1a1  27441  2lgslem1a2  27442  2lgslem1b  27444  2lgslem3b1  27453  2lgslem3c1  27454  2lgs2  27457  2lgs  27459  2lgsoddprmlem2  27461  2lgsoddprmlem3  27466  2lgsoddprm  27468  2sqblem  27483  2sqmod  27488  chebbnd1lem1  27521  chebbnd1lem3  27523  chebbnd1  27524  dchrisum0lem1a  27538  dchrvmasumiflem1  27553  dchrisum0flblem1  27560  dchrisum0flblem2  27561  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2a  27569  dchrisum0lem2  27570  dchrisum0lem3  27571  mulog2sumlem2  27587  pntlemd  27646  pntlema  27648  pntlemb  27649  pntlemh  27651  pntlemr  27654  pntlemf  27657  pntlemo  27659  istrkg2ld  28617  istrkg3ld  28618  axlowdimlem3  29102  axlowdimlem6  29105  axlowdimlem16  29115  axlowdimlem17  29116  axlowdim  29119  usgrexmpldifpr  29416  usgrexmplef  29417  cusgrsizeindb1  29608  pthdlem1  29923  clwlkclwwlklem2a1  30151  clwlkclwwlklem2fv1  30154  clwlkclwwlklem2fv2  30155  clwlkclwwlklem2a4  30156  clwlkclwwlklem2a  30157  clwwisshclwwslem  30173  eupth2lem3lem3  30389  konigsberglem5  30415  2clwwlk2  30507  numclwwlk2lem1  30535  numclwlk2lem2f  30536  frgrreggt1  30552  ex-fl  30606  ex-mod  30608  ex-hash  30612  ex-dvds  30615  ex-ind-dvds  30620  minvecolem3  31036  pjhthlem1  31551  wrdt2ind  33092  archirngz  33330  archiabllem2c  33336  evl1deg2  33734  rtelextdg2  33985  constrext2chnlem  34008  constrresqrtcl  34035  2sqr3minply  34038  cos9thpiminplylem2  34041  cos9thpiminplylem5  34044  lmat22det  34080  dya2ub  34528  dya2icoseg  34535  oddpwdc  34612  eulerpartlemd  34624  eulerpartlemt  34629  ballotlem2  34747  signslema  34817  prodfzo03  34858  hgt750leme  34913  tgoldbachgtde  34915  nn0prpwlem  36643  knoppndvlem2  36912  knoppndvlem8  36918  irrdifflemf  37778  qdiff  37780  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  logblebd  42555  lcm2un  42592  lcm3un  42593  lcmineqlem18  42624  lcmineqlem19  42625  lcmineqlem21  42627  lcmineqlem22  42628  3lexlogpow5ineq2  42633  3lexlogpow2ineq1  42636  aks4d1p1p3  42647  aks4d1p1p4  42649  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  aks4d1p1  42654  aks4d1p3  42656  aks4d1p6  42659  aks4d1p7d1  42660  aks4d1p7  42661  aks4d1p8  42665  aks4d1p9  42666  posbezout  42678  5bc2eq10  42720  2np3bcnp1  42722  2ap1caineq  42723  aks6d1c6lem4  42751  aks6d1c7lem1  42758  aks6d1c7lem2  42759  flt4lem2  43190  flt4lem5  43193  flt4lem7  43202  nna4b4nsq  43203  acongrep  43518  acongeq  43521  jm2.18  43526  jm2.22  43533  jm2.23  43534  jm2.20nn  43535  jm2.26a  43538  jm2.26  43540  jm2.15nn0  43541  jm2.27a  43543  jm2.27c  43545  rmydioph  43552  jm3.1lem1  43555  jm3.1lem3  43557  expdiophlem1  43559  expdiophlem2  43560  hashnzfz2  44858  sumnnodd  46167  coskpi2  46401  cosknegpi  46404  dvdivbd  46458  stoweidlem26  46561  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  wallispi2  46608  stirlinglem1  46609  stirlinglem3  46611  stirlinglem7  46615  stirlinglem8  46616  stirlinglem10  46618  stirlinglem11  46619  stirlinglem15  46623  dirkertrigeqlem1  46633  dirkercncflem2  46639  fourierdlem54  46695  fourierdlem56  46697  fourierdlem57  46698  fourierdlem102  46743  fourierdlem114  46755  fourierswlem  46765  fouriersw  46766  smfmullem4  47329  nthrucw  47423  evenwodadd  47424  nnmul2  47885  ceil5half3  47901  addmodne  47905  m1modnep2mod  47913  minusmodnep2tmod  47914  modmkpkne  47922  modmknepk  47923  modm2nep1  47927  modp2nep1  47928  modm1nep2  47929  modm1nem2  47930  2timesltsq  47933  2timesltsqm1  47934  fmtnorec1  48107  goldbachthlem2  48116  odz2prm2pw  48133  fmtnoprmfac1  48135  fmtnoprmfac2lem1  48136  fmtnoprmfac2  48137  fmtno4prmfac  48142  31prm  48167  sfprmdvdsmersenne  48173  lighneallem1  48175  lighneallem4a  48178  lighneallem4b  48179  lighneallem4  48180  proththdlem  48183  proththd  48184  3exp4mod41  48186  41prothprmlem2  48188  nprmdvdsfacm1lem1  48190  nprmdvdsfacm1lem2  48191  nprmdvdsfacm1lem4  48193  ppivalnnnprmge6  48196  ppivalnn  48202  m1expevenALTV  48230  dfeven2  48232  m2even  48237  gcd2odd1  48251  oexpnegALTV  48260  oexpnegnz  48261  2evenALTV  48275  2noddALTV  48276  nn0o1gt2ALTV  48277  nnpw2evenALTV  48285  perfectALTVlem1  48304  perfectALTVlem2  48305  fppr2odd  48314  341fppr2  48317  9fppr8  48320  nfermltl2rev  48326  sbgoldbalt  48364  mogoldbb  48368  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  wtgoldbnnsum4prm  48385  bgoldbnnsum3prm  48387  gpg5order  48643  gpg5nbgrvtx13starlem2  48655  gpg3nbgrvtx0ALT  48660  gpg3kgrtriexlem5  48670  gpg5gricstgr3  48673  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  gpg5edgnedg  48713  2even  48822  zlmodzxzequa  49079  zlmodzxznm  49080  zlmodzxzequap  49082  zlmodzxzldeplem1  49083  zlmodzxzldeplem3  49085  zlmodzxzldep  49087  ldepsnlinclem1  49088  ldepsnlinc  49091  pw2m1lepw2m1  49103  fldivexpfllog2  49148  nnlog2ge0lt1  49149  logbpw2m1  49150  fllog2  49151  blennnelnn  49159  blenpw2  49161  nnpw2blenfzo  49164  blennnt2  49172  nnolog2flm1  49173  dig2nn0ld  49187  dig2nn1st  49188  0dig2pr01  49193  0dig2nn0o  49196  ackval42  49279  itsclc0xyqsolr  49352