Theorem 2z 9507

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 9305	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 9500	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2202  2c2 9194  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-2 9202  df-z 9480

This theorem is referenced by:  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  zadd2cl  9609  uzuzle23  9796  uzuzle24  9797  eluz4eluz2  9802  2eluzge1  9810  eluz2b1  9835  nn01to3  9851  nn0ge2m1nnALT  9852  ige2m1fz  10345  fz0to3un2pr  10358  fz0to4untppr  10359  fzctr  10368  fzo0to2pr  10464  fzo0to42pr  10466  qbtwnre  10517  2tnp1ge0ge0  10562  flhalf  10563  m1modge3gt1  10634  q2txmodxeq0  10647  sq1  10896  expnass  10908  sqrecapd  10940  sqoddm1div8  10956  bcn2m1  11032  bcn2p1  11033  4bc2eq6  11037  pfxtrcfv0  11279  pfxtrcfvl  11282  resqrexlemcalc1  11579  resqrexlemnmsq  11582  resqrexlemcvg  11584  resqrexlemglsq  11587  resqrexlemga  11588  resqrexlemsqa  11589  efgt0  12250  tanval3ap  12280  cos01bnd  12324  cos01gt0  12329  egt2lt3  12346  zeo3  12434  odd2np1  12439  even2n  12440  oddm1even  12441  oddp1even  12442  oexpneg  12443  2tp1odd  12450  2teven  12453  evend2  12455  oddp1d2  12456  ltoddhalfle  12459  opoe  12461  omoe  12462  opeo  12463  omeo  12464  m1expo  12466  m1exp1  12467  nn0o1gt2  12471  nn0o  12473  z0even  12477  n2dvds1  12478  z2even  12480  n2dvds3  12481  z4even  12482  4dvdseven  12483  flodddiv4  12502  bits0e  12515  bits0o  12516  bitsp1e  12518  bitsp1o  12519  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitscmp  12524  bitsinv1lem  12527  bitsinv1  12528  6gcd4e2  12571  3lcm2e6woprm  12663  isprm3  12695  prmind2  12697  dvdsnprmd  12702  prm2orodd  12703  2prm  12704  3prm  12705  prmdc  12707  oddprmge3  12712  isprm5  12719  divgcdodd  12720  pw2dvds  12743  sqrt2irraplemnn  12756  oddprm  12837  pythagtriplem2  12844  pythagtriplem4  12846  pythagtriplem11  12852  pythagtriplem13  12854  pythagtrip  12861  4sqlem19  12987  dec2dvds  12989  oddennn  13018  evenennn  13019  unennn  13023  exmidunben  13052  znidomb  14678  sincos6thpi  15572  rpcxpsqrtth  15660  2logb9irr  15701  2logb9irrALT  15704  sqrt2cxp2logb9e3  15705  2logb9irrap  15707  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  lgslem1  15735  lgsval  15739  lgsfvalg  15740  lgsfcl2  15741  lgsval2lem  15745  lgsdir2lem2  15764  lgsdir2  15768  lgsdirprm  15769  lgsne0  15773  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  gausslemma2dlem1cl  15794  gausslemma2dlem1f1o  15795  gausslemma2dlem2  15797  gausslemma2dlem3  15798  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  gausslemma2dlem5  15801  gausslemma2dlem6  15802  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  lgsquad2lem2  15817  lgsquad2  15818  lgsquad3  15819  m1lgs  15820  2lgslem1a1  15821  2lgslem1a2  15822  2lgslem1b  15824  2lgslem3b1  15833  2lgslem3c1  15834  2lgs2  15837  2lgs  15839  2lgsoddprmlem2  15841  2lgsoddprmlem3  15846  2lgsoddprm  15848  usgrexmpldifpr  16106  upgr2wlkdc  16234  eupth2lem3lem3fi  16327  ex-fl  16343  ex-dvds  16348  cvgcmp2nlemabs  16662  trilpolemlt1  16671  apdifflemr  16677  apdiff  16678  qdiff  16679