Theorem 1z 12642

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

This proof depends on syntax axioms:   ∈ wcel 2146  1c1 11119  ℤcz 12609

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rrecex 11190  ax-cnre 11191

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-neg 11462  df-nn 12252  df-z 12610

This theorem is used by:  1zzd  12643  peano2z  12653  peano2zm  12655  3halfnz  12693  peano5uzti  12704  nnuz  12919  1eluzge0  12922  2eluzge1  12924  eluz2nn  12930  eluz2b1  12961  uz2m1nn  12965  nninf  12971  nnrecq  13014  qbtwnxr  13244  fz1n  13588  fz10  13591  fz01en  13599  fznatpl1  13625  fz12pr  13628  fztpval  13633  fseq1p1m1  13645  elfzp1b  13648  elfzm1b  13649  4fvwrd4  13695  fzo1lb  13761  ige2m2fzo  13776  fz0add1fz1  13783  fzo12sn  13796  fzo13pr  13797  fzo1to4tp  13802  fzofzp1  13812  fzom1ne1  13833  fzostep1  13834  flge1nn  13874  fldiv4p1lem1div2  13888  modid0  13950  nnnfi  14022  fzennn  14024  fzen2  14025  f13idfv  14056  ser1const  14114  exp1  14123  zexpcl  14132  qexpcl  14133  qexpclz  14137  m1expcl  14142  expp1z  14167  expm1  14168  facnn  14331  fac0  14332  fac1  14333  bcn1  14369  bcpasc  14377  bcnm1  14383  hashsng  14425  hashfz  14484  fz1isolem  14518  seqcoll  14521  hashge2el2difr  14538  ccat2s1p2  14690  s2f1o  14979  f1oun2prg  14980  swrd2lsw  15015  2swrd2eqwrdeq  15016  relexp1g  15089  climuni  15629  isercoll2  15746  iseraltlem1  15759  sum0  15798  sumsnf  15820  climcndslem1  15929  climcndslem2  15930  divcnvshft  15935  supcvg  15936  prod0  16023  prodsn  16042  prodsnf  16044  zrisefaccl  16100  zfallfaccl  16101  sin01gt0  16271  rpnnen2lem10  16304  nthruc  16333  iddvds  16352  1dvds  16353  dvdsle  16393  dvds1  16402  3dvds  16414  n2dvds1  16451  divalglem5  16480  divalg  16486  bitsfzolem  16517  gcdcllem1  16582  gcdcllem3  16584  gcdaddmlem  16607  gcdadd  16609  gcdid  16610  gcd1  16611  1gcd  16616  bezoutlem1  16622  nn0rppwr  16644  nn0expgcd  16647  lcmgcdlem  16689  lcm1  16693  3lcm2e6woprm  16698  lcmfunsnlem  16724  isprm3  16766  ge2nprmge4  16785  phicl2  16852  phi1  16857  dfphi2  16858  eulerthlem2  16866  prmdiv  16869  prmdiveq  16870  odzcllem  16877  oddprm  16895  pythagtriplem4  16904  pcpre1  16927  pc1  16940  pcrec  16943  pcmpt  16977  fldivp1  16982  expnprm  16987  pockthlem  16990  unbenlem  16993  prmreclem2  17002  prmrec  17007  igz  17019  4sqlem12  17041  4sqlem13  17042  4sqlem19  17048  vdwlem8  17073  vdwlem13  17078  prmo1  17122  fvprmselgcd1  17130  prmlem0  17190  1259lem4  17219  2503lem2  17223  4001lem1  17226  setsstruct  17261  chnub  18703  gsumpropd2lem  18766  efmnd1hash  18982  mulgfval  19166  mulg1  19178  mulgm1  19191  mulgp1  19204  mulgneg2  19205  cycsubgcl  19308  odinv  19662  efgs1b  19837  lt6abl  19996  pgpfac1lem2  20178  srgbinomlem4  20342  qsubdrg  21606  zsubrg  21607  gzsubrg  21608  zringmulg  21643  zringcyg  21656  mulgrhm  21664  mulgrhm2  21665  pzriprnglem7  21674  pzriprnglem9  21676  pzriprnglem12  21679  pzriprnglem13  21680  pzriprnglem14  21681  pzriprng1ALT  21683  fermltlchr  21716  chrnzr  21717  frgpcyg  21760  zrhpsgnmhm  21771  zrhpsgnodpm  21779  m2detleiblem1  22818  m2detleiblem2  22822  zfbas  24090  imasdsf1olem  24567  cphipval  25439  cmetcaulem  25484  bcthlem5  25524  ehl1eudis  25616  ovolctb  25686  ovolunlem1a  25692  ovolunlem1  25693  ovoliunnul  25703  ovolicc1  25712  ovolicc2lem4  25716  voliunlem1  25746  volsup  25752  uniioombllem6  25784  vitalilem5  25808  plyeq0lem  26404  vieta1lem2  26509  elqaalem2  26518  qaa  26521  1aa  26524  iaa  26525  abelthlem6  26636  abelthlem9  26640  sin2pim  26687  cos2pim  26688  logbleb  26985  logblt  26986  1cubrlem  27043  leibpilem2  27143  emcllem5  27201  emcllem7  27203  lgamgulm2  27237  lgamcvglem  27241  gamcvg2lem  27260  lgam1  27265  wilthlem2  27270  wilthlem3  27271  ppip1le  27362  ppi1  27365  cht1  27366  chp1  27368  cht2  27373  ppieq0  27377  ppiub  27405  chpeq0  27409  chpchtsum  27420  chpub  27421  logfacbnd3  27424  logexprlim  27426  bposlem1  27485  bposlem2  27486  bposlem5  27489  bposlem6  27490  lgslem2  27499  lgsfcl2  27504  lgsval2lem  27508  lgsdir2lem1  27526  lgsdir2lem5  27530  1lgs  27541  lgsdchr  27556  lgsquad2lem2  27586  2sqlem9  27628  2sqlem10  27629  2sqblem  27632  2sqb  27633  dchrisumlem3  27692  log2sumbnd  27745  qabvle  27826  ostth3  27839  istrkg3ld  28767  tgldimor  28808  axlowdimlem3  29331  axlowdimlem6  29334  axlowdimlem7  29335  axlowdimlem16  29344  axlowdimlem17  29345  axlowdim  29348  usgrexmpldifpr  29645  dfpth2  30115  uhgrwkspthlem2  30140  pthdlem2  30154  0ewlk  30502  0pth  30513  1wlkdlem1  30525  ntrl2v2e  30546  eupth2lem3lem4  30619  ex-fl  30835  ipval2  31096  hlim0  31624  opsqrlem2  32530  iuninc  32942  nndiffz1  33168  0dp2dp  33265  cshw1s2  33311  cycpmco2lem4  33480  1fldgenq  33674  znfermltl  33712  zringfrac  33875  constrextdg2  34170  cos9thpiminplylem5  34207  lmatfvlem  34236  mdetpmtr1  34244  mdetpmtr12  34246  lmlim  34368  qqh0  34405  qqh1  34406  esumfzf  34490  esumfsup  34491  esumpcvgval  34499  esumcvg  34507  esumcvgsum  34509  esumsup  34510  dya2ub  34692  rrvsum  34876  dstfrvclim1  34900  ballotlem2  34911  ballotlemfc0  34915  ballotlemfcc  34916  signsvf0  34999  hgt750leme  35077  subfac1  35691  subfacp1lem1  35692  subfacp1lem2a  35693  subfacp1lem5  35697  subfacp1lem6  35698  cvmliftlem10  35807  divcnvlin  36246  faclimlem1  36256  fwddifnp1  36678  irrdiff  38011  qdiff  38012  poimirlem3  38315  poimirlem4  38316  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem24  38336  poimirlem27  38339  poimirlem28  38340  poimirlem31  38343  poimirlem32  38344  mblfinlem1  38349  mblfinlem2  38350  ovoliunnfl  38354  voliunnfl  38356  fdc  38437  heibor1lem  38501  rrncmslem  38524  lcmfunnnd  42820  lcm1un  42821  lcm2un  42822  lcmineqlem11  42847  lcmineqlem19  42855  aks4d1p1p2  42878  mapfzcons  43488  mzpexpmpt  43517  eldioph3b  43537  fz1eqin  43541  diophin  43544  diophun  43545  0dioph  43550  elnnrabdioph  43575  rabren3dioph  43583  irrapxlem1  43590  irrapxlem3  43592  rmxyadd  43689  rmxy1  43690  rmxy0  43691  rmxp1  43700  rmyp1  43701  rmxm1  43702  rmym1  43703  jm2.24nn  43727  acongeq  43751  jm2.23  43764  jm2.15nn0  43771  jm2.16nn0  43772  jm2.27c  43775  jm2.27dlem2  43778  rmydioph  43782  rmxdioph  43784  expdiophlem2  43790  expdioph  43791  mpaaeu  43918  trclfvdecomr  44495  k0004val0  44921  hashnzfzclim  45073  sumsnd  45787  fmuldfeq  46340  stoweidlem3  46758  stoweidlem20  46775  stoweidlem34  46789  wallispilem4  46823  wallispi2lem1  46826  wallispi2lem2  46827  stirlinglem11  46839  dirkerper  46851  dirkertrigeqlem1  46853  dirkertrigeqlem3  46855  fourierdlem47  46908  fourierswlem  46985  smfmullem4  47549  ormklocald  47631  natlocalincr  47633  sqrtnnaa  47645  sqrtnzqaa  47646  ceilhalf1  48116  nprmdvdsfacm1lem4  48416  ppivalnnprm  48418  ppivalnn  48425  1oddALTV  48496  1nevenALTV  48497  2evenALTV  48498  nnsum3primes4  48594  nnsum3primesprm  48596  nnsum3primesgbe  48598  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  tgblthelfgott  48621  stgr1  48767  gpgusgralem  48862  1odd  48977  altgsumbcALT  49174  zlmodzxzsubm  49180  blen2  49406  blennngt2o2  49413  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441  1elfz13  50666  2elfz13  50667  crosspdotsumi  50687  crosspalti  50689  crossp3i  50690