Theorem 1z 12707

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

This proof depends on syntax axioms:   ∈ wcel 2145  1c1 11182  ℤcz 12674

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rrecex 11253  ax-cnre 11254

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-neg 11525  df-nn 12317  df-z 12675

This theorem is used by:  1zzd  12708  peano2z  12718  peano2zm  12720  3halfnz  12759  peano5uzti  12770  nnuz  12985  1eluzge0  12988  2eluzge1  12990  eluz2nn  12996  eluz2b1  13027  uz2m1nn  13031  nninf  13037  1q  13073  nnrecq  13081  qbtwnxr  13311  fz1n  13655  fz10  13658  fz01en  13666  fznatpl1  13692  fz12pr  13695  fztpval  13700  fseq1p1m1  13712  elfzp1b  13715  elfzm1b  13716  4fvwrd4  13762  fzo1lb  13828  ige2m2fzo  13843  fz0add1fz1  13850  fzo12sn  13863  fzo13pr  13864  fzo1to4tp  13869  fzofzp1  13879  fzom1ne1  13900  fzostep1  13901  flge1nn  13941  fldiv4p1lem1div2  13955  modid0  14017  nnnfi  14089  fzennn  14091  fzen2  14092  f13idfv  14123  ser1const  14181  exp1  14190  zexpcl  14199  qexpcl  14200  qexpclz  14204  m1expcl  14209  expp1z  14234  expm1  14235  facnn  14399  fac0  14400  fac1  14401  bcn1  14437  bcpasc  14445  bcnm1  14451  hashsng  14493  hashfz  14552  fz1isolem  14586  seqcoll  14589  hashge2el2difr  14606  ccat2s1p2  14758  s2f1o  15047  f1oun2prg  15048  swrd2lsw  15085  2swrd2eqwrdeq  15086  relexp1g  15159  climuni  15699  isercoll2  15816  iseraltlem1  15829  sum0  15867  sumsnf  15889  climcndslem1  15998  climcndslem2  15999  divcnvshft  16004  supcvg  16005  prod0  16090  prodsn  16109  prodsnf  16111  zrisefaccl  16167  zfallfaccl  16168  sin01gt0  16338  rpnnen2lem10  16371  nthruc  16400  iddvds  16419  1dvds  16420  dvdsle  16460  dvds1  16469  3dvds  16481  n2dvds1  16518  divalglem5  16547  divalg  16553  bitsfzolem  16584  gcdcllem1  16649  gcdcllem3  16651  gcdaddmlem  16676  gcdadd  16678  gcdid  16679  gcd1  16681  1gcd  16686  bezoutlem1  16692  nn0rppwr  16715  nn0expgcd  16718  lcmgcdlem  16761  lcm1  16765  3lcm2e6woprm  16770  lcmfunsnlem  16796  isprm3  16838  ge2nprmge4  16857  phicl2  16925  phi1  16930  dfphi2  16931  eulerthlem2  16939  prmdiv  16942  prmdiveq  16943  odzcllem  16950  oddprm  16968  pythagtriplem4  16977  pcpre1  17000  pc1  17013  pcrec  17016  pcmpt  17050  fldivp1  17055  expnprm  17060  pockthlem  17063  unbenlem  17066  prmreclem2  17075  prmrec  17080  igz  17092  4sqlem12  17114  4sqlem13  17115  4sqlem19  17121  vdwlem8  17146  vdwlem13  17151  prmo1  17195  fvprmselgcd1  17203  prmlem0  17263  1259lem4  17292  2503lem2  17296  4001lem1  17299  setsstruct  17334  chnub  18776  gsumpropd2lem  18848  efmnd1hash  19068  mulgfval  19259  mulg1  19271  mulgm1  19284  mulgp1  19297  mulgneg2  19298  cycsubgcl  19401  odinv  19755  efgs1b  19930  lt6abl  20089  pgpfac1lem2  20271  srgbinomlem4  20435  qsubdrg  21705  zsubrg  21706  gzsubrg  21707  zringmulg  21742  zringcyg  21755  mulgrhm  21763  mulgrhm2  21764  pzriprnglem7  21773  pzriprnglem9  21775  pzriprnglem12  21778  pzriprnglem13  21779  pzriprnglem14  21780  pzriprng1ALT  21782  fermltlchr  21815  chrnzr  21816  frgpcyg  21859  zrhpsgnmhm  21870  zrhpsgnodpm  21878  m2detleiblem1  22919  m2detleiblem2  22923  zfbas  24195  imasdsf1olem  24672  cphipval  25544  cmetcaulem  25589  bcthlem5  25629  ehl1eudis  25721  ovolctb  25791  ovolunlem1a  25797  ovolunlem1  25798  ovoliunnul  25808  ovolicc1  25817  ovolicc2lem4  25821  voliunlem1  25851  volsup  25857  uniioombllem6  25889  vitalilem5  25913  plyeq0lem  26509  vieta1lem2  26616  elqaalem2  26625  qaa  26629  1aa  26632  iaaOLD  26634  abelthlem6  26745  abelthlem9  26749  sin2pim  26796  cos2pim  26797  logbleb  27093  logblt  27094  1cubrlem  27151  leibpilem2  27251  emcllem5  27309  emcllem7  27311  lgamgulm2  27345  lgamcvglem  27349  gamcvg2lem  27368  lgam1  27373  wilthlem2  27378  wilthlem3  27379  ppip1le  27470  ppi1  27473  cht1  27474  chp1  27476  cht2  27481  ppieq0  27485  ppiub  27513  chpeq0  27517  chpchtsum  27528  chpub  27529  logfacbnd3  27532  logexprlim  27534  bposlem1  27593  bposlem2  27594  bposlem5  27597  bposlem6  27598  lgslem2  27607  lgsfcl2  27612  lgsval2lem  27616  lgsdir2lem1  27634  lgsdir2lem5  27638  1lgs  27649  lgsdchr  27664  lgsquad2lem2  27694  2sqlem9  27736  2sqlem10  27737  2sqblem  27740  2sqb  27741  dchrisumlem3  27800  log2sumbnd  27853  qabvle  27934  ostth3  27947  istrkg3ld  28905  tgldimor  28947  axlowdimlem3  29504  axlowdimlem6  29507  axlowdimlem7  29508  axlowdimlem16  29517  axlowdimlem17  29518  axlowdim  29521  usgrexmpldifpr  29821  dfpth2  30296  uhgrwkspthlem2  30322  pthdlem2  30336  0ewlk  30687  0pth  30698  1wlkdlem1  30710  ntrl2v2e  30741  eupth2lem3lem4  30814  ex-fl  31030  ipval2  31291  hlim0  31819  opsqrlem2  32725  iuninc  33137  nndiffz1  33360  0dp2dp  33457  cshw1s2  33503  cycpmco2lem4  33672  1fldgenq  33866  znfermltl  33904  zringfrac  34068  constrextdg2  34363  cos9thpiminplylem5  34400  lmatfvlem  34429  mdetpmtr1  34437  mdetpmtr12  34439  lmlim  34561  qqh0  34598  qqh1  34599  esumfzf  34683  esumfsup  34684  esumpcvgval  34692  esumcvg  34700  esumcvgsum  34702  esumsup  34703  dya2ub  34885  rrvsum  35069  dstfrvclim1  35093  ballotlem2  35104  ballotlemfc0  35108  ballotlemfcc  35109  signsvf0  35192  hgt750leme  35270  subfac1  35912  subfacp1lem1  35913  subfacp1lem2a  35914  subfacp1lem5  35918  subfacp1lem6  35919  cvmliftlem10  36028  divcnvlin  36467  faclimlem1  36477  fwddifnp1  36900  irrdiff  38215  qdiff  38216  poimirlem3  38509  poimirlem4  38510  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem24  38530  poimirlem27  38533  poimirlem28  38534  poimirlem31  38537  poimirlem32  38538  mblfinlem1  38543  mblfinlem2  38544  ovoliunnfl  38548  voliunnfl  38550  fdc  38647  heibor1lem  38711  rrncmslem  38734  lcmfunnnd  43030  lcm1un  43031  lcm2un  43032  lcmineqlem11  43057  lcmineqlem19  43065  aks4d1p1p2  43088  mapfzcons  43680  mzpexpmpt  43709  eldioph3b  43729  fz1eqin  43733  diophin  43736  diophun  43737  0dioph  43742  elnnrabdioph  43767  rabren3dioph  43775  irrapxlem1  43782  irrapxlem3  43784  rmxyadd  43881  rmxy1  43882  rmxy0  43883  rmxp1  43892  rmyp1  43893  rmxm1  43894  rmym1  43895  jm2.24nn  43919  acongeq  43943  jm2.23  43956  jm2.15nn0  43963  jm2.16nn0  43964  jm2.27c  43967  jm2.27dlem2  43970  rmydioph  43974  rmxdioph  43976  expdiophlem2  43982  expdioph  43983  mpaaeu  44110  trclfvdecomr  44687  k0004val0  45113  hashnzfzclim  45265  sumsnd  45986  fmuldfeq  46539  stoweidlem3  46957  stoweidlem20  46974  stoweidlem34  46988  wallispilem4  47022  wallispi2lem1  47025  wallispi2lem2  47026  stirlinglem11  47038  dirkerper  47050  dirkertrigeqlem1  47052  dirkertrigeqlem3  47054  fourierdlem47  47107  fourierswlem  47184  smfmullem4  47748  ormklocald  47830  sqrtnnaa  47857  sqrtnzqaa  47858  ceilhalf1  48352  nprmdvdsfacm1lem4  48652  ppivalnnprm  48654  ppivalnn  48661  1oddALTV  48732  1nevenALTV  48733  2evenALTV  48734  nnsum3primes4  48830  nnsum3primesprm  48832  nnsum3primesgbe  48834  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  tgblthelfgott  48857  stgr1  49003  gpgusgralem  49098  1odd  49212  altgsumbcALT  49409  zlmodzxzsubm  49415  blen2  49641  blennngt2o2  49648  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  crosspdotsumlem  50908  crosspaltd  50910  crossp3d  50911  veroquadgsumlem  50927