Theorem 1z 12625

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

Syntax hints:   ∈ wcel 2143  1c1 11102  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-neg 11445  df-nn 12235  df-z 12593

This theorem is referenced by:  1zzd  12626  peano2z  12636  peano2zm  12638  3halfnz  12676  peano5uzti  12687  nnuz  12902  1eluzge0  12905  2eluzge1  12907  eluz2nn  12913  eluz2b1  12944  uz2m1nn  12948  nninf  12954  nnrecq  12997  qbtwnxr  13227  fz1n  13571  fz10  13574  fz01en  13582  fznatpl1  13608  fz12pr  13611  fztpval  13616  fseq1p1m1  13628  elfzp1b  13631  elfzm1b  13632  4fvwrd4  13678  fzo1lb  13744  ige2m2fzo  13759  fz0add1fz1  13766  fzo12sn  13779  fzo13pr  13780  fzo1to4tp  13785  fzofzp1  13795  fzom1ne1  13816  fzostep1  13817  flge1nn  13856  fldiv4p1lem1div2  13870  modid0  13932  nnnfi  14004  fzennn  14006  fzen2  14007  f13idfv  14038  ser1const  14096  exp1  14105  zexpcl  14114  qexpcl  14115  qexpclz  14119  m1expcl  14124  expp1z  14149  expm1  14150  facnn  14313  fac0  14314  fac1  14315  bcn1  14351  bcpasc  14359  bcnm1  14365  hashsng  14407  hashfz  14466  fz1isolem  14500  seqcoll  14503  hashge2el2difr  14520  ccat2s1p2  14670  s2f1o  14955  f1oun2prg  14956  swrd2lsw  14991  2swrd2eqwrdeq  14992  relexp1g  15065  climuni  15605  isercoll2  15722  iseraltlem1  15735  sum0  15774  sumsnf  15796  climcndslem1  15905  climcndslem2  15906  divcnvshft  15911  supcvg  15912  prod0  15999  prodsn  16018  prodsnf  16020  zrisefaccl  16076  zfallfaccl  16077  sin01gt0  16247  rpnnen2lem10  16280  nthruc  16309  iddvds  16328  1dvds  16329  dvdsle  16369  dvds1  16378  3dvds  16390  n2dvds1  16427  divalglem5  16456  divalg  16462  bitsfzolem  16493  gcdcllem1  16558  gcdcllem3  16560  gcdaddmlem  16583  gcdadd  16585  gcdid  16586  gcd1  16587  1gcd  16592  bezoutlem1  16598  nn0rppwr  16620  nn0expgcd  16623  lcmgcdlem  16665  lcm1  16669  3lcm2e6woprm  16674  lcmfunsnlem  16700  isprm3  16742  ge2nprmge4  16761  phicl2  16828  phi1  16833  dfphi2  16834  eulerthlem2  16842  prmdiv  16845  prmdiveq  16846  odzcllem  16853  oddprm  16871  pythagtriplem4  16880  pcpre1  16903  pc1  16916  pcrec  16919  pcmpt  16953  fldivp1  16958  expnprm  16963  pockthlem  16966  unbenlem  16969  prmreclem2  16978  prmrec  16983  igz  16995  4sqlem12  17017  4sqlem13  17018  4sqlem19  17024  vdwlem8  17049  vdwlem13  17054  prmo1  17098  fvprmselgcd1  17106  prmlem0  17166  1259lem4  17195  2503lem2  17199  4001lem1  17202  setsstruct  17237  chnub  18679  gsumpropd2lem  18738  efmnd1hash  18952  mulgfval  19136  mulg1  19148  mulgm1  19161  mulgp1  19174  mulgneg2  19175  cycsubgcl  19278  odinv  19632  efgs1b  19807  lt6abl  19966  pgpfac1lem2  20148  srgbinomlem4  20312  qsubdrg  21550  zsubrg  21551  gzsubrg  21552  zringmulg  21587  zringcyg  21600  mulgrhm  21608  mulgrhm2  21609  pzriprnglem7  21618  pzriprnglem9  21620  pzriprnglem12  21623  pzriprnglem13  21624  pzriprnglem14  21625  pzriprng1ALT  21627  fermltlchr  21660  chrnzr  21661  frgpcyg  21704  zrhpsgnmhm  21715  zrhpsgnodpm  21723  m2detleiblem1  22762  m2detleiblem2  22766  zfbas  24034  imasdsf1olem  24511  cphipval  25383  cmetcaulem  25428  bcthlem5  25468  ehl1eudis  25560  ovolctb  25630  ovolunlem1a  25636  ovolunlem1  25637  ovoliunnul  25647  ovolicc1  25656  ovolicc2lem4  25660  voliunlem1  25690  volsup  25696  uniioombllem6  25728  vitalilem5  25752  plyeq0lem  26348  vieta1lem2  26453  elqaalem2  26462  qaa  26465  iaa  26467  abelthlem6  26577  abelthlem9  26581  sin2pim  26628  cos2pim  26629  logbleb  26926  logblt  26927  1cubrlem  26984  leibpilem2  27084  emcllem5  27142  emcllem7  27144  lgamgulm2  27178  lgamcvglem  27182  gamcvg2lem  27201  lgam1  27206  wilthlem2  27211  wilthlem3  27212  ppip1le  27303  ppi1  27306  cht1  27307  chp1  27309  cht2  27314  ppieq0  27318  ppiub  27346  chpeq0  27350  chpchtsum  27361  chpub  27362  logfacbnd3  27365  logexprlim  27367  bposlem1  27426  bposlem2  27427  bposlem5  27430  bposlem6  27431  lgslem2  27440  lgsfcl2  27445  lgsval2lem  27449  lgsdir2lem1  27467  lgsdir2lem5  27471  1lgs  27482  lgsdchr  27497  lgsquad2lem2  27527  2sqlem9  27569  2sqlem10  27570  2sqblem  27573  2sqb  27574  dchrisumlem3  27633  log2sumbnd  27686  qabvle  27767  ostth3  27780  istrkg3ld  28708  tgldimor  28749  axlowdimlem3  29272  axlowdimlem6  29275  axlowdimlem7  29276  axlowdimlem16  29285  axlowdimlem17  29286  axlowdim  29289  usgrexmpldifpr  29586  dfpth2  30056  uhgrwkspthlem2  30081  pthdlem2  30095  0ewlk  30443  0pth  30454  1wlkdlem1  30466  ntrl2v2e  30487  eupth2lem3lem4  30560  ex-fl  30776  ipval2  31037  hlim0  31565  opsqrlem2  32471  iuninc  32883  nndiffz1  33109  0dp2dp  33206  cshw1s2  33258  cycpmco2lem4  33427  1fldgenq  33621  znfermltl  33659  zringfrac  33822  constrextdg2  34117  cos9thpiminplylem5  34154  lmatfvlem  34183  mdetpmtr1  34191  mdetpmtr12  34193  lmlim  34315  qqh0  34352  qqh1  34353  esumfzf  34437  esumfsup  34438  esumpcvgval  34446  esumcvg  34454  esumcvgsum  34456  esumsup  34457  dya2ub  34638  rrvsum  34822  dstfrvclim1  34846  ballotlem2  34857  ballotlemfc0  34861  ballotlemfcc  34862  signsvf0  34945  hgt750leme  35023  subfac1  35648  subfacp1lem1  35649  subfacp1lem2a  35650  subfacp1lem5  35654  subfacp1lem6  35655  cvmliftlem10  35764  divcnvlin  36203  faclimlem1  36213  fwddifnp1  36635  irrdiff  37948  qdiff  37949  poimirlem3  38252  poimirlem4  38253  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem24  38273  poimirlem27  38276  poimirlem28  38277  poimirlem31  38280  poimirlem32  38281  mblfinlem1  38286  mblfinlem2  38287  ovoliunnfl  38291  voliunnfl  38293  fdc  38374  heibor1lem  38438  rrncmslem  38461  lcmfunnnd  42757  lcm1un  42758  lcm2un  42759  lcmineqlem11  42784  lcmineqlem19  42792  aks4d1p1p2  42815  mapfzcons  43427  mzpexpmpt  43456  eldioph3b  43476  fz1eqin  43480  diophin  43483  diophun  43484  0dioph  43489  elnnrabdioph  43514  rabren3dioph  43522  irrapxlem1  43529  irrapxlem3  43531  rmxyadd  43628  rmxy1  43629  rmxy0  43630  rmxp1  43639  rmyp1  43640  rmxm1  43641  rmym1  43642  jm2.24nn  43666  acongeq  43690  jm2.23  43703  jm2.15nn0  43710  jm2.16nn0  43711  jm2.27c  43714  jm2.27dlem2  43717  rmydioph  43721  rmxdioph  43723  expdiophlem2  43729  expdioph  43730  mpaaeu  43857  trclfvdecomr  44434  k0004val0  44860  hashnzfzclim  45012  sumsnd  45726  fmuldfeq  46279  stoweidlem3  46697  stoweidlem20  46714  stoweidlem34  46728  wallispilem4  46762  wallispi2lem1  46765  wallispi2lem2  46766  stirlinglem11  46778  dirkerper  46790  dirkertrigeqlem1  46792  dirkertrigeqlem3  46794  fourierdlem47  46847  fourierswlem  46924  smfmullem4  47488  ormklocald  47570  natlocalincr  47572  nthrucw  47582  ceilhalf1  48052  nprmdvdsfacm1lem4  48352  ppivalnnprm  48354  ppivalnn  48361  1oddALTV  48432  1nevenALTV  48433  2evenALTV  48434  nnsum3primes4  48530  nnsum3primesprm  48532  nnsum3primesgbe  48534  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  tgblthelfgott  48557  stgr1  48703  gpgusgralem  48798  1odd  48913  altgsumbcALT  49110  zlmodzxzsubm  49116  blen2  49342  blennngt2o2  49349  nn0sumshdiglemA  49376  nn0sumshdiglemB  49377