Theorem 2z 9568

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 9364	. 2 |- 2 e. NN
2	1	nnzi 9561	1 |- 2 e. ZZ

Syntax hints:   e. wcel 2202   2c2 9253   ZZcz 9540

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 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8183  ax-resscn 8184  ax-1cn 8185  ax-1re 8186  ax-icn 8187  ax-addcl 8188  ax-addrcl 8189  ax-mulcl 8190  ax-addcom 8192  ax-addass 8194  ax-distr 8196  ax-i2m1 8197  ax-0lt1 8198  ax-0id 8200  ax-rnegex 8201  ax-cnre 8203  ax-pre-ltirr 8204  ax-pre-ltwlin 8205  ax-pre-lttrn 8206  ax-pre-ltadd 8208

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 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8275  df-mnf 8276  df-xr 8277  df-ltxr 8278  df-le 8279  df-sub 8411  df-neg 8412  df-inn 9203  df-2 9261  df-z 9541

This theorem is referenced by:  nn0n0n1ge2b  9620  nn0lt2  9622  nn0le2is012  9623  zadd2cl  9670  uzuzle23  9857  uzuzle24  9858  eluz4eluz2  9863  2eluzge1  9871  eluz2b1  9896  nn01to3  9912  nn0ge2m1nnALT  9913  ige2m1fz  10407  fz0to3un2pr  10420  fz0to4untppr  10421  fzctr  10430  fzo0to2pr  10526  fzo0to42pr  10528  qbtwnre  10579  2tnp1ge0ge0  10624  flhalf  10625  m1modge3gt1  10696  q2txmodxeq0  10709  sq1  10958  expnass  10970  sqrecapd  11002  sqoddm1div8  11018  bcn2m1  11094  bcn2p1  11095  4bc2eq6  11099  pfxtrcfv0  11341  pfxtrcfvl  11344  resqrexlemcalc1  11654  resqrexlemnmsq  11657  resqrexlemcvg  11659  resqrexlemglsq  11662  resqrexlemga  11663  resqrexlemsqa  11664  efgt0  12325  tanval3ap  12355  cos01bnd  12399  cos01gt0  12404  egt2lt3  12421  zeo3  12509  odd2np1  12514  even2n  12515  oddm1even  12516  oddp1even  12517  oexpneg  12518  2tp1odd  12525  2teven  12528  evend2  12530  oddp1d2  12531  ltoddhalfle  12534  opoe  12536  omoe  12537  opeo  12538  omeo  12539  m1expo  12541  m1exp1  12542  nn0o1gt2  12546  nn0o  12548  z0even  12552  n2dvds1  12553  z2even  12555  n2dvds3  12556  z4even  12557  4dvdseven  12558  flodddiv4  12577  bits0e  12590  bits0o  12591  bitsp1e  12593  bitsp1o  12594  bitsfzolem  12595  bitsfzo  12596  bitsmod  12597  bitscmp  12599  bitsinv1lem  12602  bitsinv1  12603  6gcd4e2  12646  3lcm2e6woprm  12738  isprm3  12770  prmind2  12772  dvdsnprmd  12777  prm2orodd  12778  2prm  12779  3prm  12780  prmdc  12782  oddprmge3  12787  isprm5  12794  divgcdodd  12795  pw2dvds  12818  sqrt2irraplemnn  12831  oddprm  12912  pythagtriplem2  12919  pythagtriplem4  12921  pythagtriplem11  12927  pythagtriplem13  12929  pythagtrip  12936  4sqlem19  13062  dec2dvds  13064  oddennn  13093  evenennn  13094  unennn  13098  exmidunben  13127  znidomb  14754  sincos6thpi  15653  rpcxpsqrtth  15741  2logb9irr  15782  2logb9irrALT  15785  sqrt2cxp2logb9e3  15786  2logb9irrap  15788  mersenne  15811  perfect1  15812  perfectlem1  15813  perfectlem2  15814  lgslem1  15819  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgsval2lem  15829  lgsdir2lem2  15848  lgsdir2  15852  lgsdirprm  15853  lgsne0  15857  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2dlem1cl  15878  gausslemma2dlem1f1o  15879  gausslemma2dlem2  15881  gausslemma2dlem3  15882  gausslemma2dlem4  15883  gausslemma2dlem5a  15884  gausslemma2dlem5  15885  gausslemma2dlem6  15886  gausslemma2dlem7  15887  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  lgsquad2lem2  15901  lgsquad2  15902  lgsquad3  15903  m1lgs  15904  2lgslem1a1  15905  2lgslem1a2  15906  2lgslem1b  15908  2lgslem3b1  15917  2lgslem3c1  15918  2lgs2  15921  2lgs  15923  2lgsoddprmlem2  15925  2lgsoddprmlem3  15930  2lgsoddprm  15932  usgrexmpldifpr  16190  upgr2wlkdc  16318  eupth2lem3lem3fi  16411  konigsbergvtx  16423  konigsbergiedg  16424  konigsbergumgr  16428  konigsberglem1  16429  konigsberglem5  16433  ex-fl  16439  ex-dvds  16444  cvgcmp2nlemabs  16764  trilpolemlt1  16773  apdifflemr  16779  apdiff  16780  qdiff  16781