Theorem 1z 12594

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

Syntax hints:   ∈ wcel 2106  1c1 11113  ℤcz 12560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-neg 11449  df-nn 12215  df-z 12561

This theorem is referenced by:  1zzd  12595  peano2z  12605  peano2zm  12607  3halfnz  12643  peano5uzti  12654  nnuz  12867  eluz2nn  12870  eluzge3nn  12876  1eluzge0  12878  2eluzge1  12880  eluz2b1  12905  uz2m1nn  12909  nninf  12915  nnrecq  12958  qbtwnxr  13181  fz1n  13521  fz10  13524  fz01en  13531  fznatpl1  13557  fz12pr  13560  fztpval  13565  fseq1p1m1  13577  elfzp1b  13580  elfzm1b  13581  4fvwrd4  13623  ige2m2fzo  13697  fz0add1fz1  13704  fzo12sn  13717  fzo13pr  13718  fzo1to4tp  13722  fzofzp1  13731  fzostep1  13750  flge1nn  13788  fldiv4p1lem1div2  13802  modid0  13864  nnnfi  13933  fzennn  13935  fzen2  13936  f13idfv  13967  ser1const  14026  exp1  14035  zexpcl  14044  qexpcl  14045  qexpclz  14049  m1expcl  14054  expp1z  14079  expm1  14080  facnn  14237  fac0  14238  fac1  14239  bcn1  14275  bcpasc  14283  bcnm1  14289  hashsng  14331  hashfz  14389  fz1isolem  14424  seqcoll  14427  hashge2el2difr  14444  ccat2s1p2  14582  s2f1o  14869  f1oun2prg  14870  swrd2lsw  14905  2swrd2eqwrdeq  14906  relexp1g  14975  climuni  15498  isercoll2  15617  iseraltlem1  15630  sum0  15669  sumsnf  15691  climcndslem1  15797  climcndslem2  15798  divcnvshft  15803  supcvg  15804  prod0  15889  prodsn  15908  prodsnf  15910  zrisefaccl  15966  zfallfaccl  15967  sin01gt0  16135  rpnnen2lem10  16168  nthruc  16197  iddvds  16215  1dvds  16216  dvdsle  16255  dvds1  16264  3dvds  16276  n2dvds1  16313  divalglem5  16342  divalg  16348  bitsfzolem  16377  gcdcllem1  16442  gcdcllem3  16444  gcdaddmlem  16467  gcdadd  16469  gcdid  16470  gcd1  16471  1gcd  16477  bezoutlem1  16483  lcmgcdlem  16545  lcm1  16549  3lcm2e6woprm  16554  lcmfunsnlem  16580  isprm3  16622  ge2nprmge4  16640  phicl2  16703  phi1  16708  dfphi2  16709  eulerthlem2  16717  prmdiv  16720  prmdiveq  16721  odzcllem  16727  oddprm  16745  pythagtriplem4  16754  pcpre1  16777  pc1  16790  pcrec  16793  pcmpt  16827  fldivp1  16832  expnprm  16837  pockthlem  16840  unbenlem  16843  prmreclem2  16852  prmrec  16857  igz  16869  4sqlem12  16891  4sqlem13  16892  4sqlem19  16898  vdwlem8  16923  vdwlem13  16928  prmo1  16972  fvprmselgcd1  16980  prmlem0  17041  1259lem4  17069  2503lem2  17073  4001lem1  17076  setsstruct  17111  gsumpropd2lem  18600  efmnd1hash  18775  mulgfval  18954  mulg1  18963  mulgm1  18976  mulgp1  18989  mulgneg2  18990  cycsubgcl  19085  odinv  19431  efgs1b  19606  lt6abl  19765  pgpfac1lem2  19947  srgbinomlem4  20054  qsubdrg  21003  zsubrg  21004  gzsubrg  21005  zringmulg  21032  zringcyg  21045  mulgrhm  21053  mulgrhm2  21054  chrnzr  21088  frgpcyg  21135  zrhpsgnmhm  21143  zrhpsgnodpm  21151  m2detleiblem1  22133  m2detleiblem2  22137  zfbas  23407  imasdsf1olem  23886  cphipval  24767  cmetcaulem  24812  bcthlem5  24852  ehl1eudis  24944  ovolctb  25014  ovolunlem1a  25020  ovolunlem1  25021  ovoliunnul  25031  ovolicc1  25040  ovolicc2lem4  25044  voliunlem1  25074  volsup  25080  uniioombllem6  25112  vitalilem5  25136  plyeq0lem  25731  vieta1lem2  25831  elqaalem2  25840  qaa  25843  iaa  25845  abelthlem6  25955  abelthlem9  25959  sin2pim  26002  cos2pim  26003  logbleb  26295  logblt  26296  1cubrlem  26353  leibpilem2  26453  emcllem5  26511  emcllem7  26513  lgamgulm2  26547  lgamcvglem  26551  gamcvg2lem  26570  lgam1  26575  wilthlem2  26580  wilthlem3  26581  ppip1le  26672  ppi1  26675  cht1  26676  chp1  26678  cht2  26683  ppieq0  26687  ppiub  26714  chpeq0  26718  chpchtsum  26729  chpub  26730  logfacbnd3  26733  logexprlim  26735  bposlem1  26794  bposlem2  26795  bposlem5  26798  bposlem6  26799  lgslem2  26808  lgsfcl2  26813  lgsval2lem  26817  lgsdir2lem1  26835  lgsdir2lem5  26839  1lgs  26850  lgsdchr  26865  lgsquad2lem2  26895  2sqlem9  26937  2sqlem10  26938  2sqblem  26941  2sqb  26942  dchrisumlem3  27001  log2sumbnd  27054  qabvle  27135  ostth3  27148  istrkg3ld  27750  tgldimor  27791  axlowdimlem3  28240  axlowdimlem6  28243  axlowdimlem7  28244  axlowdimlem16  28253  axlowdimlem17  28254  axlowdim  28257  usgrexmpldifpr  28553  uhgrwkspthlem2  29049  pthdlem2  29063  0ewlk  29405  0pth  29416  1wlkdlem1  29428  ntrl2v2e  29449  eupth2lem3lem4  29522  ex-fl  29738  ipval2  29998  hlim0  30526  opsqrlem2  31432  iuninc  31830  nndiffz1  32035  fzom1ne1  32050  0dp2dp  32113  cshw1s2  32162  cycpmco2lem4  32329  1fldgenq  32453  fermltlchr  32523  znfermltl  32524  lmatfvlem  32864  mdetpmtr1  32872  mdetpmtr12  32874  lmlim  32996  qqh0  33033  qqh1  33034  esumfzf  33136  esumfsup  33137  esumpcvgval  33145  esumcvg  33153  esumcvgsum  33155  esumsup  33156  dya2ub  33338  rrvsum  33522  dstfrvclim1  33545  ballotlem2  33556  ballotlemfc0  33560  ballotlemfcc  33561  signsvf0  33660  hgt750leme  33739  subfac1  34238  subfacp1lem1  34239  subfacp1lem2a  34240  subfacp1lem5  34244  subfacp1lem6  34245  cvmliftlem10  34354  divcnvlin  34777  faclimlem1  34788  fwddifnp1  35212  irrdiff  36299  poimirlem3  36583  poimirlem4  36584  poimirlem16  36596  poimirlem17  36597  poimirlem19  36599  poimirlem20  36600  poimirlem24  36604  poimirlem27  36607  poimirlem28  36608  poimirlem31  36611  poimirlem32  36612  mblfinlem1  36617  mblfinlem2  36618  ovoliunnfl  36622  voliunnfl  36624  fdc  36705  heibor1lem  36769  rrncmslem  36792  lcmfunnnd  40969  lcm1un  40970  lcm2un  40971  lcmineqlem11  40996  lcmineqlem19  41004  aks4d1p1p2  41027  nn0rppwr  41312  nn0expgcd  41314  mapfzcons  41542  mzpexpmpt  41571  eldioph3b  41591  fz1eqin  41595  diophin  41598  diophun  41599  0dioph  41604  elnnrabdioph  41633  rabren3dioph  41641  irrapxlem1  41648  irrapxlem3  41650  rmxyadd  41748  rmxy1  41749  rmxy0  41750  rmxp1  41759  rmyp1  41760  rmxm1  41761  rmym1  41762  jm2.24nn  41786  acongeq  41810  jm2.23  41823  jm2.15nn0  41830  jm2.16nn0  41831  jm2.27c  41834  jm2.27dlem2  41837  rmydioph  41841  rmxdioph  41843  expdiophlem2  41849  expdioph  41850  mpaaeu  41980  trclfvdecomr  42567  k0004val0  42993  hashnzfzclim  43169  sumsnd  43798  fmuldfeq  44384  stoweidlem3  44804  stoweidlem20  44821  stoweidlem34  44835  wallispilem4  44869  wallispi2lem1  44872  wallispi2lem2  44873  stirlinglem11  44885  dirkerper  44897  dirkertrigeqlem1  44899  dirkertrigeqlem3  44901  fourierdlem47  44954  fourierswlem  45031  smfmullem4  45595  natlocalincr  45675  tworepnotupword  45685  1oddALTV  46443  1nevenALTV  46444  2evenALTV  46445  nnsum3primes4  46541  nnsum3primesprm  46543  nnsum3primesgbe  46545  nnsum4primesodd  46549  nnsum4primesoddALTV  46550  nnsum4primeseven  46553  nnsum4primesevenALTV  46554  tgblthelfgott  46568  1odd  46666  pzriprnglem7  46896  pzriprnglem9  46898  pzriprnglem12  46901  pzriprnglem13  46902  pzriprnglem14  46903  pzriprng1ALT  46905  altgsumbcALT  47114  zlmodzxzsubm  47120  blen2  47355  blennngt2o2  47362  nn0sumshdiglemA  47389  nn0sumshdiglemB  47390