Theorem 2z 9420

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

Syntax hints:   ∈ wcel 2177  2c2 9107  ℤcz 9392

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488  ax-setind 4593  ax-cnex 8036  ax-resscn 8037  ax-1cn 8038  ax-1re 8039  ax-icn 8040  ax-addcl 8041  ax-addrcl 8042  ax-mulcl 8043  ax-addcom 8045  ax-addass 8047  ax-distr 8049  ax-i2m1 8050  ax-0lt1 8051  ax-0id 8053  ax-rnegex 8054  ax-cnre 8056  ax-pre-ltirr 8057  ax-pre-ltwlin 8058  ax-pre-lttrn 8059  ax-pre-ltadd 8061

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3003  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-int 3892  df-br 4052  df-opab 4114  df-id 4348  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-iota 5241  df-fun 5282  df-fv 5288  df-riota 5912  df-ov 5960  df-oprab 5961  df-mpo 5962  df-pnf 8129  df-mnf 8130  df-xr 8131  df-ltxr 8132  df-le 8133  df-sub 8265  df-neg 8266  df-inn 9057  df-2 9115  df-z 9393

This theorem is referenced by:  nn0n0n1ge2b  9472  nn0lt2  9474  nn0le2is012  9475  zadd2cl  9522  eluz4eluz2  9708  uzuzle23  9712  2eluzge1  9717  eluz2b1  9742  nn01to3  9758  nn0ge2m1nnALT  9759  ige2m1fz  10252  fz0to3un2pr  10265  fz0to4untppr  10266  fzctr  10275  fzo0to2pr  10369  fzo0to42pr  10371  qbtwnre  10421  2tnp1ge0ge0  10466  flhalf  10467  m1modge3gt1  10538  q2txmodxeq0  10551  sq1  10800  expnass  10812  sqrecapd  10844  sqoddm1div8  10860  bcn2m1  10936  bcn2p1  10937  4bc2eq6  10941  pfxtrcfv0  11170  pfxtrcfvl  11173  resqrexlemcalc1  11400  resqrexlemnmsq  11403  resqrexlemcvg  11405  resqrexlemglsq  11408  resqrexlemga  11409  resqrexlemsqa  11410  efgt0  12070  tanval3ap  12100  cos01bnd  12144  cos01gt0  12149  egt2lt3  12166  zeo3  12254  odd2np1  12259  even2n  12260  oddm1even  12261  oddp1even  12262  oexpneg  12263  2tp1odd  12270  2teven  12273  evend2  12275  oddp1d2  12276  ltoddhalfle  12279  opoe  12281  omoe  12282  opeo  12283  omeo  12284  m1expo  12286  m1exp1  12287  nn0o1gt2  12291  nn0o  12293  z0even  12297  n2dvds1  12298  z2even  12300  n2dvds3  12301  z4even  12302  4dvdseven  12303  flodddiv4  12322  bits0e  12335  bits0o  12336  bitsp1e  12338  bitsp1o  12339  bitsfzolem  12340  bitsfzo  12341  bitsmod  12342  bitscmp  12344  bitsinv1lem  12347  bitsinv1  12348  6gcd4e2  12391  3lcm2e6woprm  12483  isprm3  12515  prmind2  12517  dvdsnprmd  12522  prm2orodd  12523  2prm  12524  3prm  12525  prmdc  12527  oddprmge3  12532  isprm5  12539  divgcdodd  12540  pw2dvds  12563  sqrt2irraplemnn  12576  oddprm  12657  pythagtriplem2  12664  pythagtriplem4  12666  pythagtriplem11  12672  pythagtriplem13  12674  pythagtrip  12681  4sqlem19  12807  dec2dvds  12809  oddennn  12838  evenennn  12839  unennn  12843  exmidunben  12872  znidomb  14495  sincos6thpi  15389  rpcxpsqrtth  15477  2logb9irr  15518  2logb9irrALT  15521  sqrt2cxp2logb9e3  15522  2logb9irrap  15524  mersenne  15544  perfect1  15545  perfectlem1  15546  perfectlem2  15547  lgslem1  15552  lgsval  15556  lgsfvalg  15557  lgsfcl2  15558  lgsval2lem  15562  lgsdir2lem2  15581  lgsdir2  15585  lgsdirprm  15586  lgsne0  15590  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  gausslemma2dlem1cl  15611  gausslemma2dlem1f1o  15612  gausslemma2dlem2  15614  gausslemma2dlem3  15615  gausslemma2dlem4  15616  gausslemma2dlem5a  15617  gausslemma2dlem5  15618  gausslemma2dlem6  15619  gausslemma2dlem7  15620  gausslemma2d  15621  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgseisen  15626  lgsquadlem1  15629  lgsquadlem2  15630  lgsquad2lem1  15633  lgsquad2lem2  15634  lgsquad2  15635  lgsquad3  15636  m1lgs  15637  2lgslem1a1  15638  2lgslem1a2  15639  2lgslem1b  15641  2lgslem3b1  15650  2lgslem3c1  15651  2lgs2  15654  2lgs  15656  2lgsoddprmlem2  15658  2lgsoddprmlem3  15663  2lgsoddprm  15665  ex-fl  15800  ex-dvds  15805  cvgcmp2nlemabs  16112  trilpolemlt1  16121  apdifflemr  16127  apdiff  16128