Theorem 1z 12508

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

Syntax hints:   ∈ wcel 2113  1c1 11014  ℤcz 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  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 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11354  df-nn 12133  df-z 12476

This theorem is referenced by:  1zzd  12509  peano2z  12519  peano2zm  12521  3halfnz  12558  peano5uzti  12569  nnuz  12777  1eluzge0  12780  2eluzge1  12782  eluz2nn  12788  eluz2b1  12819  uz2m1nn  12823  nninf  12829  nnrecq  12872  qbtwnxr  13101  fz1n  13444  fz10  13447  fz01en  13454  fznatpl1  13480  fz12pr  13483  fztpval  13488  fseq1p1m1  13500  elfzp1b  13503  elfzm1b  13504  4fvwrd4  13550  fzo1lb  13615  ige2m2fzo  13630  fz0add1fz1  13637  fzo12sn  13650  fzo13pr  13651  fzo1to4tp  13656  fzofzp1  13666  fzom1ne1  13687  fzostep1  13688  flge1nn  13727  fldiv4p1lem1div2  13741  modid0  13803  nnnfi  13875  fzennn  13877  fzen2  13878  f13idfv  13909  ser1const  13967  exp1  13976  zexpcl  13985  qexpcl  13986  qexpclz  13990  m1expcl  13995  expp1z  14020  expm1  14021  facnn  14184  fac0  14185  fac1  14186  bcn1  14222  bcpasc  14230  bcnm1  14236  hashsng  14278  hashfz  14336  fz1isolem  14370  seqcoll  14373  hashge2el2difr  14390  ccat2s1p2  14540  s2f1o  14825  f1oun2prg  14826  swrd2lsw  14861  2swrd2eqwrdeq  14862  relexp1g  14935  climuni  15461  isercoll2  15578  iseraltlem1  15591  sum0  15630  sumsnf  15652  climcndslem1  15758  climcndslem2  15759  divcnvshft  15764  supcvg  15765  prod0  15852  prodsn  15871  prodsnf  15873  zrisefaccl  15929  zfallfaccl  15930  sin01gt0  16101  rpnnen2lem10  16134  nthruc  16163  iddvds  16182  1dvds  16183  dvdsle  16223  dvds1  16232  3dvds  16244  n2dvds1  16281  divalglem5  16310  divalg  16316  bitsfzolem  16347  gcdcllem1  16412  gcdcllem3  16414  gcdaddmlem  16437  gcdadd  16439  gcdid  16440  gcd1  16441  1gcd  16446  bezoutlem1  16452  nn0rppwr  16474  nn0expgcd  16477  lcmgcdlem  16519  lcm1  16523  3lcm2e6woprm  16528  lcmfunsnlem  16554  isprm3  16596  ge2nprmge4  16614  phicl2  16681  phi1  16686  dfphi2  16687  eulerthlem2  16695  prmdiv  16698  prmdiveq  16699  odzcllem  16706  oddprm  16724  pythagtriplem4  16733  pcpre1  16756  pc1  16769  pcrec  16772  pcmpt  16806  fldivp1  16811  expnprm  16816  pockthlem  16819  unbenlem  16822  prmreclem2  16831  prmrec  16836  igz  16848  4sqlem12  16870  4sqlem13  16871  4sqlem19  16877  vdwlem8  16902  vdwlem13  16907  prmo1  16951  fvprmselgcd1  16959  prmlem0  17019  1259lem4  17047  2503lem2  17051  4001lem1  17054  setsstruct  17089  chnub  18530  gsumpropd2lem  18589  efmnd1hash  18802  mulgfval  18984  mulg1  18996  mulgm1  19009  mulgp1  19022  mulgneg2  19023  cycsubgcl  19120  odinv  19475  efgs1b  19650  lt6abl  19809  pgpfac1lem2  19991  srgbinomlem4  20149  qsubdrg  21358  zsubrg  21359  gzsubrg  21360  zringmulg  21395  zringcyg  21408  mulgrhm  21416  mulgrhm2  21417  pzriprnglem7  21426  pzriprnglem9  21428  pzriprnglem12  21431  pzriprnglem13  21432  pzriprnglem14  21433  pzriprng1ALT  21435  fermltlchr  21468  chrnzr  21469  frgpcyg  21512  zrhpsgnmhm  21523  zrhpsgnodpm  21531  m2detleiblem1  22540  m2detleiblem2  22544  zfbas  23812  imasdsf1olem  24289  cphipval  25171  cmetcaulem  25216  bcthlem5  25256  ehl1eudis  25348  ovolctb  25419  ovolunlem1a  25425  ovolunlem1  25426  ovoliunnul  25436  ovolicc1  25445  ovolicc2lem4  25449  voliunlem1  25479  volsup  25485  uniioombllem6  25517  vitalilem5  25541  plyeq0lem  26143  vieta1lem2  26247  elqaalem2  26256  qaa  26259  iaa  26261  abelthlem6  26374  abelthlem9  26378  sin2pim  26422  cos2pim  26423  logbleb  26721  logblt  26722  1cubrlem  26779  leibpilem2  26879  emcllem5  26938  emcllem7  26940  lgamgulm2  26974  lgamcvglem  26978  gamcvg2lem  26997  lgam1  27002  wilthlem2  27007  wilthlem3  27008  ppip1le  27099  ppi1  27102  cht1  27103  chp1  27105  cht2  27110  ppieq0  27114  ppiub  27143  chpeq0  27147  chpchtsum  27158  chpub  27159  logfacbnd3  27162  logexprlim  27164  bposlem1  27223  bposlem2  27224  bposlem5  27227  bposlem6  27228  lgslem2  27237  lgsfcl2  27242  lgsval2lem  27246  lgsdir2lem1  27264  lgsdir2lem5  27268  1lgs  27279  lgsdchr  27294  lgsquad2lem2  27324  2sqlem9  27366  2sqlem10  27367  2sqblem  27370  2sqb  27371  dchrisumlem3  27430  log2sumbnd  27483  qabvle  27564  ostth3  27577  istrkg3ld  28440  tgldimor  28481  axlowdimlem3  28924  axlowdimlem6  28927  axlowdimlem7  28928  axlowdimlem16  28937  axlowdimlem17  28938  axlowdim  28941  usgrexmpldifpr  29238  dfpth2  29709  uhgrwkspthlem2  29734  pthdlem2  29748  0ewlk  30096  0pth  30107  1wlkdlem1  30119  ntrl2v2e  30140  eupth2lem3lem4  30213  ex-fl  30429  ipval2  30689  hlim0  31217  opsqrlem2  32123  iuninc  32542  nndiffz1  32773  0dp2dp  32896  cshw1s2  32948  cycpmco2lem4  33105  1fldgenq  33295  znfermltl  33338  zringfrac  33526  constrextdg2  33783  cos9thpiminplylem5  33820  lmatfvlem  33849  mdetpmtr1  33857  mdetpmtr12  33859  lmlim  33981  qqh0  34018  qqh1  34019  esumfzf  34103  esumfsup  34104  esumpcvgval  34112  esumcvg  34120  esumcvgsum  34122  esumsup  34123  dya2ub  34304  rrvsum  34488  dstfrvclim1  34512  ballotlem2  34523  ballotlemfc0  34527  ballotlemfcc  34528  signsvf0  34614  hgt750leme  34692  subfac1  35243  subfacp1lem1  35244  subfacp1lem2a  35245  subfacp1lem5  35249  subfacp1lem6  35250  cvmliftlem10  35359  divcnvlin  35798  faclimlem1  35808  fwddifnp1  36230  irrdiff  37391  poimirlem3  37683  poimirlem4  37684  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem24  37704  poimirlem27  37707  poimirlem28  37708  poimirlem31  37711  poimirlem32  37712  mblfinlem1  37717  mblfinlem2  37718  ovoliunnfl  37722  voliunnfl  37724  fdc  37805  heibor1lem  37869  rrncmslem  37892  lcmfunnnd  42125  lcm1un  42126  lcm2un  42127  lcmineqlem11  42152  lcmineqlem19  42160  aks4d1p1p2  42183  mapfzcons  42833  mzpexpmpt  42862  eldioph3b  42882  fz1eqin  42886  diophin  42889  diophun  42890  0dioph  42895  elnnrabdioph  42924  rabren3dioph  42932  irrapxlem1  42939  irrapxlem3  42941  rmxyadd  43038  rmxy1  43039  rmxy0  43040  rmxp1  43049  rmyp1  43050  rmxm1  43051  rmym1  43052  jm2.24nn  43076  acongeq  43100  jm2.23  43113  jm2.15nn0  43120  jm2.16nn0  43121  jm2.27c  43124  jm2.27dlem2  43127  rmydioph  43131  rmxdioph  43133  expdiophlem2  43139  expdioph  43140  mpaaeu  43267  trclfvdecomr  43845  k0004val0  44271  hashnzfzclim  44439  sumsnd  45147  fmuldfeq  45707  stoweidlem3  46125  stoweidlem20  46142  stoweidlem34  46156  wallispilem4  46190  wallispi2lem1  46193  wallispi2lem2  46194  stirlinglem11  46206  dirkerper  46218  dirkertrigeqlem1  46220  dirkertrigeqlem3  46222  fourierdlem47  46275  fourierswlem  46352  smfmullem4  46916  ormklocald  46996  natlocalincr  46998  nthrucw  47008  ceilhalf1  47458  1oddALTV  47814  1nevenALTV  47815  2evenALTV  47816  nnsum3primes4  47912  nnsum3primesprm  47914  nnsum3primesgbe  47916  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  tgblthelfgott  47939  stgr1  48085  gpgusgralem  48180  1odd  48295  altgsumbcALT  48477  zlmodzxzsubm  48483  blen2  48710  blennngt2o2  48717  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745