MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1z Structured version   Visualization version   GIF version

Theorem 1z 12001
Description: One is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
1z 1 ∈ ℤ

Proof of Theorem 1z
StepHypRef Expression
1 1nn 11638 . 2 1 ∈ ℕ
21nnzi 11995 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10527  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-neg 10862  df-nn 11628  df-z 11971
This theorem is referenced by:  1zzd  12002  peano2z  12012  peano2zm  12014  3halfnz  12050  peano5uzti  12061  nnuz  12270  eluz2nn  12273  eluzge3nn  12279  1eluzge0  12281  2eluzge1  12283  eluz2b1  12308  uz2m1nn  12312  nninf  12318  nnrecq  12361  qbtwnxr  12583  fz1n  12915  fz10  12918  fz01en  12925  fznatpl1  12951  fz12pr  12954  fztpval  12959  fseq1p1m1  12971  elfzp1b  12974  elfzm1b  12975  4fvwrd4  13017  ige2m2fzo  13090  fz0add1fz1  13097  fzo12sn  13110  fzo13pr  13111  fzo1to4tp  13115  fzofzp1  13124  fzostep1  13143  flge1nn  13181  fldiv4p1lem1div2  13195  modid0  13255  nnnfi  13324  fzennn  13326  fzen2  13327  f13idfv  13358  ser1const  13416  exp1  13425  zexpcl  13434  qexpcl  13435  qexpclz  13440  m1expcl  13442  expp1z  13468  expm1  13469  facnn  13625  fac0  13626  fac1  13627  bcn1  13663  bcpasc  13671  bcnm1  13677  hashsng  13720  hashfz  13778  fz1isolem  13809  seqcoll  13812  hashge2el2difr  13829  ccat2s1p2  13976  ccat2s1p2OLD  13978  s2f1o  14268  f1oun2prg  14269  swrd2lsw  14304  2swrd2eqwrdeq  14305  relexp1g  14375  climuni  14899  isercoll2  15015  iseraltlem1  15028  sum0  15068  sumsnf  15089  climcndslem1  15194  climcndslem2  15195  divcnvshft  15200  supcvg  15201  prod0  15287  prodsn  15306  prodsnf  15308  zrisefaccl  15364  zfallfaccl  15365  sin01gt0  15533  rpnnen2lem10  15566  nthruc  15595  iddvds  15613  1dvds  15614  dvdsle  15650  dvds1  15659  3dvds  15670  n2dvds1  15707  divalglem5  15738  divalg  15744  bitsfzolem  15773  gcdcllem1  15838  gcdcllem3  15840  gcdaddmlem  15862  gcdadd  15864  gcdid  15865  gcd1  15866  1gcd  15871  bezoutlem1  15877  gcdmultipleOLD  15890  lcmgcdlem  15940  lcm1  15944  3lcm2e6woprm  15949  lcmfunsnlem  15975  isprm3  16017  ge2nprmge4  16035  phicl2  16095  phi1  16100  dfphi2  16101  eulerthlem2  16109  prmdiv  16112  prmdiveq  16113  odzcllem  16119  oddprm  16137  pythagtriplem4  16146  pcpre1  16169  pc1  16182  pcrec  16185  pcmpt  16218  fldivp1  16223  expnprm  16228  pockthlem  16231  unbenlem  16234  prmreclem2  16243  prmrec  16248  igz  16260  4sqlem12  16282  4sqlem13  16283  4sqlem19  16289  vdwlem8  16314  vdwlem13  16319  prmo1  16363  fvprmselgcd1  16371  prmgaplem7  16383  prmlem0  16429  1259lem4  16457  2503lem2  16461  4001lem1  16464  setsstruct  16513  gsumpropd2lem  17879  mulgfval  18166  mulg1  18175  mulgm1  18188  mulgp1  18200  mulgneg2  18201  cycsubgcl  18289  odinv  18619  efgs1b  18793  lt6abl  18946  pgpfac1lem2  19128  srgbinomlem4  19224  qsubdrg  20527  zsubrg  20528  gzsubrg  20529  zringmulg  20555  zringcyg  20568  mulgrhm  20575  mulgrhm2  20576  chrnzr  20607  frgpcyg  20650  zrhpsgnmhm  20658  zrhpsgnodpm  20666  m2detleiblem1  21163  m2detleiblem2  21167  zfbas  22434  imasdsf1olem  22912  cphipval  23775  cmetcaulem  23820  bcthlem5  23860  ehl1eudis  23952  ovolctb  24020  ovolunlem1a  24026  ovolunlem1  24027  ovoliunnul  24037  ovolicc1  24046  ovolicc2lem4  24050  voliunlem1  24080  volsup  24086  uniioombllem6  24118  vitalilem5  24142  plyeq0lem  24729  vieta1lem2  24829  elqaalem2  24838  qaa  24841  iaa  24843  abelthlem6  24953  abelthlem9  24957  sin2pim  25000  cos2pim  25001  logbleb  25288  logblt  25289  1cubrlem  25346  leibpilem2  25447  emcllem5  25505  emcllem7  25507  lgamgulm2  25541  lgamcvglem  25545  gamcvg2lem  25564  lgam1  25569  wilthlem2  25574  wilthlem3  25575  ppip1le  25666  ppi1  25669  cht1  25670  chp1  25672  cht2  25677  ppieq0  25681  ppiub  25708  chpeq0  25712  chpchtsum  25723  chpub  25724  logfacbnd3  25727  logexprlim  25729  bposlem1  25788  bposlem2  25789  bposlem5  25792  bposlem6  25793  lgslem2  25802  lgsfcl2  25807  lgsval2lem  25811  lgsdir2lem1  25829  lgsdir2lem5  25833  1lgs  25844  lgsdchr  25859  lgsquad2lem2  25889  2sqlem9  25931  2sqlem10  25932  2sqblem  25935  2sqb  25936  dchrisumlem3  25995  log2sumbnd  26048  qabvle  26129  ostth3  26142  istrkg3ld  26175  tgldimor  26216  axlowdimlem3  26658  axlowdimlem6  26661  axlowdimlem7  26662  axlowdimlem16  26671  axlowdimlem17  26672  axlowdim  26675  usgrexmpldifpr  26968  uhgrwkspthlem2  27463  pthdlem2  27477  0ewlk  27821  0pth  27832  1wlkdlem1  27844  ntrl2v2e  27865  eupth2lem3lem4  27938  ex-fl  28154  ipval2  28412  hlim0  28940  opsqrlem2  29846  iuninc  30241  nndiffz1  30436  fzom1ne1  30451  0dp2dp  30513  cshw1s2  30562  cycpmco2lem4  30699  lmatfvlem  30980  mdetpmtr1  30988  mdetpmtr12  30990  lmlim  31090  qqh0  31125  qqh1  31126  esumfzf  31228  esumfsup  31229  esumpcvgval  31237  esumcvg  31245  esumcvgsum  31247  esumsup  31248  dya2ub  31428  rrvsum  31612  dstfrvclim1  31635  ballotlem2  31646  ballotlemfc0  31650  ballotlemfcc  31651  signsvf0  31750  hgt750leme  31829  subfac1  32323  subfacp1lem1  32324  subfacp1lem2a  32325  subfacp1lem5  32329  subfacp1lem6  32330  cvmliftlem10  32439  divcnvlin  32862  faclimlem1  32873  fwddifnp1  33524  poimirlem3  34777  poimirlem4  34778  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimirlem32  34806  mblfinlem1  34811  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  fdc  34903  heibor1lem  34970  rrncmslem  34993  nn0rppwr  39062  nn0expgcd  39064  mapfzcons  39193  mzpexpmpt  39222  eldioph3b  39242  fz1eqin  39246  diophin  39249  diophun  39250  0dioph  39255  elnnrabdioph  39284  rabren3dioph  39292  irrapxlem1  39299  irrapxlem3  39301  rmxyadd  39398  rmxy1  39399  rmxy0  39400  rmxp1  39409  rmyp1  39410  rmxm1  39411  rmym1  39412  jm2.24nn  39436  acongeq  39460  jm2.23  39473  jm2.15nn0  39480  jm2.16nn0  39481  jm2.27c  39484  jm2.27dlem2  39487  rmydioph  39491  rmxdioph  39493  expdiophlem2  39499  expdioph  39500  mpaaeu  39630  trclfvdecomr  39953  k0004val0  40384  hashnzfzclim  40534  sumsnd  41163  fmuldfeq  41744  stoweidlem3  42169  stoweidlem20  42186  stoweidlem34  42200  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem11  42250  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  fourierdlem47  42319  fourierswlem  42396  smfmullem4  42950  1oddALTV  43702  1nevenALTV  43703  2evenALTV  43704  nnsum3primes4  43800  nnsum3primesprm  43802  nnsum3primesgbe  43804  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  tgblthelfgott  43827  1odd  43925  efmnd1hash  43959  altgsumbcALT  44299  zlmodzxzsubm  44305  blen2  44543  blennngt2o2  44550  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator