Theorem 2z 9605

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

Syntax hints:   ∈ wcel 2203  2c2 9288  ℤcz 9577

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-2 9296  df-z 9578

This theorem is referenced by:  nn0n0n1ge2b  9657  nn0lt2  9659  nn0le2is012  9660  zadd2cl  9707  uzuzle23  9894  uzuzle24  9895  eluz4eluz2  9900  2eluzge1  9908  eluz2b1  9933  nn01to3  9949  nn0ge2m1nnALT  9950  ige2m1fz  10444  fz0to3un2pr  10457  fz0to4untppr  10458  fzctr  10467  fzo0to2pr  10563  fzo0to42pr  10565  qbtwnre  10616  2tnp1ge0ge0  10661  flhalf  10662  m1modge3gt1  10733  q2txmodxeq0  10746  sq1  10995  expnass  11007  sqrecapd  11039  sqoddm1div8  11055  bcn2m1  11132  bcn2p1  11133  4bc2eq6  11137  pfxtrcfv0  11386  pfxtrcfvl  11389  resqrexlemcalc1  11699  resqrexlemnmsq  11702  resqrexlemcvg  11704  resqrexlemglsq  11707  resqrexlemga  11708  resqrexlemsqa  11709  efgt0  12370  tanval3ap  12400  cos01bnd  12444  cos01gt0  12449  egt2lt3  12466  zeo3  12554  odd2np1  12559  even2n  12560  oddm1even  12561  oddp1even  12562  oexpneg  12563  2tp1odd  12570  2teven  12573  evend2  12575  oddp1d2  12576  ltoddhalfle  12579  opoe  12581  omoe  12582  opeo  12583  omeo  12584  m1expo  12586  m1exp1  12587  nn0o1gt2  12591  nn0o  12593  z0even  12597  n2dvds1  12598  z2even  12600  n2dvds3  12601  z4even  12602  4dvdseven  12603  flodddiv4  12622  bits0e  12635  bits0o  12636  bitsp1e  12638  bitsp1o  12639  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitscmp  12644  bitsinv1lem  12647  bitsinv1  12648  6gcd4e2  12691  3lcm2e6woprm  12783  isprm3  12815  prmind2  12817  dvdsnprmd  12822  prm2orodd  12823  2prm  12824  3prm  12825  prmdc  12827  oddprmge3  12832  isprm5  12839  divgcdodd  12840  pw2dvds  12863  sqrt2irraplemnn  12876  oddprm  12957  pythagtriplem2  12964  pythagtriplem4  12966  pythagtriplem11  12972  pythagtriplem13  12974  pythagtrip  12981  4sqlem19  13107  dec2dvds  13109  ballotfilem2  13142  oddennn  13143  evenennn  13144  unennn  13148  exmidunben  13177  znidomb  14806  sincos6thpi  15707  rpcxpsqrtth  15795  2logb9irr  15836  2logb9irrALT  15839  sqrt2cxp2logb9e3  15840  2logb9irrap  15842  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsval2lem  15883  lgsdir2lem2  15902  lgsdir2  15906  lgsdirprm  15907  lgsne0  15911  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  gausslemma2dlem1cl  15932  gausslemma2dlem1f1o  15933  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  lgsquad2lem2  15955  lgsquad2  15956  lgsquad3  15957  m1lgs  15958  2lgslem1a1  15959  2lgslem1a2  15960  2lgslem1b  15962  2lgslem3b1  15971  2lgslem3c1  15972  2lgs2  15975  2lgs  15977  2lgsoddprmlem2  15979  2lgsoddprmlem3  15984  2lgsoddprm  15986  usgrexmpldifpr  16244  upgr2wlkdc  16372  eupth2lem3lem3fi  16465  konigsbergvtx  16477  konigsbergiedg  16478  konigsbergumgr  16482  konigsberglem1  16483  konigsberglem5  16487  ex-fl  16493  ex-dvds  16498  cvgcmp2nlemabs  16816  trilpolemlt1  16825  apdifflemr  16831  apdiff  16832  qdiff  16833