Theorem 1z 12652

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

This proof depends on syntax axioms:   ∈ wcel 2145  1c1 11129  ℤcz 12619

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11472  df-nn 12262  df-z 12620

This theorem is used by:  1zzd  12653  peano2z  12663  peano2zm  12665  3halfnz  12704  peano5uzti  12715  nnuz  12930  1eluzge0  12933  2eluzge1  12935  eluz2nn  12941  eluz2b1  12972  uz2m1nn  12976  nninf  12982  1q  13018  nnrecq  13026  qbtwnxr  13256  fz1n  13600  fz10  13603  fz01en  13611  fznatpl1  13637  fz12pr  13640  fztpval  13645  fseq1p1m1  13657  elfzp1b  13660  elfzm1b  13661  4fvwrd4  13707  fzo1lb  13773  ige2m2fzo  13788  fz0add1fz1  13795  fzo12sn  13808  fzo13pr  13809  fzo1to4tp  13814  fzofzp1  13824  fzom1ne1  13845  fzostep1  13846  flge1nn  13886  fldiv4p1lem1div2  13900  modid0  13962  nnnfi  14034  fzennn  14036  fzen2  14037  f13idfv  14068  ser1const  14126  exp1  14135  zexpcl  14144  qexpcl  14145  qexpclz  14149  m1expcl  14154  expp1z  14179  expm1  14180  facnn  14343  fac0  14344  fac1  14345  bcn1  14381  bcpasc  14389  bcnm1  14395  hashsng  14437  hashfz  14496  fz1isolem  14530  seqcoll  14533  hashge2el2difr  14550  ccat2s1p2  14702  s2f1o  14991  f1oun2prg  14992  swrd2lsw  15029  2swrd2eqwrdeq  15030  relexp1g  15103  climuni  15643  isercoll2  15760  iseraltlem1  15773  sum0  15811  sumsnf  15833  climcndslem1  15942  climcndslem2  15943  divcnvshft  15948  supcvg  15949  prod0  16036  prodsn  16055  prodsnf  16057  zrisefaccl  16113  zfallfaccl  16114  sin01gt0  16284  rpnnen2lem10  16317  nthruc  16346  iddvds  16365  1dvds  16366  dvdsle  16406  dvds1  16415  3dvds  16427  n2dvds1  16464  divalglem5  16493  divalg  16499  bitsfzolem  16530  gcdcllem1  16595  gcdcllem3  16597  gcdaddmlem  16620  gcdadd  16622  gcdid  16623  gcd1  16624  1gcd  16629  bezoutlem1  16635  nn0rppwr  16657  nn0expgcd  16660  lcmgcdlem  16702  lcm1  16706  3lcm2e6woprm  16711  lcmfunsnlem  16737  isprm3  16779  ge2nprmge4  16798  phicl2  16865  phi1  16870  dfphi2  16871  eulerthlem2  16879  prmdiv  16882  prmdiveq  16883  odzcllem  16890  oddprm  16908  pythagtriplem4  16917  pcpre1  16940  pc1  16953  pcrec  16956  pcmpt  16990  fldivp1  16995  expnprm  17000  pockthlem  17003  unbenlem  17006  prmreclem2  17015  prmrec  17020  igz  17032  4sqlem12  17054  4sqlem13  17055  4sqlem19  17061  vdwlem8  17086  vdwlem13  17091  prmo1  17135  fvprmselgcd1  17143  prmlem0  17203  1259lem4  17232  2503lem2  17236  4001lem1  17239  setsstruct  17274  chnub  18716  gsumpropd2lem  18787  efmnd1hash  19007  mulgfval  19198  mulg1  19210  mulgm1  19223  mulgp1  19236  mulgneg2  19237  cycsubgcl  19340  odinv  19694  efgs1b  19869  lt6abl  20028  pgpfac1lem2  20210  srgbinomlem4  20374  qsubdrg  21638  zsubrg  21639  gzsubrg  21640  zringmulg  21675  zringcyg  21688  mulgrhm  21696  mulgrhm2  21697  pzriprnglem7  21706  pzriprnglem9  21708  pzriprnglem12  21711  pzriprnglem13  21712  pzriprnglem14  21713  pzriprng1ALT  21715  fermltlchr  21748  chrnzr  21749  frgpcyg  21792  zrhpsgnmhm  21803  zrhpsgnodpm  21811  m2detleiblem1  22852  m2detleiblem2  22856  zfbas  24128  imasdsf1olem  24605  cphipval  25477  cmetcaulem  25522  bcthlem5  25562  ehl1eudis  25654  ovolctb  25724  ovolunlem1a  25730  ovolunlem1  25731  ovoliunnul  25741  ovolicc1  25750  ovolicc2lem4  25754  voliunlem1  25784  volsup  25790  uniioombllem6  25822  vitalilem5  25846  plyeq0lem  26443  vieta1lem2  26550  elqaalem2  26559  qaa  26563  1aa  26566  iaaOLD  26568  abelthlem6  26679  abelthlem9  26683  sin2pim  26730  cos2pim  26731  logbleb  27028  logblt  27029  1cubrlem  27086  leibpilem2  27186  emcllem5  27244  emcllem7  27246  lgamgulm2  27280  lgamcvglem  27284  gamcvg2lem  27303  lgam1  27308  wilthlem2  27313  wilthlem3  27314  ppip1le  27405  ppi1  27408  cht1  27409  chp1  27411  cht2  27416  ppieq0  27420  ppiub  27448  chpeq0  27452  chpchtsum  27463  chpub  27464  logfacbnd3  27467  logexprlim  27469  bposlem1  27528  bposlem2  27529  bposlem5  27532  bposlem6  27533  lgslem2  27542  lgsfcl2  27547  lgsval2lem  27551  lgsdir2lem1  27569  lgsdir2lem5  27573  1lgs  27584  lgsdchr  27599  lgsquad2lem2  27629  2sqlem9  27671  2sqlem10  27672  2sqblem  27675  2sqb  27676  dchrisumlem3  27735  log2sumbnd  27788  qabvle  27869  ostth3  27882  istrkg3ld  28810  tgldimor  28852  axlowdimlem3  29409  axlowdimlem6  29412  axlowdimlem7  29413  axlowdimlem16  29422  axlowdimlem17  29423  axlowdim  29426  usgrexmpldifpr  29726  dfpth2  30201  uhgrwkspthlem2  30227  pthdlem2  30241  0ewlk  30592  0pth  30603  1wlkdlem1  30615  ntrl2v2e  30646  eupth2lem3lem4  30719  ex-fl  30935  ipval2  31196  hlim0  31724  opsqrlem2  32630  iuninc  33042  nndiffz1  33265  0dp2dp  33362  cshw1s2  33408  cycpmco2lem4  33577  1fldgenq  33771  znfermltl  33809  zringfrac  33972  constrextdg2  34267  cos9thpiminplylem5  34304  lmatfvlem  34333  mdetpmtr1  34341  mdetpmtr12  34343  lmlim  34465  qqh0  34502  qqh1  34503  esumfzf  34587  esumfsup  34588  esumpcvgval  34596  esumcvg  34604  esumcvgsum  34606  esumsup  34607  dya2ub  34789  rrvsum  34973  dstfrvclim1  34997  ballotlem2  35008  ballotlemfc0  35012  ballotlemfcc  35013  signsvf0  35096  hgt750leme  35174  subfac1  35765  subfacp1lem1  35766  subfacp1lem2a  35767  subfacp1lem5  35771  subfacp1lem6  35772  cvmliftlem10  35881  divcnvlin  36320  faclimlem1  36330  fwddifnp1  36753  irrdiff  38086  qdiff  38087  poimirlem3  38380  poimirlem4  38381  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem24  38401  poimirlem27  38404  poimirlem28  38405  poimirlem31  38408  poimirlem32  38409  mblfinlem1  38414  mblfinlem2  38415  ovoliunnfl  38419  voliunnfl  38421  fdc  38503  heibor1lem  38567  rrncmslem  38590  lcmfunnnd  42886  lcm1un  42887  lcm2un  42888  lcmineqlem11  42913  lcmineqlem19  42921  aks4d1p1p2  42944  mapfzcons  43569  mzpexpmpt  43598  eldioph3b  43618  fz1eqin  43622  diophin  43625  diophun  43626  0dioph  43631  elnnrabdioph  43656  rabren3dioph  43664  irrapxlem1  43671  irrapxlem3  43673  rmxyadd  43770  rmxy1  43771  rmxy0  43772  rmxp1  43781  rmyp1  43782  rmxm1  43783  rmym1  43784  jm2.24nn  43808  acongeq  43832  jm2.23  43845  jm2.15nn0  43852  jm2.16nn0  43853  jm2.27c  43856  jm2.27dlem2  43859  rmydioph  43863  rmxdioph  43865  expdiophlem2  43871  expdioph  43872  mpaaeu  43999  trclfvdecomr  44576  k0004val0  45002  hashnzfzclim  45154  sumsnd  45868  fmuldfeq  46421  stoweidlem3  46839  stoweidlem20  46856  stoweidlem34  46870  wallispilem4  46904  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem11  46920  dirkerper  46932  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  fourierdlem47  46989  fourierswlem  47066  smfmullem4  47630  ormklocald  47712  sqrtnnaa  47739  sqrtnzqaa  47740  ceilhalf1  48234  nprmdvdsfacm1lem4  48534  ppivalnnprm  48536  ppivalnn  48543  1oddALTV  48614  1nevenALTV  48615  2evenALTV  48616  nnsum3primes4  48712  nnsum3primesprm  48714  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  tgblthelfgott  48739  stgr1  48885  gpgusgralem  48980  1odd  49094  altgsumbcALT  49291  zlmodzxzsubm  49297  blen2  49523  blennngt2o2  49530  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  crosspdotsumlem  50805  crosspaltd  50807  crossp3d  50808  veroquadgsumlem  50824