Theorem 2z 9485

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

Syntax hints:   ∈ wcel 2200  2c2 9172  ℤcz 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  11241  pfxtrcfvl  11244  resqrexlemcalc1  11540  resqrexlemnmsq  11543  resqrexlemcvg  11545  resqrexlemglsq  11548  resqrexlemga  11549  resqrexlemsqa  11550  efgt0  12210  tanval3ap  12240  cos01bnd  12284  cos01gt0  12289  egt2lt3  12306  zeo3  12394  odd2np1  12399  even2n  12400  oddm1even  12401  oddp1even  12402  oexpneg  12403  2tp1odd  12410  2teven  12413  evend2  12415  oddp1d2  12416  ltoddhalfle  12419  opoe  12421  omoe  12422  opeo  12423  omeo  12424  m1expo  12426  m1exp1  12427  nn0o1gt2  12431  nn0o  12433  z0even  12437  n2dvds1  12438  z2even  12440  n2dvds3  12441  z4even  12442  4dvdseven  12443  flodddiv4  12462  bits0e  12475  bits0o  12476  bitsp1e  12478  bitsp1o  12479  bitsfzolem  12480  bitsfzo  12481  bitsmod  12482  bitscmp  12484  bitsinv1lem  12487  bitsinv1  12488  6gcd4e2  12531  3lcm2e6woprm  12623  isprm3  12655  prmind2  12657  dvdsnprmd  12662  prm2orodd  12663  2prm  12664  3prm  12665  prmdc  12667  oddprmge3  12672  isprm5  12679  divgcdodd  12680  pw2dvds  12703  sqrt2irraplemnn  12716  oddprm  12797  pythagtriplem2  12804  pythagtriplem4  12806  pythagtriplem11  12812  pythagtriplem13  12814  pythagtrip  12821  4sqlem19  12947  dec2dvds  12949  oddennn  12978  evenennn  12979  unennn  12983  exmidunben  13012  znidomb  14637  sincos6thpi  15531  rpcxpsqrtth  15619  2logb9irr  15660  2logb9irrALT  15663  sqrt2cxp2logb9e3  15664  2logb9irrap  15666  mersenne  15686  perfect1  15687  perfectlem1  15688  perfectlem2  15689  lgslem1  15694  lgsval  15698  lgsfvalg  15699  lgsfcl2  15700  lgsval2lem  15704  lgsdir2lem2  15723  lgsdir2  15727  lgsdirprm  15728  lgsne0  15732  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  gausslemma2dlem1cl  15753  gausslemma2dlem1f1o  15754  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  gausslemma2dlem5a  15759  gausslemma2dlem5  15760  gausslemma2dlem6  15761  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  lgsquad2lem2  15776  lgsquad2  15777  lgsquad3  15778  m1lgs  15779  2lgslem1a1  15780  2lgslem1a2  15781  2lgslem1b  15783  2lgslem3b1  15792  2lgslem3c1  15793  2lgs2  15796  2lgs  15798  2lgsoddprmlem2  15800  2lgsoddprmlem3  15805  2lgsoddprm  15807  upgr2wlkdc  16116  ex-fl  16144  ex-dvds  16149  cvgcmp2nlemabs  16460  trilpolemlt1  16469  apdifflemr  16475  apdiff  16476