Theorem 2z 9240

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

Assertion

Ref	Expression
2z	|- 2 e. ZZ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 9039	. 2 |- 2 e. NN
2	1	nnzi 9233	1 |- 2 e. ZZ

Syntax hints:   e. wcel 2141   2c2 8929   ZZcz 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-ltadd 7890

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-iota 5160  df-fun 5200  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-inn 8879  df-2 8937  df-z 9213

This theorem is referenced by:  nn0n0n1ge2b  9291  nn0lt2  9293  nn0le2is012  9294  zadd2cl  9341  eluz4eluz2  9526  uzuzle23  9530  2eluzge1  9535  eluz2b1  9560  nn01to3  9576  nn0ge2m1nnALT  9577  ige2m1fz  10066  fz0to3un2pr  10079  fz0to4untppr  10080  fzctr  10089  fzo0to2pr  10174  fzo0to42pr  10176  qbtwnre  10213  2tnp1ge0ge0  10257  flhalf  10258  m1modge3gt1  10327  q2txmodxeq0  10340  sq1  10569  expnass  10581  sqrecapd  10613  sqoddm1div8  10629  bcn2m1  10703  bcn2p1  10704  4bc2eq6  10708  resqrexlemcalc1  10978  resqrexlemnmsq  10981  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  resqrexlemsqa  10988  efgt0  11647  tanval3ap  11677  cos01bnd  11721  cos01gt0  11725  egt2lt3  11742  zeo3  11827  odd2np1  11832  even2n  11833  oddm1even  11834  oddp1even  11835  oexpneg  11836  2tp1odd  11843  2teven  11846  evend2  11848  oddp1d2  11849  ltoddhalfle  11852  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1expo  11859  m1exp1  11860  nn0o1gt2  11864  nn0o  11866  z0even  11870  n2dvds1  11871  z2even  11873  n2dvds3  11874  z4even  11875  4dvdseven  11876  flodddiv4  11893  6gcd4e2  11950  3lcm2e6woprm  12040  isprm3  12072  prmind2  12074  dvdsnprmd  12079  prm2orodd  12080  2prm  12081  3prm  12082  prmdc  12084  oddprmge3  12089  isprm5  12096  divgcdodd  12097  pw2dvds  12120  sqrt2irraplemnn  12133  oddprm  12213  pythagtriplem2  12220  pythagtriplem4  12222  pythagtriplem11  12228  pythagtriplem13  12230  pythagtrip  12237  oddennn  12347  evenennn  12348  unennn  12352  exmidunben  12381  sincos6thpi  13557  rpcxpsqrtth  13644  2logb9irr  13683  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  2logb9irrap  13689  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgsdir2lem2  13724  lgsdir2  13728  lgsdirprm  13729  lgsne0  13733  ex-fl  13760  ex-dvds  13765  cvgcmp2nlemabs  14064  trilpolemlt1  14073  apdifflemr  14079  apdiff  14080