Theorem 2z 9284

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 9083	. 2 |- 2 e. NN
2	1	nnzi 9277	1 |- 2 e. ZZ

Syntax hints:   e. wcel 2148   2c2 8973   ZZcz 9256

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-addcom 7914  ax-addass 7916  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-0id 7922  ax-rnegex 7923  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-ltadd 7930

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-inn 8923  df-2 8981  df-z 9257

This theorem is referenced by:  nn0n0n1ge2b  9335  nn0lt2  9337  nn0le2is012  9338  zadd2cl  9385  eluz4eluz2  9570  uzuzle23  9574  2eluzge1  9579  eluz2b1  9604  nn01to3  9620  nn0ge2m1nnALT  9621  ige2m1fz  10113  fz0to3un2pr  10126  fz0to4untppr  10127  fzctr  10136  fzo0to2pr  10221  fzo0to42pr  10223  qbtwnre  10260  2tnp1ge0ge0  10304  flhalf  10305  m1modge3gt1  10374  q2txmodxeq0  10387  sq1  10617  expnass  10629  sqrecapd  10661  sqoddm1div8  10677  bcn2m1  10752  bcn2p1  10753  4bc2eq6  10757  resqrexlemcalc1  11026  resqrexlemnmsq  11029  resqrexlemcvg  11031  resqrexlemglsq  11034  resqrexlemga  11035  resqrexlemsqa  11036  efgt0  11695  tanval3ap  11725  cos01bnd  11769  cos01gt0  11773  egt2lt3  11790  zeo3  11876  odd2np1  11881  even2n  11882  oddm1even  11883  oddp1even  11884  oexpneg  11885  2tp1odd  11892  2teven  11895  evend2  11897  oddp1d2  11898  ltoddhalfle  11901  opoe  11903  omoe  11904  opeo  11905  omeo  11906  m1expo  11908  m1exp1  11909  nn0o1gt2  11913  nn0o  11915  z0even  11919  n2dvds1  11920  z2even  11922  n2dvds3  11923  z4even  11924  4dvdseven  11925  flodddiv4  11942  6gcd4e2  11999  3lcm2e6woprm  12089  isprm3  12121  prmind2  12123  dvdsnprmd  12128  prm2orodd  12129  2prm  12130  3prm  12131  prmdc  12133  oddprmge3  12138  isprm5  12145  divgcdodd  12146  pw2dvds  12169  sqrt2irraplemnn  12182  oddprm  12262  pythagtriplem2  12269  pythagtriplem4  12271  pythagtriplem11  12277  pythagtriplem13  12279  pythagtrip  12286  oddennn  12396  evenennn  12397  unennn  12401  exmidunben  12430  sincos6thpi  14403  rpcxpsqrtth  14490  2logb9irr  14529  2logb9irrALT  14532  sqrt2cxp2logb9e3  14533  2logb9irrap  14535  lgslem1  14541  lgsval  14545  lgsfvalg  14546  lgsfcl2  14547  lgsval2lem  14551  lgsdir2lem2  14570  lgsdir2  14574  lgsdirprm  14575  lgsne0  14579  lgseisenlem1  14590  lgseisenlem2  14591  m1lgs  14592  2lgsoddprmlem2  14594  2lgsoddprmlem3  14599  ex-fl  14617  ex-dvds  14622  cvgcmp2nlemabs  14920  trilpolemlt1  14929  apdifflemr  14935  apdiff  14936