Theorem 1z 12756

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

This proof depends on syntax axioms:   ∈ wcel 2147  1c1 11231  ℤcz 12723

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-i2m1 11298  ax-1ne0 11299  ax-rrecex 11302  ax-cnre 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-neg 11574  df-nn 12366  df-z 12724

This theorem is used by:  1zzd  12757  peano2z  12767  peano2zm  12769  3halfnz  12808  peano5uzti  12819  nnuz  13034  1eluzge0  13037  2eluzge1  13039  eluz2nn  13045  eluz2b1  13076  uz2m1nn  13080  nninf  13086  1q  13122  nnrecq  13130  qbtwnxr  13360  fz1n  13705  fz10  13708  fz01en  13716  fznatpl1  13742  fz12pr  13745  fztpval  13750  fseq1p1m1  13762  elfzp1b  13765  elfzm1b  13766  4fvwrd4  13812  fzo1lb  13878  ige2m2fzo  13893  fz0add1fz1  13900  fzo12sn  13913  fzo13pr  13914  fzo1to4tp  13919  fzofzp1  13929  fzom1ne1  13950  fzostep1  13951  flge1nn  13991  fldiv4p1lem1div2  14005  modid0  14067  nnnfi  14139  fzennn  14141  fzen2  14142  f13idfv  14173  ser1const  14231  exp1  14240  zexpcl  14249  qexpclz  14254  m1expcl  14259  expp1z  14284  expm1  14285  facnn  14449  fac0  14450  fac1  14451  bcn1  14487  bcpasc  14495  bcnm1  14501  hashsng  14543  hashfz  14602  fz1isolem  14636  seqcoll  14639  hashge2el2difr  14656  ccat2s1p2  14809  s2f1o  15099  f1oun2prg  15100  swrd2lsw  15137  2swrd2eqwrdeq  15138  relexp1g  15211  climuni  15751  isercoll2  15868  iseraltlem1  15881  sum0  15919  sumsnf  15941  climcndslem1  16050  climcndslem2  16051  divcnvshft  16056  supcvg  16057  prod0  16142  prodsn  16161  prodsnf  16163  zrisefaccl  16219  zfallfaccl  16220  sin01gt0  16390  rpnnen2lem10  16423  nthruc  16452  iddvds  16471  1dvds  16472  dvdsle  16512  dvds1  16521  3dvds  16533  n2dvds1  16570  divalglem5  16599  divalg  16605  bitsfzolem  16636  gcdcllem1  16701  gcdcllem3  16703  gcdaddmlem  16728  gcdadd  16730  gcdid  16731  gcd1  16733  1gcd  16738  bezoutlem1  16744  nn0rppwr  16767  nn0expgcd  16770  lcmgcdlem  16813  lcm1  16817  3lcm2e6woprm  16822  lcmfunsnlem  16848  isprm3  16890  ge2nprmge4  16909  phicl2  16977  phi1  16982  dfphi2  16983  eulerthlem2  16991  prmdiv  16994  prmdiveq  16995  odzcllem  17002  oddprm  17020  pythagtriplem4  17029  pcpre1  17052  pc1  17065  pcrec  17068  pcmpt  17102  fldivp1  17107  expnprm  17112  pockthlem  17115  unbenlem  17118  prmreclem2  17127  prmrec  17132  igz  17144  4sqlem12  17166  4sqlem13  17167  4sqlem19  17173  vdwlem8  17198  vdwlem13  17203  prmo1  17247  fvprmselgcd1  17255  prmlem0  17315  1259lem4  17344  2503lem2  17348  4001lem1  17351  setsstruct  17386  chnub  18828  gsumpropd2lem  18900  efmnd1hash  19120  mulgfval  19311  mulg1  19323  mulgm1  19336  mulgp1  19349  mulgneg2  19350  cycsubgcl  19453  odinv  19808  efgs1b  19983  lt6abl  20142  pgpfac1lem2  20324  srgbinomlem4  20488  qsubdrg  21758  zsubrg  21759  gzsubrg  21760  zringmulg  21795  zringcyg  21808  mulgrhm  21816  mulgrhm2  21817  pzriprnglem7  21826  pzriprnglem9  21828  pzriprnglem12  21831  pzriprnglem13  21832  pzriprnglem14  21833  pzriprng1ALT  21835  fermltlchr  21868  chrnzr  21869  frgpcyg  21912  zrhpsgnmhm  21923  zrhpsgnodpm  21931  m2detleiblem1  22972  m2detleiblem2  22976  zfbas  24248  imasdsf1olem  24725  cphipval  25597  cmetcaulem  25642  bcthlem5  25682  ovolctb  25844  ovolunlem1a  25850  ovolunlem1  25851  ovoliunnul  25861  ovolicc1  25870  ovolicc2lem4  25874  voliunlem1  25904  volsup  25910  uniioombllem6  25942  vitalilem5  25966  plyeq0lem  26562  vieta1lem2  26667  elqaalem2  26676  1aa  26683  iaaOLD  26685  abelthlem6  26796  abelthlem9  26800  sin2pim  26847  cos2pim  26848  logbleb  27144  logblt  27145  1cubrlem  27202  leibpilem2  27302  emcllem5  27360  emcllem7  27362  lgamgulm2  27396  lgamcvglem  27400  gamcvg2lem  27419  lgam1  27424  wilthlem2  27429  wilthlem3  27430  ppip1le  27521  ppi1  27524  cht1  27525  chp1  27527  cht2  27532  ppieq0  27536  ppiub  27564  chpeq0  27568  chpchtsum  27579  chpub  27580  logfacbnd3  27583  logexprlim  27585  bposlem1  27644  bposlem2  27645  bposlem5  27648  bposlem6  27649  lgslem2  27658  lgsfcl2  27663  lgsval2lem  27667  lgsdir2lem1  27685  lgsdir2lem5  27689  1lgs  27700  lgsdchr  27715  lgsquad2lem2  27745  2sqlem9  27787  2sqlem10  27788  2sqblem  27791  2sqb  27792  dchrisumlem3  27851  log2sumbnd  27904  qabvle  27985  ostth3  27998  istrkg3ld  28956  tgldimor  28998  axlowdimlem3  29555  axlowdimlem6  29558  axlowdimlem7  29559  axlowdimlem16  29568  axlowdimlem17  29569  axlowdim  29572  usgrexmpldifpr  29872  dfpth2  30347  uhgrwkspthlem2  30373  pthdlem2  30387  0ewlk  30738  0pth  30749  1wlkdlem1  30761  ntrl2v2e  30792  eupth2lem3lem4  30865  ex-fl  31081  ipval2  31342  hlim0  31870  opsqrlem2  32776  iuninc  33230  nndiffz1  33451  0dp2dp  33548  cshw1s2  33594  cycpmco2lem4  33766  1fldgenq  33968  znfermltl  34006  zringfrac  34169  constrextdg2  34464  cos9thpiminplylem5  34501  lmatfvlem  34530  mdetpmtr1  34538  mdetpmtr12  34540  lmlim  34662  qqh0  34699  qqh1  34700  esumfzf  34784  esumfsup  34785  esumpcvgval  34793  esumcvg  34801  esumcvgsum  34803  esumsup  34804  dya2ub  34985  rrvsum  35169  dstfrvclim1  35193  ballotlem2  35204  ballotlemfc0  35208  ballotlemfcc  35209  signsvf0  35292  hgt750leme  35370  subfac1  36123  subfacp1lem1  36124  subfacp1lem2a  36125  subfacp1lem5  36129  subfacp1lem6  36130  cvmliftlem10  36239  divcnvlin  36689  faclimlem1  36699  fwddifnp1  37121  irrdiff  38452  qdiff  38453  poimirlem3  38746  poimirlem4  38747  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem24  38767  poimirlem27  38770  poimirlem28  38771  poimirlem31  38774  poimirlem32  38775  mblfinlem1  38780  mblfinlem2  38781  ovoliunnfl  38785  voliunnfl  38787  fdc  38882  heibor1lem  38946  rrncmslem  38969  lcmfunnnd  43265  lcm1un  43266  lcm2un  43267  lcmineqlem11  43292  lcmineqlem19  43300  aks4d1p1p2  43323  mapfzcons  43931  mzpexpmpt  43960  eldioph3b  43980  fz1eqin  43984  diophin  43987  diophun  43988  0dioph  43993  elnnrabdioph  44018  rabren3dioph  44026  irrapxlem1  44033  irrapxlem3  44035  rmxyadd  44132  rmxy1  44133  rmxy0  44134  rmxp1  44143  rmyp1  44144  rmxm1  44145  rmym1  44146  jm2.24nn  44170  acongeq  44194  jm2.23  44207  jm2.15nn0  44214  jm2.16nn0  44215  jm2.27c  44218  jm2.27dlem2  44221  rmydioph  44225  rmxdioph  44227  expdiophlem2  44233  expdioph  44234  mpaaeu  44355  trclfvdecomr  44931  k0004val0  45357  hashnzfzclim  45509  sumsnd  46259  fmuldfeq  46810  stoweidlem3  47228  stoweidlem20  47245  stoweidlem34  47259  wallispilem4  47293  wallispi2lem1  47296  wallispi2lem2  47297  stirlinglem11  47309  dirkerper  47321  dirkertrigeqlem1  47323  dirkertrigeqlem3  47325  fourierdlem47  47378  fourierswlem  47455  smfmullem4  48019  ormklocald  48101  sqrtnnaa  48128  sqrtnzqaa  48129  ceilhalf1  48623  nprmdvdsfacm1lem4  48923  ppivalnnprm  48925  ppivalnn  48932  1oddALTV  49003  1nevenALTV  49004  2evenALTV  49005  nnsum3primes4  49101  nnsum3primesprm  49103  nnsum3primesgbe  49105  nnsum4primesodd  49109  nnsum4primesoddALTV  49110  nnsum4primeseven  49113  nnsum4primesevenALTV  49114  tgblthelfgott  49128  stgr1  49274  gpgusgralem  49369  1odd  49483  altgsumbcALT  49680  zlmodzxzsubm  49686  blen2  49912  blennngt2o2  49919  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947  crosspdotsumlem  51276  crosspaltd  51278  crossp3d  51279  veroquadgsumlem  51295