ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2z GIF version

Theorem 2z 8703
Description: Two is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
2z 2 ∈ ℤ

Proof of Theorem 2z
StepHypRef Expression
1 2nn 8503 . 2 2 ∈ ℕ
21nnzi 8696 1 2 ∈ ℤ
Colors of variables: wff set class
Syntax hints:  wcel 1436  2c2 8399  cz 8675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-cnex 7372  ax-resscn 7373  ax-1cn 7374  ax-1re 7375  ax-icn 7376  ax-addcl 7377  ax-addrcl 7378  ax-mulcl 7379  ax-addcom 7381  ax-addass 7383  ax-distr 7385  ax-i2m1 7386  ax-0lt1 7387  ax-0id 7389  ax-rnegex 7390  ax-cnre 7392  ax-pre-ltirr 7393  ax-pre-ltwlin 7394  ax-pre-lttrn 7395  ax-pre-ltadd 7397
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-br 3820  df-opab 3874  df-id 4092  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-iota 4942  df-fun 4979  df-fv 4985  df-riota 5562  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-pnf 7460  df-mnf 7461  df-xr 7462  df-ltxr 7463  df-le 7464  df-sub 7591  df-neg 7592  df-inn 8350  df-2 8408  df-z 8676
This theorem is referenced by:  nn0n0n1ge2b  8751  nn0lt2  8753  zadd2cl  8800  uzuzle23  8983  2eluzge1  8988  eluz2b1  9012  nn01to3  9026  nn0ge2m1nnALT  9027  ige2m1fz  9446  fzctr  9464  fzo0to2pr  9549  fzo0to42pr  9551  rebtwn2zlemshrink  9585  qbtwnre  9588  2tnp1ge0ge0  9628  flhalf  9629  m1modge3gt1  9698  q2txmodxeq0  9711  sq1  9938  expnass  9949  sqrecapd  9978  sqoddm1div8  9994  bcn2m1  10065  bcn2p1  10066  4bc2eq6  10070  resqrexlemcalc1  10334  resqrexlemnmsq  10337  resqrexlemcvg  10339  resqrexlemglsq  10342  resqrexlemga  10343  resqrexlemsqa  10344  zeo3  10734  odd2np1  10739  even2n  10740  oddm1even  10741  oddp1even  10742  oexpneg  10743  2tp1odd  10750  2teven  10753  evend2  10755  oddp1d2  10756  ltoddhalfle  10759  opoe  10761  omoe  10762  opeo  10763  omeo  10764  m1expo  10766  m1exp1  10767  nn0o1gt2  10771  nn0o  10773  z0even  10777  n2dvds1  10778  z2even  10780  n2dvds3  10781  z4even  10782  4dvdseven  10783  flodddiv4  10800  6gcd4e2  10850  3lcm2e6woprm  10934  isprm3  10966  prmind2  10968  dvdsnprmd  10973  prm2orodd  10974  2prm  10975  3prm  10976  oddprmge3  10982  divgcdodd  10988  pw2dvds  11010  sqrt2irraplemnn  11023  oddennn  11071  evenennn  11072  unennn  11076  ex-fl  11082  ex-dvds  11086
  Copyright terms: Public domain W3C validator