Theorem 1z 12579

Description: One is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
1z	⊢ 1 ∈ ℤ

Proof of Theorem 1z

Step	Hyp	Ref	Expression
1		1nn 12210	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 12573	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 2107  1c1 11098  ℤcz 12545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pr 5423  ax-un 7712  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-i2m1 11165  ax-1ne0 11166  ax-rrecex 11169  ax-cnre 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-ov 7399  df-om 7843  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-neg 11434  df-nn 12200  df-z 12546

This theorem is referenced by:  1zzd  12580  peano2z  12590  peano2zm  12592  3halfnz  12628  peano5uzti  12639  nnuz  12852  eluz2nn  12855  eluzge3nn  12861  1eluzge0  12863  2eluzge1  12865  eluz2b1  12890  uz2m1nn  12894  nninf  12900  nnrecq  12943  qbtwnxr  13166  fz1n  13506  fz10  13509  fz01en  13516  fznatpl1  13542  fz12pr  13545  fztpval  13550  fseq1p1m1  13562  elfzp1b  13565  elfzm1b  13566  4fvwrd4  13608  ige2m2fzo  13682  fz0add1fz1  13689  fzo12sn  13702  fzo13pr  13703  fzo1to4tp  13707  fzofzp1  13716  fzostep1  13735  flge1nn  13773  fldiv4p1lem1div2  13787  modid0  13849  nnnfi  13918  fzennn  13920  fzen2  13921  f13idfv  13952  ser1const  14011  exp1  14020  zexpcl  14029  qexpcl  14030  qexpclz  14034  m1expcl  14039  expp1z  14064  expm1  14065  facnn  14222  fac0  14223  fac1  14224  bcn1  14260  bcpasc  14268  bcnm1  14274  hashsng  14316  hashfz  14374  fz1isolem  14409  seqcoll  14412  hashge2el2difr  14429  ccat2s1p2  14567  s2f1o  14854  f1oun2prg  14855  swrd2lsw  14890  2swrd2eqwrdeq  14891  relexp1g  14960  climuni  15483  isercoll2  15602  iseraltlem1  15615  sum0  15654  sumsnf  15676  climcndslem1  15782  climcndslem2  15783  divcnvshft  15788  supcvg  15789  prod0  15874  prodsn  15893  prodsnf  15895  zrisefaccl  15951  zfallfaccl  15952  sin01gt0  16120  rpnnen2lem10  16153  nthruc  16182  iddvds  16200  1dvds  16201  dvdsle  16240  dvds1  16249  3dvds  16261  n2dvds1  16298  divalglem5  16327  divalg  16333  bitsfzolem  16362  gcdcllem1  16427  gcdcllem3  16429  gcdaddmlem  16452  gcdadd  16454  gcdid  16455  gcd1  16456  1gcd  16462  bezoutlem1  16468  lcmgcdlem  16530  lcm1  16534  3lcm2e6woprm  16539  lcmfunsnlem  16565  isprm3  16607  ge2nprmge4  16625  phicl2  16688  phi1  16693  dfphi2  16694  eulerthlem2  16702  prmdiv  16705  prmdiveq  16706  odzcllem  16712  oddprm  16730  pythagtriplem4  16739  pcpre1  16762  pc1  16775  pcrec  16778  pcmpt  16812  fldivp1  16817  expnprm  16822  pockthlem  16825  unbenlem  16828  prmreclem2  16837  prmrec  16842  igz  16854  4sqlem12  16876  4sqlem13  16877  4sqlem19  16883  vdwlem8  16908  vdwlem13  16913  prmo1  16957  fvprmselgcd1  16965  prmlem0  17026  1259lem4  17054  2503lem2  17058  4001lem1  17061  setsstruct  17096  gsumpropd2lem  18585  efmnd1hash  18760  mulgfval  18937  mulg1  18946  mulgm1  18959  mulgp1  18972  mulgneg2  18973  cycsubgcl  19068  odinv  19413  efgs1b  19588  lt6abl  19746  pgpfac1lem2  19928  srgbinomlem4  20034  qsubdrg  20971  zsubrg  20972  gzsubrg  20973  zringmulg  20999  zringcyg  21012  mulgrhm  21020  mulgrhm2  21021  chrnzr  21055  frgpcyg  21102  zrhpsgnmhm  21110  zrhpsgnodpm  21118  m2detleiblem1  22095  m2detleiblem2  22099  zfbas  23369  imasdsf1olem  23848  cphipval  24729  cmetcaulem  24774  bcthlem5  24814  ehl1eudis  24906  ovolctb  24976  ovolunlem1a  24982  ovolunlem1  24983  ovoliunnul  24993  ovolicc1  25002  ovolicc2lem4  25006  voliunlem1  25036  volsup  25042  uniioombllem6  25074  vitalilem5  25098  plyeq0lem  25693  vieta1lem2  25793  elqaalem2  25802  qaa  25805  iaa  25807  abelthlem6  25917  abelthlem9  25921  sin2pim  25964  cos2pim  25965  logbleb  26255  logblt  26256  1cubrlem  26313  leibpilem2  26413  emcllem5  26471  emcllem7  26473  lgamgulm2  26507  lgamcvglem  26511  gamcvg2lem  26530  lgam1  26535  wilthlem2  26540  wilthlem3  26541  ppip1le  26632  ppi1  26635  cht1  26636  chp1  26638  cht2  26643  ppieq0  26647  ppiub  26674  chpeq0  26678  chpchtsum  26689  chpub  26690  logfacbnd3  26693  logexprlim  26695  bposlem1  26754  bposlem2  26755  bposlem5  26758  bposlem6  26759  lgslem2  26768  lgsfcl2  26773  lgsval2lem  26777  lgsdir2lem1  26795  lgsdir2lem5  26799  1lgs  26810  lgsdchr  26825  lgsquad2lem2  26855  2sqlem9  26897  2sqlem10  26898  2sqblem  26901  2sqb  26902  dchrisumlem3  26961  log2sumbnd  27014  qabvle  27095  ostth3  27108  istrkg3ld  27679  tgldimor  27720  axlowdimlem3  28169  axlowdimlem6  28172  axlowdimlem7  28173  axlowdimlem16  28182  axlowdimlem17  28183  axlowdim  28186  usgrexmpldifpr  28482  uhgrwkspthlem2  28978  pthdlem2  28992  0ewlk  29334  0pth  29345  1wlkdlem1  29357  ntrl2v2e  29378  eupth2lem3lem4  29451  ex-fl  29667  ipval2  29925  hlim0  30453  opsqrlem2  31359  iuninc  31758  nndiffz1  31968  fzom1ne1  31983  0dp2dp  32046  cshw1s2  32095  cycpmco2lem4  32259  1fldgenq  32374  fermltlchr  32440  znfermltl  32441  lmatfvlem  32726  mdetpmtr1  32734  mdetpmtr12  32736  lmlim  32858  qqh0  32895  qqh1  32896  esumfzf  32998  esumfsup  32999  esumpcvgval  33007  esumcvg  33015  esumcvgsum  33017  esumsup  33018  dya2ub  33200  rrvsum  33384  dstfrvclim1  33407  ballotlem2  33418  ballotlemfc0  33422  ballotlemfcc  33423  signsvf0  33522  hgt750leme  33601  subfac1  34100  subfacp1lem1  34101  subfacp1lem2a  34102  subfacp1lem5  34106  subfacp1lem6  34107  cvmliftlem10  34216  divcnvlin  34633  faclimlem1  34644  fwddifnp1  35068  irrdiff  36112  poimirlem3  36396  poimirlem4  36397  poimirlem16  36409  poimirlem17  36410  poimirlem19  36412  poimirlem20  36413  poimirlem24  36417  poimirlem27  36420  poimirlem28  36421  poimirlem31  36424  poimirlem32  36425  mblfinlem1  36430  mblfinlem2  36431  ovoliunnfl  36435  voliunnfl  36437  fdc  36519  heibor1lem  36583  rrncmslem  36606  lcmfunnnd  40783  lcm1un  40784  lcm2un  40785  lcmineqlem11  40810  lcmineqlem19  40818  aks4d1p1p2  40841  nn0rppwr  41105  nn0expgcd  41107  mapfzcons  41325  mzpexpmpt  41354  eldioph3b  41374  fz1eqin  41378  diophin  41381  diophun  41382  0dioph  41387  elnnrabdioph  41416  rabren3dioph  41424  irrapxlem1  41431  irrapxlem3  41433  rmxyadd  41531  rmxy1  41532  rmxy0  41533  rmxp1  41542  rmyp1  41543  rmxm1  41544  rmym1  41545  jm2.24nn  41569  acongeq  41593  jm2.23  41606  jm2.15nn0  41613  jm2.16nn0  41614  jm2.27c  41617  jm2.27dlem2  41620  rmydioph  41624  rmxdioph  41626  expdiophlem2  41632  expdioph  41633  mpaaeu  41763  trclfvdecomr  42350  k0004val0  42776  hashnzfzclim  42952  sumsnd  43581  fmuldfeq  44172  stoweidlem3  44592  stoweidlem20  44609  stoweidlem34  44623  wallispilem4  44657  wallispi2lem1  44660  wallispi2lem2  44661  stirlinglem11  44673  dirkerper  44685  dirkertrigeqlem1  44687  dirkertrigeqlem3  44689  fourierdlem47  44742  fourierswlem  44819  smfmullem4  45383  natlocalincr  45463  tworepnotupword  45473  1oddALTV  46231  1nevenALTV  46232  2evenALTV  46233  nnsum3primes4  46329  nnsum3primesprm  46331  nnsum3primesgbe  46333  nnsum4primesodd  46337  nnsum4primesoddALTV  46338  nnsum4primeseven  46341  nnsum4primesevenALTV  46342  tgblthelfgott  46356  1odd  46454  altgsumbcALT  46869  zlmodzxzsubm  46875  blen2  47111  blennngt2o2  47118  nn0sumshdiglemA  47145  nn0sumshdiglemB  47146