Theorem 2z 9485

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 9283	. 2 |- 2 e. NN
2	1	nnzi 9478	1 |- 2 e. ZZ

Syntax hints:   e. wcel 2200   2c2 9172   ZZcz 9457

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8101  ax-resscn 8102  ax-1cn 8103  ax-1re 8104  ax-icn 8105  ax-addcl 8106  ax-addrcl 8107  ax-mulcl 8108  ax-addcom 8110  ax-addass 8112  ax-distr 8114  ax-i2m1 8115  ax-0lt1 8116  ax-0id 8118  ax-rnegex 8119  ax-cnre 8121  ax-pre-ltirr 8122  ax-pre-ltwlin 8123  ax-pre-lttrn 8124  ax-pre-ltadd 8126

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198  df-sub 8330  df-neg 8331  df-inn 9122  df-2 9180  df-z 9458

This theorem is referenced by:  nn0n0n1ge2b  9537  nn0lt2  9539  nn0le2is012  9540  zadd2cl  9587  eluz4eluz2  9774  uzuzle23  9778  2eluzge1  9783  eluz2b1  9808  nn01to3  9824  nn0ge2m1nnALT  9825  ige2m1fz  10318  fz0to3un2pr  10331  fz0to4untppr  10332  fzctr  10341  fzo0to2pr  10436  fzo0to42pr  10438  qbtwnre  10488  2tnp1ge0ge0  10533  flhalf  10534  m1modge3gt1  10605  q2txmodxeq0  10618  sq1  10867  expnass  10879  sqrecapd  10911  sqoddm1div8  10927  bcn2m1  11003  bcn2p1  11004  4bc2eq6  11008  pfxtrcfv0  11242  pfxtrcfvl  11245  resqrexlemcalc1  11541  resqrexlemnmsq  11544  resqrexlemcvg  11546  resqrexlemglsq  11549  resqrexlemga  11550  resqrexlemsqa  11551  efgt0  12211  tanval3ap  12241  cos01bnd  12285  cos01gt0  12290  egt2lt3  12307  zeo3  12395  odd2np1  12400  even2n  12401  oddm1even  12402  oddp1even  12403  oexpneg  12404  2tp1odd  12411  2teven  12414  evend2  12416  oddp1d2  12417  ltoddhalfle  12420  opoe  12422  omoe  12423  opeo  12424  omeo  12425  m1expo  12427  m1exp1  12428  nn0o1gt2  12432  nn0o  12434  z0even  12438  n2dvds1  12439  z2even  12441  n2dvds3  12442  z4even  12443  4dvdseven  12444  flodddiv4  12463  bits0e  12476  bits0o  12477  bitsp1e  12479  bitsp1o  12480  bitsfzolem  12481  bitsfzo  12482  bitsmod  12483  bitscmp  12485  bitsinv1lem  12488  bitsinv1  12489  6gcd4e2  12532  3lcm2e6woprm  12624  isprm3  12656  prmind2  12658  dvdsnprmd  12663  prm2orodd  12664  2prm  12665  3prm  12666  prmdc  12668  oddprmge3  12673  isprm5  12680  divgcdodd  12681  pw2dvds  12704  sqrt2irraplemnn  12717  oddprm  12798  pythagtriplem2  12805  pythagtriplem4  12807  pythagtriplem11  12813  pythagtriplem13  12815  pythagtrip  12822  4sqlem19  12948  dec2dvds  12950  oddennn  12979  evenennn  12980  unennn  12984  exmidunben  13013  znidomb  14638  sincos6thpi  15532  rpcxpsqrtth  15620  2logb9irr  15661  2logb9irrALT  15664  sqrt2cxp2logb9e3  15665  2logb9irrap  15667  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  lgslem1  15695  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgsval2lem  15705  lgsdir2lem2  15724  lgsdir2  15728  lgsdirprm  15729  lgsne0  15733  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem1cl  15754  gausslemma2dlem1f1o  15755  gausslemma2dlem2  15757  gausslemma2dlem3  15758  gausslemma2dlem4  15759  gausslemma2dlem5a  15760  gausslemma2dlem5  15761  gausslemma2dlem6  15762  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  lgsquad2lem2  15777  lgsquad2  15778  lgsquad3  15779  m1lgs  15780  2lgslem1a1  15781  2lgslem1a2  15782  2lgslem1b  15784  2lgslem3b1  15793  2lgslem3c1  15794  2lgs2  15797  2lgs  15799  2lgsoddprmlem2  15801  2lgsoddprmlem3  15806  2lgsoddprm  15808  upgr2wlkdc  16121  ex-fl  16172  ex-dvds  16177  cvgcmp2nlemabs  16488  trilpolemlt1  16497  apdifflemr  16503  apdiff  16504