Theorem 1z 12499

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

Syntax hints:   ∈ wcel 2111  1c1 11004  ℤcz 12465

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-addrcl 11064  ax-mulcl 11065  ax-mulrcl 11066  ax-i2m1 11071  ax-1ne0 11072  ax-rrecex 11075  ax-cnre 11076

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-neg 11344  df-nn 12123  df-z 12466

This theorem is referenced by:  1zzd  12500  peano2z  12510  peano2zm  12512  3halfnz  12549  peano5uzti  12560  nnuz  12772  1eluzge0  12775  2eluzge1  12777  eluz2nn  12783  eluz2b1  12814  uz2m1nn  12818  nninf  12824  nnrecq  12867  qbtwnxr  13096  fz1n  13439  fz10  13442  fz01en  13449  fznatpl1  13475  fz12pr  13478  fztpval  13483  fseq1p1m1  13495  elfzp1b  13498  elfzm1b  13499  4fvwrd4  13545  fzo1lb  13610  ige2m2fzo  13625  fz0add1fz1  13632  fzo12sn  13645  fzo13pr  13646  fzo1to4tp  13651  fzofzp1  13661  fzom1ne1  13682  fzostep1  13683  flge1nn  13722  fldiv4p1lem1div2  13736  modid0  13798  nnnfi  13870  fzennn  13872  fzen2  13873  f13idfv  13904  ser1const  13962  exp1  13971  zexpcl  13980  qexpcl  13981  qexpclz  13985  m1expcl  13990  expp1z  14015  expm1  14016  facnn  14179  fac0  14180  fac1  14181  bcn1  14217  bcpasc  14225  bcnm1  14231  hashsng  14273  hashfz  14331  fz1isolem  14365  seqcoll  14368  hashge2el2difr  14385  ccat2s1p2  14535  s2f1o  14820  f1oun2prg  14821  swrd2lsw  14856  2swrd2eqwrdeq  14857  relexp1g  14930  climuni  15456  isercoll2  15573  iseraltlem1  15586  sum0  15625  sumsnf  15647  climcndslem1  15753  climcndslem2  15754  divcnvshft  15759  supcvg  15760  prod0  15847  prodsn  15866  prodsnf  15868  zrisefaccl  15924  zfallfaccl  15925  sin01gt0  16096  rpnnen2lem10  16129  nthruc  16158  iddvds  16177  1dvds  16178  dvdsle  16218  dvds1  16227  3dvds  16239  n2dvds1  16276  divalglem5  16305  divalg  16311  bitsfzolem  16342  gcdcllem1  16407  gcdcllem3  16409  gcdaddmlem  16432  gcdadd  16434  gcdid  16435  gcd1  16436  1gcd  16441  bezoutlem1  16447  nn0rppwr  16469  nn0expgcd  16472  lcmgcdlem  16514  lcm1  16518  3lcm2e6woprm  16523  lcmfunsnlem  16549  isprm3  16591  ge2nprmge4  16609  phicl2  16676  phi1  16681  dfphi2  16682  eulerthlem2  16690  prmdiv  16693  prmdiveq  16694  odzcllem  16701  oddprm  16719  pythagtriplem4  16728  pcpre1  16751  pc1  16764  pcrec  16767  pcmpt  16801  fldivp1  16806  expnprm  16811  pockthlem  16814  unbenlem  16817  prmreclem2  16826  prmrec  16831  igz  16843  4sqlem12  16865  4sqlem13  16866  4sqlem19  16872  vdwlem8  16897  vdwlem13  16902  prmo1  16946  fvprmselgcd1  16954  prmlem0  17014  1259lem4  17042  2503lem2  17046  4001lem1  17049  setsstruct  17084  chnub  18525  gsumpropd2lem  18584  efmnd1hash  18797  mulgfval  18979  mulg1  18991  mulgm1  19004  mulgp1  19017  mulgneg2  19018  cycsubgcl  19116  odinv  19471  efgs1b  19646  lt6abl  19805  pgpfac1lem2  19987  srgbinomlem4  20145  qsubdrg  21354  zsubrg  21355  gzsubrg  21356  zringmulg  21391  zringcyg  21404  mulgrhm  21412  mulgrhm2  21413  pzriprnglem7  21422  pzriprnglem9  21424  pzriprnglem12  21427  pzriprnglem13  21428  pzriprnglem14  21429  pzriprng1ALT  21431  fermltlchr  21464  chrnzr  21465  frgpcyg  21508  zrhpsgnmhm  21519  zrhpsgnodpm  21527  m2detleiblem1  22537  m2detleiblem2  22541  zfbas  23809  imasdsf1olem  24286  cphipval  25168  cmetcaulem  25213  bcthlem5  25253  ehl1eudis  25345  ovolctb  25416  ovolunlem1a  25422  ovolunlem1  25423  ovoliunnul  25433  ovolicc1  25442  ovolicc2lem4  25446  voliunlem1  25476  volsup  25482  uniioombllem6  25514  vitalilem5  25538  plyeq0lem  26140  vieta1lem2  26244  elqaalem2  26253  qaa  26256  iaa  26258  abelthlem6  26371  abelthlem9  26375  sin2pim  26419  cos2pim  26420  logbleb  26718  logblt  26719  1cubrlem  26776  leibpilem2  26876  emcllem5  26935  emcllem7  26937  lgamgulm2  26971  lgamcvglem  26975  gamcvg2lem  26994  lgam1  26999  wilthlem2  27004  wilthlem3  27005  ppip1le  27096  ppi1  27099  cht1  27100  chp1  27102  cht2  27107  ppieq0  27111  ppiub  27140  chpeq0  27144  chpchtsum  27155  chpub  27156  logfacbnd3  27159  logexprlim  27161  bposlem1  27220  bposlem2  27221  bposlem5  27224  bposlem6  27225  lgslem2  27234  lgsfcl2  27239  lgsval2lem  27243  lgsdir2lem1  27261  lgsdir2lem5  27265  1lgs  27276  lgsdchr  27291  lgsquad2lem2  27321  2sqlem9  27363  2sqlem10  27364  2sqblem  27367  2sqb  27368  dchrisumlem3  27427  log2sumbnd  27480  qabvle  27561  ostth3  27574  istrkg3ld  28437  tgldimor  28478  axlowdimlem3  28920  axlowdimlem6  28923  axlowdimlem7  28924  axlowdimlem16  28933  axlowdimlem17  28934  axlowdim  28937  usgrexmpldifpr  29234  dfpth2  29705  uhgrwkspthlem2  29730  pthdlem2  29744  0ewlk  30089  0pth  30100  1wlkdlem1  30112  ntrl2v2e  30133  eupth2lem3lem4  30206  ex-fl  30422  ipval2  30682  hlim0  31210  opsqrlem2  32116  iuninc  32535  nndiffz1  32764  0dp2dp  32884  cshw1s2  32936  cycpmco2lem4  33093  1fldgenq  33283  znfermltl  33326  zringfrac  33514  constrextdg2  33757  cos9thpiminplylem5  33794  lmatfvlem  33823  mdetpmtr1  33831  mdetpmtr12  33833  lmlim  33955  qqh0  33992  qqh1  33993  esumfzf  34077  esumfsup  34078  esumpcvgval  34086  esumcvg  34094  esumcvgsum  34096  esumsup  34097  dya2ub  34278  rrvsum  34462  dstfrvclim1  34486  ballotlem2  34497  ballotlemfc0  34501  ballotlemfcc  34502  signsvf0  34588  hgt750leme  34666  subfac1  35210  subfacp1lem1  35211  subfacp1lem2a  35212  subfacp1lem5  35216  subfacp1lem6  35217  cvmliftlem10  35326  divcnvlin  35765  faclimlem1  35775  fwddifnp1  36198  irrdiff  37359  poimirlem3  37662  poimirlem4  37663  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem24  37683  poimirlem27  37686  poimirlem28  37687  poimirlem31  37690  poimirlem32  37691  mblfinlem1  37696  mblfinlem2  37697  ovoliunnfl  37701  voliunnfl  37703  fdc  37784  heibor1lem  37848  rrncmslem  37871  lcmfunnnd  42044  lcm1un  42045  lcm2un  42046  lcmineqlem11  42071  lcmineqlem19  42079  aks4d1p1p2  42102  mapfzcons  42748  mzpexpmpt  42777  eldioph3b  42797  fz1eqin  42801  diophin  42804  diophun  42805  0dioph  42810  elnnrabdioph  42839  rabren3dioph  42847  irrapxlem1  42854  irrapxlem3  42856  rmxyadd  42953  rmxy1  42954  rmxy0  42955  rmxp1  42964  rmyp1  42965  rmxm1  42966  rmym1  42967  jm2.24nn  42991  acongeq  43015  jm2.23  43028  jm2.15nn0  43035  jm2.16nn0  43036  jm2.27c  43039  jm2.27dlem2  43042  rmydioph  43046  rmxdioph  43048  expdiophlem2  43054  expdioph  43055  mpaaeu  43182  trclfvdecomr  43760  k0004val0  44186  hashnzfzclim  44354  sumsnd  45062  fmuldfeq  45622  stoweidlem3  46040  stoweidlem20  46057  stoweidlem34  46071  wallispilem4  46105  wallispi2lem1  46108  wallispi2lem2  46109  stirlinglem11  46121  dirkerper  46133  dirkertrigeqlem1  46135  dirkertrigeqlem3  46137  fourierdlem47  46190  fourierswlem  46267  smfmullem4  46831  ormklocald  46911  natlocalincr  46913  ceilhalf1  47364  1oddALTV  47720  1nevenALTV  47721  2evenALTV  47722  nnsum3primes4  47818  nnsum3primesprm  47820  nnsum3primesgbe  47822  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  tgblthelfgott  47845  stgr1  47991  gpgusgralem  48086  1odd  48201  altgsumbcALT  48383  zlmodzxzsubm  48389  blen2  48616  blennngt2o2  48623  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651