Theorem 2z 9348

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 9146	. 2 |- 2 e. NN
2	1	nnzi 9341	1 |- 2 e. ZZ

Syntax hints:   e. wcel 2164   2c2 9035   ZZcz 9320

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-2 9043  df-z 9321

This theorem is referenced by:  nn0n0n1ge2b  9399  nn0lt2  9401  nn0le2is012  9402  zadd2cl  9449  eluz4eluz2  9635  uzuzle23  9639  2eluzge1  9644  eluz2b1  9669  nn01to3  9685  nn0ge2m1nnALT  9686  ige2m1fz  10179  fz0to3un2pr  10192  fz0to4untppr  10193  fzctr  10202  fzo0to2pr  10288  fzo0to42pr  10290  qbtwnre  10328  2tnp1ge0ge0  10373  flhalf  10374  m1modge3gt1  10445  q2txmodxeq0  10458  sq1  10707  expnass  10719  sqrecapd  10751  sqoddm1div8  10767  bcn2m1  10843  bcn2p1  10844  4bc2eq6  10848  resqrexlemcalc1  11161  resqrexlemnmsq  11164  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  resqrexlemsqa  11171  efgt0  11830  tanval3ap  11860  cos01bnd  11904  cos01gt0  11909  egt2lt3  11926  zeo3  12012  odd2np1  12017  even2n  12018  oddm1even  12019  oddp1even  12020  oexpneg  12021  2tp1odd  12028  2teven  12031  evend2  12033  oddp1d2  12034  ltoddhalfle  12037  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1expo  12044  m1exp1  12045  nn0o1gt2  12049  nn0o  12051  z0even  12055  n2dvds1  12056  z2even  12058  n2dvds3  12059  z4even  12060  4dvdseven  12061  flodddiv4  12078  6gcd4e2  12135  3lcm2e6woprm  12227  isprm3  12259  prmind2  12261  dvdsnprmd  12266  prm2orodd  12267  2prm  12268  3prm  12269  prmdc  12271  oddprmge3  12276  isprm5  12283  divgcdodd  12284  pw2dvds  12307  sqrt2irraplemnn  12320  oddprm  12400  pythagtriplem2  12407  pythagtriplem4  12409  pythagtriplem11  12415  pythagtriplem13  12417  pythagtrip  12424  4sqlem19  12550  oddennn  12552  evenennn  12553  unennn  12557  exmidunben  12586  znidomb  14157  sincos6thpi  15018  rpcxpsqrtth  15105  2logb9irr  15144  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  2logb9irrap  15150  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgsdir2lem2  15186  lgsdir2  15190  lgsdirprm  15191  lgsne0  15195  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem1cl  15216  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  gausslemma2dlem5  15223  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad2  15240  lgsquad3  15241  m1lgs  15242  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1b  15246  2lgslem3b1  15255  2lgslem3c1  15256  2lgs2  15259  2lgs  15261  2lgsoddprmlem2  15263  2lgsoddprmlem3  15268  2lgsoddprm  15270  ex-fl  15287  ex-dvds  15292  cvgcmp2nlemabs  15592  trilpolemlt1  15601  apdifflemr  15607  apdiff  15608