Theorem 2z 9676

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 9470	. 2 |- 2 e. NN
2	1	nnzi 9669	1 |- 2 e. ZZ

This proof depends on syntax axioms:   e. wcel 2209   2c2 9357   ZZcz 9648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-addcom 8279  ax-addass 8281  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-0id 8287  ax-rnegex 8288  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-ltadd 8295

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8500  df-neg 8501  df-inn 9307  df-2 9365  df-z 9649

This theorem is used by:  nn0n0n1ge2b  9729  nn0lt2  9731  nn0le2is012  9732  zadd2cl  9779  uzuzle23  9971  uzuzle24  9972  eluz4eluz2  9977  2eluzge1  9985  eluz2b1  10010  nn01to3  10026  nn0ge2m1nnALT  10027  ige2m1fz  10527  fz0to3un2pr  10540  fz0to4untppr  10541  fzctr  10550  fzo0to2pr  10646  fzo0to42pr  10648  qbtwnre  10701  2tnp1ge0ge0  10749  flhalf  10750  m1modge3gt1  10821  q2txmodxeq0  10834  sq1  11083  expnass  11095  sqrecapd  11128  sqoddm1div8  11144  bcn2m1  11222  bcn2p1  11223  4bc2eq6  11227  pfxtrcfv0  11480  pfxtrcfvl  11483  resqrexlemcalc1  11794  resqrexlemnmsq  11797  resqrexlemcvg  11799  resqrexlemglsq  11802  resqrexlemga  11803  resqrexlemsqa  11804  efgt0  12467  tanval3ap  12497  cos01bnd  12541  cos01gt0  12546  egt2lt3  12563  zeo3  12651  odd2np1  12656  even2n  12657  oddm1even  12658  oddp1even  12659  oexpneg  12660  2tp1odd  12667  2teven  12670  evend2  12672  oddp1d2  12673  ltoddhalfle  12676  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1expo  12683  m1exp1  12684  nn0o1gt2  12688  nn0o  12690  z0even  12694  n2dvds1  12695  z2even  12697  n2dvds3  12698  z4even  12699  4dvdseven  12700  flodddiv4  12719  bits0e  12732  bits0o  12733  bitsp1e  12735  bitsp1o  12736  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  bitsinv1  12745  6gcd4e2  12788  3lcm2e6woprm  12880  isprm3  12912  prmind2  12914  dvdsnprmd  12919  prm2orodd  12920  2prm  12921  3prm  12922  prmdc  12924  oddprmge3  12930  isprm5  12937  divgcdodd  12938  oddpwdc  12970  sqrt2irraplemnn  12975  oddprm  13058  pythagtriplem2  13065  pythagtriplem4  13067  pythagtriplem11  13073  pythagtriplem13  13075  pythagtrip  13082  4sqlem19  13208  dec2dvds  13210  prmlem0  13240  prmlem1a  13241  ballotfilem2  13277  oddennn  13332  evenennn  13333  unennn  13337  exmidunben  13366  znidomb  15042  sincos6thpi  15993  rpcxpsqrtth  16085  2logb9irr  16126  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  ppiqsval  16156  ppiqfi  16158  ppiprm  16170  ppinprm  16171  ppidif  16175  ppi1  16176  ppiqnncl  16181  ppiqeq0  16182  ppiublem1  16192  ppiqub  16194  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem5  16213  lgslem1  16217  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsval2lem  16227  lgsdir2lem2  16246  lgsdir2  16250  lgsdirprm  16251  lgsne0  16255  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2dlem1cl  16276  gausslemma2dlem1f1o  16277  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  gausslemma2dlem5a  16282  gausslemma2dlem5  16283  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2lem2  16299  lgsquad2  16300  lgsquad3  16301  m1lgs  16302  2lgslem1a1  16303  2lgslem1a2  16304  2lgslem1b  16306  2lgslem3b1  16315  2lgslem3c1  16316  2lgs2  16319  2lgs  16321  2lgsoddprmlem2  16323  2lgsoddprmlem3  16328  2lgsoddprm  16330  usgrexmpldifpr  16588  upgr2wlkdc  16716  eupth2lem3lem3fi  16809  konigsbergvtx  16821  konigsbergiedg  16822  konigsbergumgr  16826  konigsberglem1  16827  konigsberglem5  16831  ex-fl  16837  ex-dvds  16842  cvgcmp2nlemabs  17179  trilpolemlt1  17188  apdifflemr  17194  apdiff  17195  qdiff  17196