Theorem 2z 12432

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

Syntax hints:   ∈ wcel 2105  2c2 12108  ℤcz 12399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-i2m1 11019  ax-1ne0 11020  ax-rrecex 11023  ax-cnre 11024

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-ov 7320  df-om 7760  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-neg 11288  df-nn 12054  df-2 12116  df-z 12400

This theorem is referenced by:  nn0lt2  12463  nn0le2is012  12464  zadd2cl  12514  eluz4eluz2  12705  uzuzle23  12709  2eluzge1  12714  eluz2b1  12739  nn01to3  12761  nn0ge2m1nnALT  12762  ige2m1fz  13426  fz0to3un2pr  13438  fz0to4untppr  13439  fzctr  13448  fzo0to2pr  13552  fzo0to42pr  13554  2tnp1ge0ge0  13629  flhalf  13630  m1modge3gt1  13718  2txmodxeq0  13731  f13idfv  13800  sqrecd  13948  znsqcld  13960  sq1  13992  expnass  14004  sqoddm1div8  14038  bcn2m1  14118  bcn2p1  14119  4bc2eq6  14123  hashtpg  14278  ccat2s1p2  14416  ccat2s1p2OLD  14418  pfxtrcfv0  14486  pfxtrcfvl  14489  eqwrds3  14755  iseraltlem2  15473  iseraltlem3  15474  climcndslem1  15640  climcnds  15642  bpolydiflem  15843  efgt0  15891  tanval3  15922  cos01bnd  15974  cos01gt0  15979  odd2np1  16129  even2n  16130  oddm1even  16131  oddp1even  16132  oexpneg  16133  mod2eq1n2dvds  16135  2tp1odd  16140  2teven  16143  evend2  16145  oddp1d2  16146  ltoddhalfle  16149  opoe  16151  omoe  16152  opeo  16153  omeo  16154  z0even  16155  z2even  16158  z4even  16160  4dvdseven  16161  m1expo  16163  m1exp1  16164  nn0o  16171  sumeven  16175  flodddiv4  16201  bits0e  16215  bits0o  16216  bitsp1e  16218  bitsp1o  16219  bitsfzo  16221  bitsmod  16222  bitscmp  16224  bitsinv1lem  16227  bitsinv1  16228  6gcd4e2  16325  3lcm2e6woprm  16397  lcmf2a3a4e12  16429  isprm3  16465  dvdsnprmd  16472  2prm  16474  2mulprm  16475  oddprmge3  16482  ge2nprmge4  16483  isprm7  16490  divgcdodd  16492  oddprm  16588  pythagtriplem4  16597  pythagtriplem11  16603  pythagtriplem13  16605  iserodd  16613  prmgaplem3  16831  prmgaplem7  16835  dec2dvds  16841  prmlem0  16884  4001lem1  16919  psgnunilem4  19181  efgredleme  19424  lt6abl  19571  ablsimpgfindlem1  19785  ablsimpgfindlem2  19786  zringndrg  20773  znidomb  20852  chfacfscmulfsupp  22091  chfacfpmmulfsupp  22095  minveclem2  24673  minveclem3  24676  pjthlem1  24684  dyaddisjlem  24842  mbfi1fseqlem5  24967  dvrecg  25220  dvexp3  25225  aaliou3lem6  25591  tanregt0  25778  efif1olem4  25784  tanarg  25857  cxpsqrtth  25967  2irrexpq  25968  2logb9irr  26028  2logb9irrALT  26031  sqrt2cxp2logb9e3  26032  cubic2  26081  asinlem3  26104  atantayl2  26171  cxp2limlem  26208  lgamgulmlem3  26263  lgamgulmlem4  26264  basellem2  26314  basellem3  26315  basellem4  26316  basellem5  26317  basellem8  26320  basellem9  26321  ppisval  26336  ppiprm  26383  ppinprm  26384  chtprm  26385  chtnprm  26386  chtdif  26390  ppidif  26395  ppi1  26396  cht1  26397  cht3  26405  ppieq0  26408  ppiublem1  26433  chpeq0  26439  chtub  26443  chpval2  26449  chpub  26451  mersenne  26458  perfect1  26459  perfectlem1  26460  perfectlem2  26461  bposlem1  26515  bposlem2  26516  bposlem3  26517  bposlem5  26519  bposlem6  26520  lgslem1  26528  lgsdir2lem2  26557  lgsdir2  26561  lgsqr  26582  gausslemma2dlem0i  26595  gausslemma2dlem1a  26596  gausslemma2dlem5a  26601  gausslemma2dlem5  26602  gausslemma2dlem6  26603  gausslemma2dlem7  26604  gausslemma2d  26605  lgseisenlem1  26606  lgseisenlem2  26607  lgseisenlem3  26608  lgseisenlem4  26609  lgsquadlem1  26611  lgsquadlem2  26612  lgsquad2lem1  26615  lgsquad2lem2  26616  lgsquad2  26617  lgsquad3  26618  m1lgs  26619  2lgslem1a1  26620  2lgslem1a2  26621  2lgslem1b  26623  2lgslem3b1  26632  2lgslem3c1  26633  2lgs2  26636  2lgs  26638  2lgsoddprmlem2  26640  2lgsoddprmlem3  26645  2lgsoddprm  26647  2sqblem  26662  2sqmod  26667  chebbnd1lem1  26700  chebbnd1lem3  26702  chebbnd1  26703  dchrisum0lem1a  26717  dchrvmasumiflem1  26732  dchrisum0flblem1  26739  dchrisum0flblem2  26740  dchrisum0lem1b  26746  dchrisum0lem1  26747  dchrisum0lem2a  26748  dchrisum0lem2  26749  dchrisum0lem3  26750  mulog2sumlem2  26766  pntlemd  26825  pntlema  26827  pntlemb  26828  pntlemh  26830  pntlemr  26833  pntlemf  26836  pntlemo  26838  istrkg2ld  26957  istrkg3ld  26958  axlowdimlem3  27448  axlowdimlem6  27451  axlowdimlem16  27461  axlowdimlem17  27462  axlowdim  27465  usgrexmpldifpr  27761  usgrexmplef  27762  cusgrsizeindb1  27953  pthdlem1  28270  clwlkclwwlklem2a1  28492  clwlkclwwlklem2fv1  28495  clwlkclwwlklem2fv2  28496  clwlkclwwlklem2a4  28497  clwlkclwwlklem2a  28498  clwwisshclwwslem  28514  eupth2lem3lem3  28730  konigsberglem5  28756  2clwwlk2  28848  numclwwlk2lem1  28876  numclwlk2lem2f  28877  frgrreggt1  28893  ex-fl  28947  ex-mod  28949  ex-hash  28953  ex-dvds  28956  ex-ind-dvds  28961  minvecolem3  29374  pjhthlem1  29889  wrdt2ind  31360  archirngz  31578  archiabllem2c  31584  lmat22det  31912  dya2ub  32377  dya2icoseg  32384  oddpwdc  32461  eulerpartlemd  32473  eulerpartlemt  32478  ballotlem2  32595  signslema  32681  prodfzo03  32723  hgt750leme  32778  tgoldbachgtde  32780  nn0prpwlem  34585  knoppndvlem2  34767  knoppndvlem8  34773  irrdifflemf  35568  poimirlem25  35874  poimirlem26  35875  poimirlem27  35876  poimirlem28  35877  logblebd  40205  lcm2un  40243  lcm3un  40244  lcmineqlem18  40275  lcmineqlem19  40276  lcmineqlem21  40278  lcmineqlem22  40279  3lexlogpow5ineq2  40284  3lexlogpow2ineq1  40287  aks4d1p1p3  40298  aks4d1p1p4  40300  aks4d1p1p6  40302  aks4d1p1p7  40303  aks4d1p1p5  40304  aks4d1p1  40305  aks4d1p3  40307  aks4d1p6  40310  aks4d1p7d1  40311  aks4d1p7  40312  aks4d1p8  40316  aks4d1p9  40317  5bc2eq10  40322  2np3bcnp1  40324  2ap1caineq  40325  flt4lem2  40700  flt4lem5  40703  flt4lem7  40712  nna4b4nsq  40713  acongrep  41019  acongeq  41022  jm2.18  41027  jm2.22  41034  jm2.23  41035  jm2.20nn  41036  jm2.26a  41039  jm2.26  41041  jm2.15nn0  41042  jm2.27a  41044  jm2.27c  41046  rmydioph  41053  jm3.1lem1  41056  jm3.1lem3  41058  expdiophlem1  41060  expdiophlem2  41061  hashnzfz2  42173  sumnnodd  43421  coskpi2  43657  cosknegpi  43660  dvdivbd  43714  stoweidlem26  43817  wallispilem4  43859  wallispi2lem1  43862  wallispi2lem2  43863  wallispi2  43864  stirlinglem1  43865  stirlinglem3  43867  stirlinglem7  43871  stirlinglem8  43872  stirlinglem10  43874  stirlinglem11  43875  stirlinglem15  43879  dirkertrigeqlem1  43889  dirkercncflem2  43895  fourierdlem54  43951  fourierdlem56  43953  fourierdlem57  43954  fourierdlem102  43999  fourierdlem114  44011  fourierswlem  44021  fouriersw  44022  smfmullem4  44583  fmtnorec1  45254  goldbachthlem2  45263  odz2prm2pw  45280  fmtnoprmfac1  45282  fmtnoprmfac2lem1  45283  fmtnoprmfac2  45284  fmtno4prmfac  45289  31prm  45314  sfprmdvdsmersenne  45320  lighneallem1  45322  lighneallem4a  45325  lighneallem4b  45326  lighneallem4  45327  proththdlem  45330  proththd  45331  3exp4mod41  45333  41prothprmlem2  45335  m1expevenALTV  45364  dfeven2  45366  m2even  45371  gcd2odd1  45385  oexpnegALTV  45394  oexpnegnz  45395  2evenALTV  45409  2noddALTV  45410  nn0o1gt2ALTV  45411  nnpw2evenALTV  45419  perfectALTVlem1  45438  perfectALTVlem2  45439  fppr2odd  45448  341fppr2  45451  9fppr8  45454  nfermltl2rev  45460  sbgoldbalt  45498  mogoldbb  45502  nnsum4primesodd  45513  nnsum4primesoddALTV  45514  wtgoldbnnsum4prm  45519  bgoldbnnsum3prm  45521  2even  45756  zlmodzxzequa  46102  zlmodzxznm  46103  zlmodzxzequap  46105  zlmodzxzldeplem1  46106  zlmodzxzldeplem3  46108  zlmodzxzldep  46110  ldepsnlinclem1  46111  ldepsnlinc  46114  pw2m1lepw2m1  46126  fldivexpfllog2  46176  nnlog2ge0lt1  46177  logbpw2m1  46178  fllog2  46179  blennnelnn  46187  blenpw2  46189  nnpw2blenfzo  46192  blennnt2  46200  nnolog2flm1  46201  dig2nn0ld  46215  dig2nn1st  46216  0dig2pr01  46221  0dig2nn0o  46224  ackval42  46307  itsclc0xyqsolr  46380