Theorem 1z 12555

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

Syntax hints:   ∈ wcel 2119  1c1 11037  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11378  df-nn 12173  df-z 12523

This theorem is referenced by:  1zzd  12556  peano2z  12566  peano2zm  12568  3halfnz  12606  peano5uzti  12617  nnuz  12825  1eluzge0  12828  2eluzge1  12830  eluz2nn  12836  eluz2b1  12867  uz2m1nn  12871  nninf  12877  nnrecq  12920  qbtwnxr  13150  fz1n  13494  fz10  13497  fz01en  13504  fznatpl1  13530  fz12pr  13533  fztpval  13538  fseq1p1m1  13550  elfzp1b  13553  elfzm1b  13554  4fvwrd4  13600  fzo1lb  13666  ige2m2fzo  13681  fz0add1fz1  13688  fzo12sn  13701  fzo13pr  13702  fzo1to4tp  13707  fzofzp1  13717  fzom1ne1  13738  fzostep1  13739  flge1nn  13778  fldiv4p1lem1div2  13792  modid0  13854  nnnfi  13926  fzennn  13928  fzen2  13929  f13idfv  13960  ser1const  14018  exp1  14027  zexpcl  14036  qexpcl  14037  qexpclz  14041  m1expcl  14046  expp1z  14071  expm1  14072  facnn  14235  fac0  14236  fac1  14237  bcn1  14273  bcpasc  14281  bcnm1  14287  hashsng  14329  hashfz  14387  fz1isolem  14421  seqcoll  14424  hashge2el2difr  14441  ccat2s1p2  14591  s2f1o  14876  f1oun2prg  14877  swrd2lsw  14912  2swrd2eqwrdeq  14913  relexp1g  14986  climuni  15512  isercoll2  15629  iseraltlem1  15642  sum0  15681  sumsnf  15703  climcndslem1  15812  climcndslem2  15813  divcnvshft  15818  supcvg  15819  prod0  15906  prodsn  15925  prodsnf  15927  zrisefaccl  15983  zfallfaccl  15984  sin01gt0  16155  rpnnen2lem10  16188  nthruc  16217  iddvds  16236  1dvds  16237  dvdsle  16277  dvds1  16286  3dvds  16298  n2dvds1  16335  divalglem5  16364  divalg  16370  bitsfzolem  16401  gcdcllem1  16466  gcdcllem3  16468  gcdaddmlem  16491  gcdadd  16493  gcdid  16494  gcd1  16495  1gcd  16500  bezoutlem1  16506  nn0rppwr  16528  nn0expgcd  16531  lcmgcdlem  16573  lcm1  16577  3lcm2e6woprm  16582  lcmfunsnlem  16608  isprm3  16650  ge2nprmge4  16669  phicl2  16736  phi1  16741  dfphi2  16742  eulerthlem2  16750  prmdiv  16753  prmdiveq  16754  odzcllem  16761  oddprm  16779  pythagtriplem4  16788  pcpre1  16811  pc1  16824  pcrec  16827  pcmpt  16861  fldivp1  16866  expnprm  16871  pockthlem  16874  unbenlem  16877  prmreclem2  16886  prmrec  16891  igz  16903  4sqlem12  16925  4sqlem13  16926  4sqlem19  16932  vdwlem8  16957  vdwlem13  16962  prmo1  17006  fvprmselgcd1  17014  prmlem0  17074  1259lem4  17102  2503lem2  17106  4001lem1  17109  setsstruct  17144  chnub  18586  gsumpropd2lem  18645  efmnd1hash  18858  mulgfval  19043  mulg1  19055  mulgm1  19068  mulgp1  19081  mulgneg2  19082  cycsubgcl  19179  odinv  19534  efgs1b  19709  lt6abl  19868  pgpfac1lem2  20050  srgbinomlem4  20208  qsubdrg  21401  zsubrg  21402  gzsubrg  21403  zringmulg  21438  zringcyg  21451  mulgrhm  21459  mulgrhm2  21460  pzriprnglem7  21469  pzriprnglem9  21471  pzriprnglem12  21474  pzriprnglem13  21475  pzriprnglem14  21476  pzriprng1ALT  21478  fermltlchr  21511  chrnzr  21512  frgpcyg  21555  zrhpsgnmhm  21566  zrhpsgnodpm  21574  m2detleiblem1  22614  m2detleiblem2  22618  zfbas  23886  imasdsf1olem  24363  cphipval  25235  cmetcaulem  25280  bcthlem5  25320  ehl1eudis  25412  ovolctb  25482  ovolunlem1a  25488  ovolunlem1  25489  ovoliunnul  25499  ovolicc1  25508  ovolicc2lem4  25512  voliunlem1  25542  volsup  25548  uniioombllem6  25580  vitalilem5  25604  plyeq0lem  26200  vieta1lem2  26302  elqaalem2  26311  qaa  26314  iaa  26316  abelthlem6  26426  abelthlem9  26430  sin2pim  26474  cos2pim  26475  logbleb  26772  logblt  26773  1cubrlem  26830  leibpilem2  26930  emcllem5  26988  emcllem7  26990  lgamgulm2  27024  lgamcvglem  27028  gamcvg2lem  27047  lgam1  27052  wilthlem2  27057  wilthlem3  27058  ppip1le  27149  ppi1  27152  cht1  27153  chp1  27155  cht2  27160  ppieq0  27164  ppiub  27192  chpeq0  27196  chpchtsum  27207  chpub  27208  logfacbnd3  27211  logexprlim  27213  bposlem1  27272  bposlem2  27273  bposlem5  27276  bposlem6  27277  lgslem2  27286  lgsfcl2  27291  lgsval2lem  27295  lgsdir2lem1  27313  lgsdir2lem5  27317  1lgs  27328  lgsdchr  27343  lgsquad2lem2  27373  2sqlem9  27415  2sqlem10  27416  2sqblem  27419  2sqb  27420  dchrisumlem3  27479  log2sumbnd  27532  qabvle  27613  ostth3  27626  istrkg3ld  28554  tgldimor  28595  axlowdimlem3  29038  axlowdimlem6  29041  axlowdimlem7  29042  axlowdimlem16  29051  axlowdimlem17  29052  axlowdim  29055  usgrexmpldifpr  29352  dfpth2  29822  uhgrwkspthlem2  29847  pthdlem2  29861  0ewlk  30209  0pth  30220  1wlkdlem1  30232  ntrl2v2e  30253  eupth2lem3lem4  30326  ex-fl  30542  ipval2  30803  hlim0  31331  opsqrlem2  32237  iuninc  32656  nndiffz1  32885  0dp2dp  32994  cshw1s2  33046  cycpmco2lem4  33217  1fldgenq  33413  znfermltl  33456  zringfrac  33644  constrextdg2  33940  cos9thpiminplylem5  33977  lmatfvlem  34006  mdetpmtr1  34014  mdetpmtr12  34016  lmlim  34138  qqh0  34175  qqh1  34176  esumfzf  34260  esumfsup  34261  esumpcvgval  34269  esumcvg  34277  esumcvgsum  34279  esumsup  34280  dya2ub  34461  rrvsum  34645  dstfrvclim1  34669  ballotlem2  34680  ballotlemfc0  34684  ballotlemfcc  34685  signsvf0  34771  hgt750leme  34849  subfac1  35413  subfacp1lem1  35414  subfacp1lem2a  35415  subfacp1lem5  35419  subfacp1lem6  35420  cvmliftlem10  35529  divcnvlin  35968  faclimlem1  35978  fwddifnp1  36400  irrdiff  37693  qdiff  37694  poimirlem3  37997  poimirlem4  37998  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem24  38018  poimirlem27  38021  poimirlem28  38022  poimirlem31  38025  poimirlem32  38026  mblfinlem1  38031  mblfinlem2  38032  ovoliunnfl  38036  voliunnfl  38038  fdc  38119  heibor1lem  38183  rrncmslem  38206  lcmfunnnd  42504  lcm1un  42505  lcm2un  42506  lcmineqlem11  42531  lcmineqlem19  42539  aks4d1p1p2  42562  mapfzcons  43172  mzpexpmpt  43201  eldioph3b  43221  fz1eqin  43225  diophin  43228  diophun  43229  0dioph  43234  elnnrabdioph  43259  rabren3dioph  43267  irrapxlem1  43274  irrapxlem3  43276  rmxyadd  43373  rmxy1  43374  rmxy0  43375  rmxp1  43384  rmyp1  43385  rmxm1  43386  rmym1  43387  jm2.24nn  43411  acongeq  43435  jm2.23  43448  jm2.15nn0  43455  jm2.16nn0  43456  jm2.27c  43459  jm2.27dlem2  43462  rmydioph  43466  rmxdioph  43468  expdiophlem2  43474  expdioph  43475  mpaaeu  43602  trclfvdecomr  44179  k0004val0  44605  hashnzfzclim  44773  sumsnd  45481  fmuldfeq  46035  stoweidlem3  46453  stoweidlem20  46470  stoweidlem34  46484  wallispilem4  46518  wallispi2lem1  46521  wallispi2lem2  46522  stirlinglem11  46534  dirkerper  46546  dirkertrigeqlem1  46548  dirkertrigeqlem3  46550  fourierdlem47  46603  fourierswlem  46680  smfmullem4  47244  ormklocald  47326  natlocalincr  47328  nthrucw  47338  ceilhalf1  47808  nprmdvdsfacm1lem4  48108  ppivalnnprm  48110  ppivalnn  48117  1oddALTV  48188  1nevenALTV  48189  2evenALTV  48190  nnsum3primes4  48286  nnsum3primesprm  48288  nnsum3primesgbe  48290  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  tgblthelfgott  48313  stgr1  48459  gpgusgralem  48554  1odd  48669  altgsumbcALT  48851  zlmodzxzsubm  48857  blen2  49083  blennngt2o2  49090  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118