Theorem 1z 12620

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

Syntax hints:   ∈ wcel 2108  1c1 11128  ℤcz 12586

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-neg 11467  df-nn 12239  df-z 12587

This theorem is referenced by:  1zzd  12621  peano2z  12631  peano2zm  12633  3halfnz  12670  peano5uzti  12681  nnuz  12893  eluz2nn  12896  eluzge3nn  12904  1eluzge0  12906  2eluzge1  12908  eluz2b1  12933  uz2m1nn  12937  nninf  12943  nnrecq  12986  qbtwnxr  13214  fz1n  13557  fz10  13560  fz01en  13567  fznatpl1  13593  fz12pr  13596  fztpval  13601  fseq1p1m1  13613  elfzp1b  13616  elfzm1b  13617  4fvwrd4  13663  fzo1lb  13728  ige2m2fzo  13742  fz0add1fz1  13749  fzo12sn  13762  fzo13pr  13763  fzo1to4tp  13768  fzofzp1  13778  fzostep1  13797  flge1nn  13836  fldiv4p1lem1div2  13850  modid0  13912  nnnfi  13982  fzennn  13984  fzen2  13985  f13idfv  14016  ser1const  14074  exp1  14083  zexpcl  14092  qexpcl  14093  qexpclz  14097  m1expcl  14102  expp1z  14127  expm1  14128  facnn  14291  fac0  14292  fac1  14293  bcn1  14329  bcpasc  14337  bcnm1  14343  hashsng  14385  hashfz  14443  fz1isolem  14477  seqcoll  14480  hashge2el2difr  14497  ccat2s1p2  14646  s2f1o  14933  f1oun2prg  14934  swrd2lsw  14969  2swrd2eqwrdeq  14970  relexp1g  15043  climuni  15566  isercoll2  15683  iseraltlem1  15696  sum0  15735  sumsnf  15757  climcndslem1  15863  climcndslem2  15864  divcnvshft  15869  supcvg  15870  prod0  15957  prodsn  15976  prodsnf  15978  zrisefaccl  16034  zfallfaccl  16035  sin01gt0  16206  rpnnen2lem10  16239  nthruc  16268  iddvds  16287  1dvds  16288  dvdsle  16327  dvds1  16336  3dvds  16348  n2dvds1  16385  divalglem5  16414  divalg  16420  bitsfzolem  16451  gcdcllem1  16516  gcdcllem3  16518  gcdaddmlem  16541  gcdadd  16543  gcdid  16544  gcd1  16545  1gcd  16550  bezoutlem1  16556  nn0rppwr  16578  nn0expgcd  16581  lcmgcdlem  16623  lcm1  16627  3lcm2e6woprm  16632  lcmfunsnlem  16658  isprm3  16700  ge2nprmge4  16718  phicl2  16785  phi1  16790  dfphi2  16791  eulerthlem2  16799  prmdiv  16802  prmdiveq  16803  odzcllem  16810  oddprm  16828  pythagtriplem4  16837  pcpre1  16860  pc1  16873  pcrec  16876  pcmpt  16910  fldivp1  16915  expnprm  16920  pockthlem  16923  unbenlem  16926  prmreclem2  16935  prmrec  16940  igz  16952  4sqlem12  16974  4sqlem13  16975  4sqlem19  16981  vdwlem8  17006  vdwlem13  17011  prmo1  17055  fvprmselgcd1  17063  prmlem0  17123  1259lem4  17151  2503lem2  17155  4001lem1  17158  setsstruct  17193  gsumpropd2lem  18655  efmnd1hash  18868  mulgfval  19050  mulg1  19062  mulgm1  19075  mulgp1  19088  mulgneg2  19089  cycsubgcl  19187  odinv  19540  efgs1b  19715  lt6abl  19874  pgpfac1lem2  20056  srgbinomlem4  20187  qsubdrg  21385  zsubrg  21386  gzsubrg  21387  zringmulg  21415  zringcyg  21428  mulgrhm  21436  mulgrhm2  21437  pzriprnglem7  21446  pzriprnglem9  21448  pzriprnglem12  21451  pzriprnglem13  21452  pzriprnglem14  21453  pzriprng1ALT  21455  fermltlchr  21488  chrnzr  21489  frgpcyg  21532  zrhpsgnmhm  21542  zrhpsgnodpm  21550  m2detleiblem1  22560  m2detleiblem2  22564  zfbas  23832  imasdsf1olem  24310  cphipval  25193  cmetcaulem  25238  bcthlem5  25278  ehl1eudis  25370  ovolctb  25441  ovolunlem1a  25447  ovolunlem1  25448  ovoliunnul  25458  ovolicc1  25467  ovolicc2lem4  25471  voliunlem1  25501  volsup  25507  uniioombllem6  25539  vitalilem5  25563  plyeq0lem  26165  vieta1lem2  26269  elqaalem2  26278  qaa  26281  iaa  26283  abelthlem6  26396  abelthlem9  26400  sin2pim  26444  cos2pim  26445  logbleb  26743  logblt  26744  1cubrlem  26801  leibpilem2  26901  emcllem5  26960  emcllem7  26962  lgamgulm2  26996  lgamcvglem  27000  gamcvg2lem  27019  lgam1  27024  wilthlem2  27029  wilthlem3  27030  ppip1le  27121  ppi1  27124  cht1  27125  chp1  27127  cht2  27132  ppieq0  27136  ppiub  27165  chpeq0  27169  chpchtsum  27180  chpub  27181  logfacbnd3  27184  logexprlim  27186  bposlem1  27245  bposlem2  27246  bposlem5  27249  bposlem6  27250  lgslem2  27259  lgsfcl2  27264  lgsval2lem  27268  lgsdir2lem1  27286  lgsdir2lem5  27290  1lgs  27301  lgsdchr  27316  lgsquad2lem2  27346  2sqlem9  27388  2sqlem10  27389  2sqblem  27392  2sqb  27393  dchrisumlem3  27452  log2sumbnd  27505  qabvle  27586  ostth3  27599  istrkg3ld  28386  tgldimor  28427  axlowdimlem3  28869  axlowdimlem6  28872  axlowdimlem7  28873  axlowdimlem16  28882  axlowdimlem17  28883  axlowdim  28886  usgrexmpldifpr  29183  dfpth2  29657  uhgrwkspthlem2  29682  pthdlem2  29696  0ewlk  30041  0pth  30052  1wlkdlem1  30064  ntrl2v2e  30085  eupth2lem3lem4  30158  ex-fl  30374  ipval2  30634  hlim0  31162  opsqrlem2  32068  iuninc  32487  nndiffz1  32709  fzom1ne1  32724  0dp2dp  32829  cshw1s2  32882  chnub  32938  cycpmco2lem4  33086  1fldgenq  33262  znfermltl  33327  zringfrac  33515  constrextdg2  33729  cos9thpiminplylem5  33766  lmatfvlem  33792  mdetpmtr1  33800  mdetpmtr12  33802  lmlim  33924  qqh0  33961  qqh1  33962  esumfzf  34046  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  esumcvgsum  34065  esumsup  34066  dya2ub  34248  rrvsum  34432  dstfrvclim1  34456  ballotlem2  34467  ballotlemfc0  34471  ballotlemfcc  34472  signsvf0  34558  hgt750leme  34636  subfac1  35146  subfacp1lem1  35147  subfacp1lem2a  35148  subfacp1lem5  35152  subfacp1lem6  35153  cvmliftlem10  35262  divcnvlin  35696  faclimlem1  35706  fwddifnp1  36129  irrdiff  37290  poimirlem3  37593  poimirlem4  37594  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  poimirlem27  37617  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  mblfinlem1  37627  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  fdc  37715  heibor1lem  37779  rrncmslem  37802  lcmfunnnd  41971  lcm1un  41972  lcm2un  41973  lcmineqlem11  41998  lcmineqlem19  42006  aks4d1p1p2  42029  mapfzcons  42686  mzpexpmpt  42715  eldioph3b  42735  fz1eqin  42739  diophin  42742  diophun  42743  0dioph  42748  elnnrabdioph  42777  rabren3dioph  42785  irrapxlem1  42792  irrapxlem3  42794  rmxyadd  42892  rmxy1  42893  rmxy0  42894  rmxp1  42903  rmyp1  42904  rmxm1  42905  rmym1  42906  jm2.24nn  42930  acongeq  42954  jm2.23  42967  jm2.15nn0  42974  jm2.16nn0  42975  jm2.27c  42978  jm2.27dlem2  42981  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  mpaaeu  43121  trclfvdecomr  43699  k0004val0  44125  hashnzfzclim  44294  sumsnd  44998  fmuldfeq  45560  stoweidlem3  45980  stoweidlem20  45997  stoweidlem34  46011  wallispilem4  46045  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem11  46061  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  fourierdlem47  46130  fourierswlem  46207  smfmullem4  46771  ormklocald  46851  natlocalincr  46853  tworepnotupword  46863  ceilhalf1  47311  1oddALTV  47652  1nevenALTV  47653  2evenALTV  47654  nnsum3primes4  47750  nnsum3primesprm  47752  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  tgblthelfgott  47777  stgr1  47921  gpgusgralem  48008  1odd  48094  altgsumbcALT  48276  zlmodzxzsubm  48282  blen2  48513  blennngt2o2  48520  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548