Theorem 1z 12523

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

Syntax hints:   ∈ wcel 2109  1c1 11029  ℤcz 12489

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 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11368  df-nn 12147  df-z 12490

This theorem is referenced by:  1zzd  12524  peano2z  12534  peano2zm  12536  3halfnz  12573  peano5uzti  12584  nnuz  12796  1eluzge0  12799  2eluzge1  12801  eluz2nn  12807  eluz2b1  12838  uz2m1nn  12842  nninf  12848  nnrecq  12891  qbtwnxr  13120  fz1n  13463  fz10  13466  fz01en  13473  fznatpl1  13499  fz12pr  13502  fztpval  13507  fseq1p1m1  13519  elfzp1b  13522  elfzm1b  13523  4fvwrd4  13569  fzo1lb  13634  ige2m2fzo  13649  fz0add1fz1  13656  fzo12sn  13669  fzo13pr  13670  fzo1to4tp  13675  fzofzp1  13685  fzostep1  13704  flge1nn  13743  fldiv4p1lem1div2  13757  modid0  13819  nnnfi  13891  fzennn  13893  fzen2  13894  f13idfv  13925  ser1const  13983  exp1  13992  zexpcl  14001  qexpcl  14002  qexpclz  14006  m1expcl  14011  expp1z  14036  expm1  14037  facnn  14200  fac0  14201  fac1  14202  bcn1  14238  bcpasc  14246  bcnm1  14252  hashsng  14294  hashfz  14352  fz1isolem  14386  seqcoll  14389  hashge2el2difr  14406  ccat2s1p2  14555  s2f1o  14841  f1oun2prg  14842  swrd2lsw  14877  2swrd2eqwrdeq  14878  relexp1g  14951  climuni  15477  isercoll2  15594  iseraltlem1  15607  sum0  15646  sumsnf  15668  climcndslem1  15774  climcndslem2  15775  divcnvshft  15780  supcvg  15781  prod0  15868  prodsn  15887  prodsnf  15889  zrisefaccl  15945  zfallfaccl  15946  sin01gt0  16117  rpnnen2lem10  16150  nthruc  16179  iddvds  16198  1dvds  16199  dvdsle  16239  dvds1  16248  3dvds  16260  n2dvds1  16297  divalglem5  16326  divalg  16332  bitsfzolem  16363  gcdcllem1  16428  gcdcllem3  16430  gcdaddmlem  16453  gcdadd  16455  gcdid  16456  gcd1  16457  1gcd  16462  bezoutlem1  16468  nn0rppwr  16490  nn0expgcd  16493  lcmgcdlem  16535  lcm1  16539  3lcm2e6woprm  16544  lcmfunsnlem  16570  isprm3  16612  ge2nprmge4  16630  phicl2  16697  phi1  16702  dfphi2  16703  eulerthlem2  16711  prmdiv  16714  prmdiveq  16715  odzcllem  16722  oddprm  16740  pythagtriplem4  16749  pcpre1  16772  pc1  16785  pcrec  16788  pcmpt  16822  fldivp1  16827  expnprm  16832  pockthlem  16835  unbenlem  16838  prmreclem2  16847  prmrec  16852  igz  16864  4sqlem12  16886  4sqlem13  16887  4sqlem19  16893  vdwlem8  16918  vdwlem13  16923  prmo1  16967  fvprmselgcd1  16975  prmlem0  17035  1259lem4  17063  2503lem2  17067  4001lem1  17070  setsstruct  17105  gsumpropd2lem  18571  efmnd1hash  18784  mulgfval  18966  mulg1  18978  mulgm1  18991  mulgp1  19004  mulgneg2  19005  cycsubgcl  19103  odinv  19458  efgs1b  19633  lt6abl  19792  pgpfac1lem2  19974  srgbinomlem4  20132  qsubdrg  21344  zsubrg  21345  gzsubrg  21346  zringmulg  21381  zringcyg  21394  mulgrhm  21402  mulgrhm2  21403  pzriprnglem7  21412  pzriprnglem9  21414  pzriprnglem12  21417  pzriprnglem13  21418  pzriprnglem14  21419  pzriprng1ALT  21421  fermltlchr  21454  chrnzr  21455  frgpcyg  21498  zrhpsgnmhm  21509  zrhpsgnodpm  21517  m2detleiblem1  22527  m2detleiblem2  22531  zfbas  23799  imasdsf1olem  24277  cphipval  25159  cmetcaulem  25204  bcthlem5  25244  ehl1eudis  25336  ovolctb  25407  ovolunlem1a  25413  ovolunlem1  25414  ovoliunnul  25424  ovolicc1  25433  ovolicc2lem4  25437  voliunlem1  25467  volsup  25473  uniioombllem6  25505  vitalilem5  25529  plyeq0lem  26131  vieta1lem2  26235  elqaalem2  26244  qaa  26247  iaa  26249  abelthlem6  26362  abelthlem9  26366  sin2pim  26410  cos2pim  26411  logbleb  26709  logblt  26710  1cubrlem  26767  leibpilem2  26867  emcllem5  26926  emcllem7  26928  lgamgulm2  26962  lgamcvglem  26966  gamcvg2lem  26985  lgam1  26990  wilthlem2  26995  wilthlem3  26996  ppip1le  27087  ppi1  27090  cht1  27091  chp1  27093  cht2  27098  ppieq0  27102  ppiub  27131  chpeq0  27135  chpchtsum  27146  chpub  27147  logfacbnd3  27150  logexprlim  27152  bposlem1  27211  bposlem2  27212  bposlem5  27215  bposlem6  27216  lgslem2  27225  lgsfcl2  27230  lgsval2lem  27234  lgsdir2lem1  27252  lgsdir2lem5  27256  1lgs  27267  lgsdchr  27282  lgsquad2lem2  27312  2sqlem9  27354  2sqlem10  27355  2sqblem  27358  2sqb  27359  dchrisumlem3  27418  log2sumbnd  27471  qabvle  27552  ostth3  27565  istrkg3ld  28424  tgldimor  28465  axlowdimlem3  28907  axlowdimlem6  28910  axlowdimlem7  28911  axlowdimlem16  28920  axlowdimlem17  28921  axlowdim  28924  usgrexmpldifpr  29221  dfpth2  29692  uhgrwkspthlem2  29717  pthdlem2  29731  0ewlk  30076  0pth  30087  1wlkdlem1  30099  ntrl2v2e  30120  eupth2lem3lem4  30193  ex-fl  30409  ipval2  30669  hlim0  31197  opsqrlem2  32103  iuninc  32522  nndiffz1  32742  fzom1ne1  32757  0dp2dp  32862  cshw1s2  32915  chnub  32967  cycpmco2lem4  33084  1fldgenq  33271  znfermltl  33313  zringfrac  33501  constrextdg2  33715  cos9thpiminplylem5  33752  lmatfvlem  33781  mdetpmtr1  33789  mdetpmtr12  33791  lmlim  33913  qqh0  33950  qqh1  33951  esumfzf  34035  esumfsup  34036  esumpcvgval  34044  esumcvg  34052  esumcvgsum  34054  esumsup  34055  dya2ub  34237  rrvsum  34421  dstfrvclim1  34445  ballotlem2  34456  ballotlemfc0  34460  ballotlemfcc  34461  signsvf0  34547  hgt750leme  34625  subfac1  35150  subfacp1lem1  35151  subfacp1lem2a  35152  subfacp1lem5  35156  subfacp1lem6  35157  cvmliftlem10  35266  divcnvlin  35705  faclimlem1  35715  fwddifnp1  36138  irrdiff  37299  poimirlem3  37602  poimirlem4  37603  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem24  37623  poimirlem27  37626  poimirlem28  37627  poimirlem31  37630  poimirlem32  37631  mblfinlem1  37636  mblfinlem2  37637  ovoliunnfl  37641  voliunnfl  37643  fdc  37724  heibor1lem  37788  rrncmslem  37811  lcmfunnnd  41985  lcm1un  41986  lcm2un  41987  lcmineqlem11  42012  lcmineqlem19  42020  aks4d1p1p2  42043  mapfzcons  42689  mzpexpmpt  42718  eldioph3b  42738  fz1eqin  42742  diophin  42745  diophun  42746  0dioph  42751  elnnrabdioph  42780  rabren3dioph  42788  irrapxlem1  42795  irrapxlem3  42797  rmxyadd  42894  rmxy1  42895  rmxy0  42896  rmxp1  42905  rmyp1  42906  rmxm1  42907  rmym1  42908  jm2.24nn  42932  acongeq  42956  jm2.23  42969  jm2.15nn0  42976  jm2.16nn0  42977  jm2.27c  42980  jm2.27dlem2  42983  rmydioph  42987  rmxdioph  42989  expdiophlem2  42995  expdioph  42996  mpaaeu  43123  trclfvdecomr  43701  k0004val0  44127  hashnzfzclim  44295  sumsnd  45004  fmuldfeq  45565  stoweidlem3  45985  stoweidlem20  46002  stoweidlem34  46016  wallispilem4  46050  wallispi2lem1  46053  wallispi2lem2  46054  stirlinglem11  46066  dirkerper  46078  dirkertrigeqlem1  46080  dirkertrigeqlem3  46082  fourierdlem47  46135  fourierswlem  46212  smfmullem4  46776  ormklocald  46856  natlocalincr  46858  tworepnotupword  46868  ceilhalf1  47319  1oddALTV  47675  1nevenALTV  47676  2evenALTV  47677  nnsum3primes4  47773  nnsum3primesprm  47775  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  tgblthelfgott  47800  stgr1  47946  gpgusgralem  48041  1odd  48156  altgsumbcALT  48338  zlmodzxzsubm  48344  blen2  48571  blennngt2o2  48578  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606