Theorem 2z 9509

Description: Two is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
2z	⊢ 2 ∈ ℤ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 9307	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 9502	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2201  2c2 9196  ℤcz 9481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-pow 4263  ax-pr 4298  ax-un 4529  ax-setind 4634  ax-cnex 8125  ax-resscn 8126  ax-1cn 8127  ax-1re 8128  ax-icn 8129  ax-addcl 8130  ax-addrcl 8131  ax-mulcl 8132  ax-addcom 8134  ax-addass 8136  ax-distr 8138  ax-i2m1 8139  ax-0lt1 8140  ax-0id 8142  ax-rnegex 8143  ax-cnre 8145  ax-pre-ltirr 8146  ax-pre-ltwlin 8147  ax-pre-lttrn 8148  ax-pre-ltadd 8150

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3653  df-sn 3674  df-pr 3675  df-op 3677  df-uni 3893  df-int 3928  df-br 4088  df-opab 4150  df-id 4389  df-xp 4730  df-rel 4731  df-cnv 4732  df-co 4733  df-dm 4734  df-iota 5285  df-fun 5327  df-fv 5333  df-riota 5973  df-ov 6023  df-oprab 6024  df-mpo 6025  df-pnf 8218  df-mnf 8219  df-xr 8220  df-ltxr 8221  df-le 8222  df-sub 8354  df-neg 8355  df-inn 9146  df-2 9204  df-z 9482

This theorem is referenced by:  nn0n0n1ge2b  9561  nn0lt2  9563  nn0le2is012  9564  zadd2cl  9611  uzuzle23  9798  uzuzle24  9799  eluz4eluz2  9804  2eluzge1  9812  eluz2b1  9837  nn01to3  9853  nn0ge2m1nnALT  9854  ige2m1fz  10347  fz0to3un2pr  10360  fz0to4untppr  10361  fzctr  10370  fzo0to2pr  10466  fzo0to42pr  10468  qbtwnre  10519  2tnp1ge0ge0  10564  flhalf  10565  m1modge3gt1  10636  q2txmodxeq0  10649  sq1  10898  expnass  10910  sqrecapd  10942  sqoddm1div8  10958  bcn2m1  11034  bcn2p1  11035  4bc2eq6  11039  pfxtrcfv0  11281  pfxtrcfvl  11284  resqrexlemcalc1  11594  resqrexlemnmsq  11597  resqrexlemcvg  11599  resqrexlemglsq  11602  resqrexlemga  11603  resqrexlemsqa  11604  efgt0  12265  tanval3ap  12295  cos01bnd  12339  cos01gt0  12344  egt2lt3  12361  zeo3  12449  odd2np1  12454  even2n  12455  oddm1even  12456  oddp1even  12457  oexpneg  12458  2tp1odd  12465  2teven  12468  evend2  12470  oddp1d2  12471  ltoddhalfle  12474  opoe  12476  omoe  12477  opeo  12478  omeo  12479  m1expo  12481  m1exp1  12482  nn0o1gt2  12486  nn0o  12488  z0even  12492  n2dvds1  12493  z2even  12495  n2dvds3  12496  z4even  12497  4dvdseven  12498  flodddiv4  12517  bits0e  12530  bits0o  12531  bitsp1e  12533  bitsp1o  12534  bitsfzolem  12535  bitsfzo  12536  bitsmod  12537  bitscmp  12539  bitsinv1lem  12542  bitsinv1  12543  6gcd4e2  12586  3lcm2e6woprm  12678  isprm3  12710  prmind2  12712  dvdsnprmd  12717  prm2orodd  12718  2prm  12719  3prm  12720  prmdc  12722  oddprmge3  12727  isprm5  12734  divgcdodd  12735  pw2dvds  12758  sqrt2irraplemnn  12771  oddprm  12852  pythagtriplem2  12859  pythagtriplem4  12861  pythagtriplem11  12867  pythagtriplem13  12869  pythagtrip  12876  4sqlem19  13002  dec2dvds  13004  oddennn  13033  evenennn  13034  unennn  13038  exmidunben  13067  znidomb  14693  sincos6thpi  15592  rpcxpsqrtth  15680  2logb9irr  15721  2logb9irrALT  15724  sqrt2cxp2logb9e3  15725  2logb9irrap  15727  mersenne  15747  perfect1  15748  perfectlem1  15749  perfectlem2  15750  lgslem1  15755  lgsval  15759  lgsfvalg  15760  lgsfcl2  15761  lgsval2lem  15765  lgsdir2lem2  15784  lgsdir2  15788  lgsdirprm  15789  lgsne0  15793  gausslemma2dlem0i  15812  gausslemma2dlem1a  15813  gausslemma2dlem1cl  15814  gausslemma2dlem1f1o  15815  gausslemma2dlem2  15817  gausslemma2dlem3  15818  gausslemma2dlem4  15819  gausslemma2dlem5a  15820  gausslemma2dlem5  15821  gausslemma2dlem6  15822  gausslemma2dlem7  15823  gausslemma2d  15824  lgseisenlem1  15825  lgseisenlem2  15826  lgseisenlem3  15827  lgseisenlem4  15828  lgseisen  15829  lgsquadlem1  15832  lgsquadlem2  15833  lgsquad2lem1  15836  lgsquad2lem2  15837  lgsquad2  15838  lgsquad3  15839  m1lgs  15840  2lgslem1a1  15841  2lgslem1a2  15842  2lgslem1b  15844  2lgslem3b1  15853  2lgslem3c1  15854  2lgs2  15857  2lgs  15859  2lgsoddprmlem2  15861  2lgsoddprmlem3  15866  2lgsoddprm  15868  usgrexmpldifpr  16126  upgr2wlkdc  16254  eupth2lem3lem3fi  16347  konigsbergvtx  16359  konigsbergiedg  16360  konigsbergumgr  16364  konigsberglem1  16365  konigsberglem5  16369  ex-fl  16375  ex-dvds  16380  cvgcmp2nlemabs  16698  trilpolemlt1  16707  apdifflemr  16713  apdiff  16714  qdiff  16715