Theorem 1z 12644

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

Syntax hints:   ∈ wcel 2105  1c1 11153  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-z 12611

This theorem is referenced by:  1zzd  12645  peano2z  12655  peano2zm  12657  3halfnz  12694  peano5uzti  12705  nnuz  12918  eluz2nn  12921  eluzge3nn  12929  1eluzge0  12931  2eluzge1  12933  eluz2b1  12958  uz2m1nn  12962  nninf  12968  nnrecq  13011  qbtwnxr  13238  fz1n  13578  fz10  13581  fz01en  13588  fznatpl1  13614  fz12pr  13617  fztpval  13622  fseq1p1m1  13634  elfzp1b  13637  elfzm1b  13638  4fvwrd4  13684  fzo1lb  13749  ige2m2fzo  13763  fz0add1fz1  13770  fzo12sn  13783  fzo13pr  13784  fzo1to4tp  13789  fzofzp1  13799  fzostep1  13818  flge1nn  13857  fldiv4p1lem1div2  13871  modid0  13933  nnnfi  14003  fzennn  14005  fzen2  14006  f13idfv  14037  ser1const  14095  exp1  14104  zexpcl  14113  qexpcl  14114  qexpclz  14118  m1expcl  14123  expp1z  14148  expm1  14149  facnn  14310  fac0  14311  fac1  14312  bcn1  14348  bcpasc  14356  bcnm1  14362  hashsng  14404  hashfz  14462  fz1isolem  14496  seqcoll  14499  hashge2el2difr  14516  ccat2s1p2  14664  s2f1o  14951  f1oun2prg  14952  swrd2lsw  14987  2swrd2eqwrdeq  14988  relexp1g  15061  climuni  15584  isercoll2  15701  iseraltlem1  15714  sum0  15753  sumsnf  15775  climcndslem1  15881  climcndslem2  15882  divcnvshft  15887  supcvg  15888  prod0  15975  prodsn  15994  prodsnf  15996  zrisefaccl  16052  zfallfaccl  16053  sin01gt0  16222  rpnnen2lem10  16255  nthruc  16284  iddvds  16303  1dvds  16304  dvdsle  16343  dvds1  16352  3dvds  16364  n2dvds1  16401  divalglem5  16430  divalg  16436  bitsfzolem  16467  gcdcllem1  16532  gcdcllem3  16534  gcdaddmlem  16557  gcdadd  16559  gcdid  16560  gcd1  16561  1gcd  16566  bezoutlem1  16572  nn0rppwr  16594  nn0expgcd  16597  lcmgcdlem  16639  lcm1  16643  3lcm2e6woprm  16648  lcmfunsnlem  16674  isprm3  16716  ge2nprmge4  16734  phicl2  16801  phi1  16806  dfphi2  16807  eulerthlem2  16815  prmdiv  16818  prmdiveq  16819  odzcllem  16825  oddprm  16843  pythagtriplem4  16852  pcpre1  16875  pc1  16888  pcrec  16891  pcmpt  16925  fldivp1  16930  expnprm  16935  pockthlem  16938  unbenlem  16941  prmreclem2  16950  prmrec  16955  igz  16967  4sqlem12  16989  4sqlem13  16990  4sqlem19  16996  vdwlem8  17021  vdwlem13  17026  prmo1  17070  fvprmselgcd1  17078  prmlem0  17139  1259lem4  17167  2503lem2  17171  4001lem1  17174  setsstruct  17209  gsumpropd2lem  18704  efmnd1hash  18917  mulgfval  19099  mulg1  19111  mulgm1  19124  mulgp1  19137  mulgneg2  19138  cycsubgcl  19236  odinv  19593  efgs1b  19768  lt6abl  19927  pgpfac1lem2  20109  srgbinomlem4  20246  qsubdrg  21454  zsubrg  21455  gzsubrg  21456  zringmulg  21484  zringcyg  21497  mulgrhm  21505  mulgrhm2  21506  pzriprnglem7  21515  pzriprnglem9  21517  pzriprnglem12  21520  pzriprnglem13  21521  pzriprnglem14  21522  pzriprng1ALT  21524  fermltlchr  21561  chrnzr  21562  frgpcyg  21609  zrhpsgnmhm  21619  zrhpsgnodpm  21627  m2detleiblem1  22645  m2detleiblem2  22649  zfbas  23919  imasdsf1olem  24398  cphipval  25290  cmetcaulem  25335  bcthlem5  25375  ehl1eudis  25467  ovolctb  25538  ovolunlem1a  25544  ovolunlem1  25545  ovoliunnul  25555  ovolicc1  25564  ovolicc2lem4  25568  voliunlem1  25598  volsup  25604  uniioombllem6  25636  vitalilem5  25660  plyeq0lem  26263  vieta1lem2  26367  elqaalem2  26376  qaa  26379  iaa  26381  abelthlem6  26494  abelthlem9  26498  sin2pim  26541  cos2pim  26542  logbleb  26840  logblt  26841  1cubrlem  26898  leibpilem2  26998  emcllem5  27057  emcllem7  27059  lgamgulm2  27093  lgamcvglem  27097  gamcvg2lem  27116  lgam1  27121  wilthlem2  27126  wilthlem3  27127  ppip1le  27218  ppi1  27221  cht1  27222  chp1  27224  cht2  27229  ppieq0  27233  ppiub  27262  chpeq0  27266  chpchtsum  27277  chpub  27278  logfacbnd3  27281  logexprlim  27283  bposlem1  27342  bposlem2  27343  bposlem5  27346  bposlem6  27347  lgslem2  27356  lgsfcl2  27361  lgsval2lem  27365  lgsdir2lem1  27383  lgsdir2lem5  27387  1lgs  27398  lgsdchr  27413  lgsquad2lem2  27443  2sqlem9  27485  2sqlem10  27486  2sqblem  27489  2sqb  27490  dchrisumlem3  27549  log2sumbnd  27602  qabvle  27683  ostth3  27696  istrkg3ld  28483  tgldimor  28524  axlowdimlem3  28973  axlowdimlem6  28976  axlowdimlem7  28977  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  usgrexmpldifpr  29289  uhgrwkspthlem2  29786  pthdlem2  29800  0ewlk  30142  0pth  30153  1wlkdlem1  30165  ntrl2v2e  30186  eupth2lem3lem4  30259  ex-fl  30475  ipval2  30735  hlim0  31263  opsqrlem2  32169  iuninc  32580  nndiffz1  32794  fzom1ne1  32808  0dp2dp  32875  cshw1s2  32929  chnub  32985  cycpmco2lem4  33131  1fldgenq  33303  znfermltl  33373  zringfrac  33561  lmatfvlem  33775  mdetpmtr1  33783  mdetpmtr12  33785  lmlim  33907  qqh0  33946  qqh1  33947  esumfzf  34049  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  esumcvgsum  34068  esumsup  34069  dya2ub  34251  rrvsum  34435  dstfrvclim1  34458  ballotlem2  34469  ballotlemfc0  34473  ballotlemfcc  34474  signsvf0  34573  hgt750leme  34651  subfac1  35162  subfacp1lem1  35163  subfacp1lem2a  35164  subfacp1lem5  35168  subfacp1lem6  35169  cvmliftlem10  35278  divcnvlin  35712  faclimlem1  35722  fwddifnp1  36146  irrdiff  37308  poimirlem3  37609  poimirlem4  37610  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  mblfinlem1  37643  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  fdc  37731  heibor1lem  37795  rrncmslem  37818  lcmfunnnd  41993  lcm1un  41994  lcm2un  41995  lcmineqlem11  42020  lcmineqlem19  42028  aks4d1p1p2  42051  mapfzcons  42703  mzpexpmpt  42732  eldioph3b  42752  fz1eqin  42756  diophin  42759  diophun  42760  0dioph  42765  elnnrabdioph  42794  rabren3dioph  42802  irrapxlem1  42809  irrapxlem3  42811  rmxyadd  42909  rmxy1  42910  rmxy0  42911  rmxp1  42920  rmyp1  42921  rmxm1  42922  rmym1  42923  jm2.24nn  42947  acongeq  42971  jm2.23  42984  jm2.15nn0  42991  jm2.16nn0  42992  jm2.27c  42995  jm2.27dlem2  42998  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  mpaaeu  43138  trclfvdecomr  43717  k0004val0  44143  hashnzfzclim  44317  sumsnd  44963  fmuldfeq  45538  stoweidlem3  45958  stoweidlem20  45975  stoweidlem34  45989  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem11  46039  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  fourierdlem47  46108  fourierswlem  46185  smfmullem4  46749  natlocalincr  46829  tworepnotupword  46839  1oddALTV  47614  1nevenALTV  47615  2evenALTV  47616  nnsum3primes4  47712  nnsum3primesprm  47714  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  tgblthelfgott  47739  stgr1  47863  gpgusgralem  47945  1odd  48014  altgsumbcALT  48197  zlmodzxzsubm  48203  blen2  48434  blennngt2o2  48441  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469