Theorem 2z 9382

Description: Two is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
2z	⊢ 2 ∈ ℤ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 9180	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 9375	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2175  2c2 9069  ℤcz 9354

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1cn 8000  ax-1re 8001  ax-icn 8002  ax-addcl 8003  ax-addrcl 8004  ax-mulcl 8005  ax-addcom 8007  ax-addass 8009  ax-distr 8011  ax-i2m1 8012  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-cnre 8018  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-iota 5229  df-fun 5270  df-fv 5276  df-riota 5889  df-ov 5937  df-oprab 5938  df-mpo 5939  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-sub 8227  df-neg 8228  df-inn 9019  df-2 9077  df-z 9355

This theorem is referenced by:  nn0n0n1ge2b  9434  nn0lt2  9436  nn0le2is012  9437  zadd2cl  9484  eluz4eluz2  9670  uzuzle23  9674  2eluzge1  9679  eluz2b1  9704  nn01to3  9720  nn0ge2m1nnALT  9721  ige2m1fz  10214  fz0to3un2pr  10227  fz0to4untppr  10228  fzctr  10237  fzo0to2pr  10328  fzo0to42pr  10330  qbtwnre  10380  2tnp1ge0ge0  10425  flhalf  10426  m1modge3gt1  10497  q2txmodxeq0  10510  sq1  10759  expnass  10771  sqrecapd  10803  sqoddm1div8  10819  bcn2m1  10895  bcn2p1  10896  4bc2eq6  10900  resqrexlemcalc1  11244  resqrexlemnmsq  11247  resqrexlemcvg  11249  resqrexlemglsq  11252  resqrexlemga  11253  resqrexlemsqa  11254  efgt0  11914  tanval3ap  11944  cos01bnd  11988  cos01gt0  11993  egt2lt3  12010  zeo3  12098  odd2np1  12103  even2n  12104  oddm1even  12105  oddp1even  12106  oexpneg  12107  2tp1odd  12114  2teven  12117  evend2  12119  oddp1d2  12120  ltoddhalfle  12123  opoe  12125  omoe  12126  opeo  12127  omeo  12128  m1expo  12130  m1exp1  12131  nn0o1gt2  12135  nn0o  12137  z0even  12141  n2dvds1  12142  z2even  12144  n2dvds3  12145  z4even  12146  4dvdseven  12147  flodddiv4  12166  bits0e  12179  bits0o  12180  bitsp1e  12182  bitsp1o  12183  bitsfzolem  12184  bitsfzo  12185  bitsmod  12186  bitscmp  12188  bitsinv1lem  12191  bitsinv1  12192  6gcd4e2  12235  3lcm2e6woprm  12327  isprm3  12359  prmind2  12361  dvdsnprmd  12366  prm2orodd  12367  2prm  12368  3prm  12369  prmdc  12371  oddprmge3  12376  isprm5  12383  divgcdodd  12384  pw2dvds  12407  sqrt2irraplemnn  12420  oddprm  12501  pythagtriplem2  12508  pythagtriplem4  12510  pythagtriplem11  12516  pythagtriplem13  12518  pythagtrip  12525  4sqlem19  12651  dec2dvds  12653  oddennn  12682  evenennn  12683  unennn  12687  exmidunben  12716  znidomb  14338  sincos6thpi  15232  rpcxpsqrtth  15320  2logb9irr  15361  2logb9irrALT  15364  sqrt2cxp2logb9e3  15365  2logb9irrap  15367  mersenne  15387  perfect1  15388  perfectlem1  15389  perfectlem2  15390  lgslem1  15395  lgsval  15399  lgsfvalg  15400  lgsfcl2  15401  lgsval2lem  15405  lgsdir2lem2  15424  lgsdir2  15428  lgsdirprm  15429  lgsne0  15433  gausslemma2dlem0i  15452  gausslemma2dlem1a  15453  gausslemma2dlem1cl  15454  gausslemma2dlem1f1o  15455  gausslemma2dlem2  15457  gausslemma2dlem3  15458  gausslemma2dlem4  15459  gausslemma2dlem5a  15460  gausslemma2dlem5  15461  gausslemma2dlem6  15462  gausslemma2dlem7  15463  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlem1  15472  lgsquadlem2  15473  lgsquad2lem1  15476  lgsquad2lem2  15477  lgsquad2  15478  lgsquad3  15479  m1lgs  15480  2lgslem1a1  15481  2lgslem1a2  15482  2lgslem1b  15484  2lgslem3b1  15493  2lgslem3c1  15494  2lgs2  15497  2lgs  15499  2lgsoddprmlem2  15501  2lgsoddprmlem3  15506  2lgsoddprm  15508  ex-fl  15525  ex-dvds  15530  cvgcmp2nlemabs  15835  trilpolemlt1  15844  apdifflemr  15850  apdiff  15851