Theorem 1z 12598

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

Syntax hints:   ∈ wcel 2141  1c1 11071  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-neg 11414  df-nn 12208  df-z 12566

This theorem is referenced by:  1zzd  12599  peano2z  12609  peano2zm  12611  3halfnz  12649  peano5uzti  12660  nnuz  12875  1eluzge0  12878  2eluzge1  12880  eluz2nn  12886  eluz2b1  12917  uz2m1nn  12921  nninf  12927  nnrecq  12970  qbtwnxr  13200  fz1n  13544  fz10  13547  fz01en  13554  fznatpl1  13580  fz12pr  13583  fztpval  13588  fseq1p1m1  13600  elfzp1b  13603  elfzm1b  13604  4fvwrd4  13650  fzo1lb  13716  ige2m2fzo  13731  fz0add1fz1  13738  fzo12sn  13751  fzo13pr  13752  fzo1to4tp  13757  fzofzp1  13767  fzom1ne1  13788  fzostep1  13789  flge1nn  13828  fldiv4p1lem1div2  13842  modid0  13904  nnnfi  13976  fzennn  13978  fzen2  13979  f13idfv  14010  ser1const  14068  exp1  14077  zexpcl  14086  qexpcl  14087  qexpclz  14091  m1expcl  14096  expp1z  14121  expm1  14122  facnn  14285  fac0  14286  fac1  14287  bcn1  14323  bcpasc  14331  bcnm1  14337  hashsng  14379  hashfz  14437  fz1isolem  14471  seqcoll  14474  hashge2el2difr  14491  ccat2s1p2  14641  s2f1o  14926  f1oun2prg  14927  swrd2lsw  14962  2swrd2eqwrdeq  14963  relexp1g  15036  climuni  15562  isercoll2  15679  iseraltlem1  15692  sum0  15731  sumsnf  15753  climcndslem1  15862  climcndslem2  15863  divcnvshft  15868  supcvg  15869  prod0  15956  prodsn  15975  prodsnf  15977  zrisefaccl  16033  zfallfaccl  16034  sin01gt0  16205  rpnnen2lem10  16238  nthruc  16267  iddvds  16286  1dvds  16287  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  16719  phicl2  16786  phi1  16791  dfphi2  16792  eulerthlem2  16800  prmdiv  16803  prmdiveq  16804  odzcllem  16811  oddprm  16829  pythagtriplem4  16838  pcpre1  16861  pc1  16874  pcrec  16877  pcmpt  16911  fldivp1  16916  expnprm  16921  pockthlem  16924  unbenlem  16927  prmreclem2  16936  prmrec  16941  igz  16953  4sqlem12  16975  4sqlem13  16976  4sqlem19  16982  vdwlem8  17007  vdwlem13  17012  prmo1  17056  fvprmselgcd1  17064  prmlem0  17124  1259lem4  17153  2503lem2  17157  4001lem1  17160  setsstruct  17195  chnub  18637  gsumpropd2lem  18696  efmnd1hash  18909  mulgfval  19094  mulg1  19106  mulgm1  19119  mulgp1  19132  mulgneg2  19133  cycsubgcl  19230  odinv  19584  efgs1b  19759  lt6abl  19918  pgpfac1lem2  20100  srgbinomlem4  20258  qsubdrg  21451  zsubrg  21452  gzsubrg  21453  zringmulg  21488  zringcyg  21501  mulgrhm  21509  mulgrhm2  21510  pzriprnglem7  21519  pzriprnglem9  21521  pzriprnglem12  21524  pzriprnglem13  21525  pzriprnglem14  21526  pzriprng1ALT  21528  fermltlchr  21561  chrnzr  21562  frgpcyg  21605  zrhpsgnmhm  21616  zrhpsgnodpm  21624  m2detleiblem1  22664  m2detleiblem2  22668  zfbas  23936  imasdsf1olem  24413  cphipval  25285  cmetcaulem  25330  bcthlem5  25370  ehl1eudis  25462  ovolctb  25532  ovolunlem1a  25538  ovolunlem1  25539  ovoliunnul  25549  ovolicc1  25558  ovolicc2lem4  25562  voliunlem1  25592  volsup  25598  uniioombllem6  25630  vitalilem5  25654  plyeq0lem  26250  vieta1lem2  26352  elqaalem2  26361  qaa  26364  iaa  26366  abelthlem6  26476  abelthlem9  26480  sin2pim  26527  cos2pim  26528  logbleb  26825  logblt  26826  1cubrlem  26883  leibpilem2  26983  emcllem5  27041  emcllem7  27043  lgamgulm2  27077  lgamcvglem  27081  gamcvg2lem  27100  lgam1  27105  wilthlem2  27110  wilthlem3  27111  ppip1le  27202  ppi1  27205  cht1  27206  chp1  27208  cht2  27213  ppieq0  27217  ppiub  27245  chpeq0  27249  chpchtsum  27260  chpub  27261  logfacbnd3  27264  logexprlim  27266  bposlem1  27325  bposlem2  27326  bposlem5  27329  bposlem6  27330  lgslem2  27339  lgsfcl2  27344  lgsval2lem  27348  lgsdir2lem1  27366  lgsdir2lem5  27370  1lgs  27381  lgsdchr  27396  lgsquad2lem2  27426  2sqlem9  27468  2sqlem10  27469  2sqblem  27472  2sqb  27473  dchrisumlem3  27532  log2sumbnd  27585  qabvle  27666  ostth3  27679  istrkg3ld  28607  tgldimor  28648  axlowdimlem3  29091  axlowdimlem6  29094  axlowdimlem7  29095  axlowdimlem16  29104  axlowdimlem17  29105  axlowdim  29108  usgrexmpldifpr  29405  dfpth2  29875  uhgrwkspthlem2  29900  pthdlem2  29914  0ewlk  30262  0pth  30273  1wlkdlem1  30285  ntrl2v2e  30306  eupth2lem3lem4  30379  ex-fl  30595  ipval2  30856  hlim0  31384  opsqrlem2  32290  iuninc  32709  nndiffz1  32938  0dp2dp  33047  cshw1s2  33099  cycpmco2lem4  33270  1fldgenq  33470  znfermltl  33513  zringfrac  33711  constrextdg2  34007  cos9thpiminplylem5  34044  lmatfvlem  34073  mdetpmtr1  34081  mdetpmtr12  34083  lmlim  34205  qqh0  34242  qqh1  34243  esumfzf  34327  esumfsup  34328  esumpcvgval  34336  esumcvg  34344  esumcvgsum  34346  esumsup  34347  dya2ub  34528  rrvsum  34712  dstfrvclim1  34736  ballotlem2  34747  ballotlemfc0  34751  ballotlemfcc  34752  signsvf0  34838  hgt750leme  34916  subfac1  35492  subfacp1lem1  35493  subfacp1lem2a  35494  subfacp1lem5  35498  subfacp1lem6  35499  cvmliftlem10  35608  divcnvlin  36047  faclimlem1  36057  fwddifnp1  36479  irrdiff  37782  qdiff  37783  poimirlem3  38086  poimirlem4  38087  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem24  38107  poimirlem27  38110  poimirlem28  38111  poimirlem31  38114  poimirlem32  38115  mblfinlem1  38120  mblfinlem2  38121  ovoliunnfl  38125  voliunnfl  38127  fdc  38208  heibor1lem  38272  rrncmslem  38295  lcmfunnnd  42593  lcm1un  42594  lcm2un  42595  lcmineqlem11  42620  lcmineqlem19  42628  aks4d1p1p2  42651  mapfzcons  43261  mzpexpmpt  43290  eldioph3b  43310  fz1eqin  43314  diophin  43317  diophun  43318  0dioph  43323  elnnrabdioph  43348  rabren3dioph  43356  irrapxlem1  43363  irrapxlem3  43365  rmxyadd  43462  rmxy1  43463  rmxy0  43464  rmxp1  43473  rmyp1  43474  rmxm1  43475  rmym1  43476  jm2.24nn  43500  acongeq  43524  jm2.23  43537  jm2.15nn0  43544  jm2.16nn0  43545  jm2.27c  43548  jm2.27dlem2  43551  rmydioph  43555  rmxdioph  43557  expdiophlem2  43563  expdioph  43564  mpaaeu  43691  trclfvdecomr  44268  k0004val0  44694  hashnzfzclim  44862  sumsnd  45570  fmuldfeq  46123  stoweidlem3  46541  stoweidlem20  46558  stoweidlem34  46572  wallispilem4  46606  wallispi2lem1  46609  wallispi2lem2  46610  stirlinglem11  46622  dirkerper  46634  dirkertrigeqlem1  46636  dirkertrigeqlem3  46638  fourierdlem47  46691  fourierswlem  46768  smfmullem4  47332  ormklocald  47414  natlocalincr  47416  nthrucw  47426  ceilhalf1  47896  nprmdvdsfacm1lem4  48196  ppivalnnprm  48198  ppivalnn  48205  1oddALTV  48276  1nevenALTV  48277  2evenALTV  48278  nnsum3primes4  48374  nnsum3primesprm  48376  nnsum3primesgbe  48378  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  tgblthelfgott  48401  stgr1  48547  gpgusgralem  48642  1odd  48757  altgsumbcALT  48939  zlmodzxzsubm  48945  blen2  49171  blennngt2o2  49178  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206