Theorem 1z 12563

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

Syntax hints:   ∈ wcel 2109  1c1 11069  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-z 12530

This theorem is referenced by:  1zzd  12564  peano2z  12574  peano2zm  12576  3halfnz  12613  peano5uzti  12624  nnuz  12836  1eluzge0  12839  2eluzge1  12841  eluz2nn  12847  eluz2b1  12878  uz2m1nn  12882  nninf  12888  nnrecq  12931  qbtwnxr  13160  fz1n  13503  fz10  13506  fz01en  13513  fznatpl1  13539  fz12pr  13542  fztpval  13547  fseq1p1m1  13559  elfzp1b  13562  elfzm1b  13563  4fvwrd4  13609  fzo1lb  13674  ige2m2fzo  13689  fz0add1fz1  13696  fzo12sn  13709  fzo13pr  13710  fzo1to4tp  13715  fzofzp1  13725  fzostep1  13744  flge1nn  13783  fldiv4p1lem1div2  13797  modid0  13859  nnnfi  13931  fzennn  13933  fzen2  13934  f13idfv  13965  ser1const  14023  exp1  14032  zexpcl  14041  qexpcl  14042  qexpclz  14046  m1expcl  14051  expp1z  14076  expm1  14077  facnn  14240  fac0  14241  fac1  14242  bcn1  14278  bcpasc  14286  bcnm1  14292  hashsng  14334  hashfz  14392  fz1isolem  14426  seqcoll  14429  hashge2el2difr  14446  ccat2s1p2  14595  s2f1o  14882  f1oun2prg  14883  swrd2lsw  14918  2swrd2eqwrdeq  14919  relexp1g  14992  climuni  15518  isercoll2  15635  iseraltlem1  15648  sum0  15687  sumsnf  15709  climcndslem1  15815  climcndslem2  15816  divcnvshft  15821  supcvg  15822  prod0  15909  prodsn  15928  prodsnf  15930  zrisefaccl  15986  zfallfaccl  15987  sin01gt0  16158  rpnnen2lem10  16191  nthruc  16220  iddvds  16239  1dvds  16240  dvdsle  16280  dvds1  16289  3dvds  16301  n2dvds1  16338  divalglem5  16367  divalg  16373  bitsfzolem  16404  gcdcllem1  16469  gcdcllem3  16471  gcdaddmlem  16494  gcdadd  16496  gcdid  16497  gcd1  16498  1gcd  16503  bezoutlem1  16509  nn0rppwr  16531  nn0expgcd  16534  lcmgcdlem  16576  lcm1  16580  3lcm2e6woprm  16585  lcmfunsnlem  16611  isprm3  16653  ge2nprmge4  16671  phicl2  16738  phi1  16743  dfphi2  16744  eulerthlem2  16752  prmdiv  16755  prmdiveq  16756  odzcllem  16763  oddprm  16781  pythagtriplem4  16790  pcpre1  16813  pc1  16826  pcrec  16829  pcmpt  16863  fldivp1  16868  expnprm  16873  pockthlem  16876  unbenlem  16879  prmreclem2  16888  prmrec  16893  igz  16905  4sqlem12  16927  4sqlem13  16928  4sqlem19  16934  vdwlem8  16959  vdwlem13  16964  prmo1  17008  fvprmselgcd1  17016  prmlem0  17076  1259lem4  17104  2503lem2  17108  4001lem1  17111  setsstruct  17146  gsumpropd2lem  18606  efmnd1hash  18819  mulgfval  19001  mulg1  19013  mulgm1  19026  mulgp1  19039  mulgneg2  19040  cycsubgcl  19138  odinv  19491  efgs1b  19666  lt6abl  19825  pgpfac1lem2  20007  srgbinomlem4  20138  qsubdrg  21336  zsubrg  21337  gzsubrg  21338  zringmulg  21366  zringcyg  21379  mulgrhm  21387  mulgrhm2  21388  pzriprnglem7  21397  pzriprnglem9  21399  pzriprnglem12  21402  pzriprnglem13  21403  pzriprnglem14  21404  pzriprng1ALT  21406  fermltlchr  21439  chrnzr  21440  frgpcyg  21483  zrhpsgnmhm  21493  zrhpsgnodpm  21501  m2detleiblem1  22511  m2detleiblem2  22515  zfbas  23783  imasdsf1olem  24261  cphipval  25143  cmetcaulem  25188  bcthlem5  25228  ehl1eudis  25320  ovolctb  25391  ovolunlem1a  25397  ovolunlem1  25398  ovoliunnul  25408  ovolicc1  25417  ovolicc2lem4  25421  voliunlem1  25451  volsup  25457  uniioombllem6  25489  vitalilem5  25513  plyeq0lem  26115  vieta1lem2  26219  elqaalem2  26228  qaa  26231  iaa  26233  abelthlem6  26346  abelthlem9  26350  sin2pim  26394  cos2pim  26395  logbleb  26693  logblt  26694  1cubrlem  26751  leibpilem2  26851  emcllem5  26910  emcllem7  26912  lgamgulm2  26946  lgamcvglem  26950  gamcvg2lem  26969  lgam1  26974  wilthlem2  26979  wilthlem3  26980  ppip1le  27071  ppi1  27074  cht1  27075  chp1  27077  cht2  27082  ppieq0  27086  ppiub  27115  chpeq0  27119  chpchtsum  27130  chpub  27131  logfacbnd3  27134  logexprlim  27136  bposlem1  27195  bposlem2  27196  bposlem5  27199  bposlem6  27200  lgslem2  27209  lgsfcl2  27214  lgsval2lem  27218  lgsdir2lem1  27236  lgsdir2lem5  27240  1lgs  27251  lgsdchr  27266  lgsquad2lem2  27296  2sqlem9  27338  2sqlem10  27339  2sqblem  27342  2sqb  27343  dchrisumlem3  27402  log2sumbnd  27455  qabvle  27536  ostth3  27549  istrkg3ld  28388  tgldimor  28429  axlowdimlem3  28871  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  usgrexmpldifpr  29185  dfpth2  29659  uhgrwkspthlem2  29684  pthdlem2  29698  0ewlk  30043  0pth  30054  1wlkdlem1  30066  ntrl2v2e  30087  eupth2lem3lem4  30160  ex-fl  30376  ipval2  30636  hlim0  31164  opsqrlem2  32070  iuninc  32489  nndiffz1  32709  fzom1ne1  32724  0dp2dp  32829  cshw1s2  32882  chnub  32938  cycpmco2lem4  33086  1fldgenq  33272  znfermltl  33337  zringfrac  33525  constrextdg2  33739  cos9thpiminplylem5  33776  lmatfvlem  33805  mdetpmtr1  33813  mdetpmtr12  33815  lmlim  33937  qqh0  33974  qqh1  33975  esumfzf  34059  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  esumcvgsum  34078  esumsup  34079  dya2ub  34261  rrvsum  34445  dstfrvclim1  34469  ballotlem2  34480  ballotlemfc0  34484  ballotlemfcc  34485  signsvf0  34571  hgt750leme  34649  subfac1  35165  subfacp1lem1  35166  subfacp1lem2a  35167  subfacp1lem5  35171  subfacp1lem6  35172  cvmliftlem10  35281  divcnvlin  35720  faclimlem1  35730  fwddifnp1  36153  irrdiff  37314  poimirlem3  37617  poimirlem4  37618  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  mblfinlem1  37651  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  fdc  37739  heibor1lem  37803  rrncmslem  37826  lcmfunnnd  42000  lcm1un  42001  lcm2un  42002  lcmineqlem11  42027  lcmineqlem19  42035  aks4d1p1p2  42058  mapfzcons  42704  mzpexpmpt  42733  eldioph3b  42753  fz1eqin  42757  diophin  42760  diophun  42761  0dioph  42766  elnnrabdioph  42795  rabren3dioph  42803  irrapxlem1  42810  irrapxlem3  42812  rmxyadd  42910  rmxy1  42911  rmxy0  42912  rmxp1  42921  rmyp1  42922  rmxm1  42923  rmym1  42924  jm2.24nn  42948  acongeq  42972  jm2.23  42985  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27c  42996  jm2.27dlem2  42999  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  mpaaeu  43139  trclfvdecomr  43717  k0004val0  44143  hashnzfzclim  44311  sumsnd  45020  fmuldfeq  45581  stoweidlem3  46001  stoweidlem20  46018  stoweidlem34  46032  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem11  46082  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  fourierdlem47  46151  fourierswlem  46228  smfmullem4  46792  ormklocald  46872  natlocalincr  46874  tworepnotupword  46884  ceilhalf1  47335  1oddALTV  47691  1nevenALTV  47692  2evenALTV  47693  nnsum3primes4  47789  nnsum3primesprm  47791  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  tgblthelfgott  47816  stgr1  47960  gpgusgralem  48047  1odd  48159  altgsumbcALT  48341  zlmodzxzsubm  48347  blen2  48574  blennngt2o2  48581  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609