Theorem 1z 12533

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

Syntax hints:   ∈ wcel 2114  1c1 11039  ℤcz 12500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-z 12501

This theorem is referenced by:  1zzd  12534  peano2z  12544  peano2zm  12546  3halfnz  12583  peano5uzti  12594  nnuz  12802  1eluzge0  12805  2eluzge1  12807  eluz2nn  12813  eluz2b1  12844  uz2m1nn  12848  nninf  12854  nnrecq  12897  qbtwnxr  13127  fz1n  13470  fz10  13473  fz01en  13480  fznatpl1  13506  fz12pr  13509  fztpval  13514  fseq1p1m1  13526  elfzp1b  13529  elfzm1b  13530  4fvwrd4  13576  fzo1lb  13641  ige2m2fzo  13656  fz0add1fz1  13663  fzo12sn  13676  fzo13pr  13677  fzo1to4tp  13682  fzofzp1  13692  fzom1ne1  13713  fzostep1  13714  flge1nn  13753  fldiv4p1lem1div2  13767  modid0  13829  nnnfi  13901  fzennn  13903  fzen2  13904  f13idfv  13935  ser1const  13993  exp1  14002  zexpcl  14011  qexpcl  14012  qexpclz  14016  m1expcl  14021  expp1z  14046  expm1  14047  facnn  14210  fac0  14211  fac1  14212  bcn1  14248  bcpasc  14256  bcnm1  14262  hashsng  14304  hashfz  14362  fz1isolem  14396  seqcoll  14399  hashge2el2difr  14416  ccat2s1p2  14566  s2f1o  14851  f1oun2prg  14852  swrd2lsw  14887  2swrd2eqwrdeq  14888  relexp1g  14961  climuni  15487  isercoll2  15604  iseraltlem1  15617  sum0  15656  sumsnf  15678  climcndslem1  15784  climcndslem2  15785  divcnvshft  15790  supcvg  15791  prod0  15878  prodsn  15897  prodsnf  15899  zrisefaccl  15955  zfallfaccl  15956  sin01gt0  16127  rpnnen2lem10  16160  nthruc  16189  iddvds  16208  1dvds  16209  dvdsle  16249  dvds1  16258  3dvds  16270  n2dvds1  16307  divalglem5  16336  divalg  16342  bitsfzolem  16373  gcdcllem1  16438  gcdcllem3  16440  gcdaddmlem  16463  gcdadd  16465  gcdid  16466  gcd1  16467  1gcd  16472  bezoutlem1  16478  nn0rppwr  16500  nn0expgcd  16503  lcmgcdlem  16545  lcm1  16549  3lcm2e6woprm  16554  lcmfunsnlem  16580  isprm3  16622  ge2nprmge4  16640  phicl2  16707  phi1  16712  dfphi2  16713  eulerthlem2  16721  prmdiv  16724  prmdiveq  16725  odzcllem  16732  oddprm  16750  pythagtriplem4  16759  pcpre1  16782  pc1  16795  pcrec  16798  pcmpt  16832  fldivp1  16837  expnprm  16842  pockthlem  16845  unbenlem  16848  prmreclem2  16857  prmrec  16862  igz  16874  4sqlem12  16896  4sqlem13  16897  4sqlem19  16903  vdwlem8  16928  vdwlem13  16933  prmo1  16977  fvprmselgcd1  16985  prmlem0  17045  1259lem4  17073  2503lem2  17077  4001lem1  17080  setsstruct  17115  chnub  18557  gsumpropd2lem  18616  efmnd1hash  18829  mulgfval  19011  mulg1  19023  mulgm1  19036  mulgp1  19049  mulgneg2  19050  cycsubgcl  19147  odinv  19502  efgs1b  19677  lt6abl  19836  pgpfac1lem2  20018  srgbinomlem4  20176  qsubdrg  21386  zsubrg  21387  gzsubrg  21388  zringmulg  21423  zringcyg  21436  mulgrhm  21444  mulgrhm2  21445  pzriprnglem7  21454  pzriprnglem9  21456  pzriprnglem12  21459  pzriprnglem13  21460  pzriprnglem14  21461  pzriprng1ALT  21463  fermltlchr  21496  chrnzr  21497  frgpcyg  21540  zrhpsgnmhm  21551  zrhpsgnodpm  21559  m2detleiblem1  22580  m2detleiblem2  22584  zfbas  23852  imasdsf1olem  24329  cphipval  25211  cmetcaulem  25256  bcthlem5  25296  ehl1eudis  25388  ovolctb  25459  ovolunlem1a  25465  ovolunlem1  25466  ovoliunnul  25476  ovolicc1  25485  ovolicc2lem4  25489  voliunlem1  25519  volsup  25525  uniioombllem6  25557  vitalilem5  25581  plyeq0lem  26183  vieta1lem2  26287  elqaalem2  26296  qaa  26299  iaa  26301  abelthlem6  26414  abelthlem9  26418  sin2pim  26462  cos2pim  26463  logbleb  26761  logblt  26762  1cubrlem  26819  leibpilem2  26919  emcllem5  26978  emcllem7  26980  lgamgulm2  27014  lgamcvglem  27018  gamcvg2lem  27037  lgam1  27042  wilthlem2  27047  wilthlem3  27048  ppip1le  27139  ppi1  27142  cht1  27143  chp1  27145  cht2  27150  ppieq0  27154  ppiub  27183  chpeq0  27187  chpchtsum  27198  chpub  27199  logfacbnd3  27202  logexprlim  27204  bposlem1  27263  bposlem2  27264  bposlem5  27267  bposlem6  27268  lgslem2  27277  lgsfcl2  27282  lgsval2lem  27286  lgsdir2lem1  27304  lgsdir2lem5  27308  1lgs  27319  lgsdchr  27334  lgsquad2lem2  27364  2sqlem9  27406  2sqlem10  27407  2sqblem  27410  2sqb  27411  dchrisumlem3  27470  log2sumbnd  27523  qabvle  27604  ostth3  27617  istrkg3ld  28545  tgldimor  28586  axlowdimlem3  29029  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  usgrexmpldifpr  29343  dfpth2  29814  uhgrwkspthlem2  29839  pthdlem2  29853  0ewlk  30201  0pth  30212  1wlkdlem1  30224  ntrl2v2e  30245  eupth2lem3lem4  30318  ex-fl  30534  ipval2  30794  hlim0  31322  opsqrlem2  32228  iuninc  32646  nndiffz1  32876  0dp2dp  33000  cshw1s2  33052  cycpmco2lem4  33222  1fldgenq  33415  znfermltl  33458  zringfrac  33646  constrextdg2  33926  cos9thpiminplylem5  33963  lmatfvlem  33992  mdetpmtr1  34000  mdetpmtr12  34002  lmlim  34124  qqh0  34161  qqh1  34162  esumfzf  34246  esumfsup  34247  esumpcvgval  34255  esumcvg  34263  esumcvgsum  34265  esumsup  34266  dya2ub  34447  rrvsum  34631  dstfrvclim1  34655  ballotlem2  34666  ballotlemfc0  34670  ballotlemfcc  34671  signsvf0  34757  hgt750leme  34835  subfac1  35391  subfacp1lem1  35392  subfacp1lem2a  35393  subfacp1lem5  35397  subfacp1lem6  35398  cvmliftlem10  35507  divcnvlin  35946  faclimlem1  35956  fwddifnp1  36378  irrdiff  37575  poimirlem3  37868  poimirlem4  37869  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem24  37889  poimirlem27  37892  poimirlem28  37893  poimirlem31  37896  poimirlem32  37897  mblfinlem1  37902  mblfinlem2  37903  ovoliunnfl  37907  voliunnfl  37909  fdc  37990  heibor1lem  38054  rrncmslem  38077  lcmfunnnd  42376  lcm1un  42377  lcm2un  42378  lcmineqlem11  42403  lcmineqlem19  42411  aks4d1p1p2  42434  mapfzcons  43067  mzpexpmpt  43096  eldioph3b  43116  fz1eqin  43120  diophin  43123  diophun  43124  0dioph  43129  elnnrabdioph  43158  rabren3dioph  43166  irrapxlem1  43173  irrapxlem3  43175  rmxyadd  43272  rmxy1  43273  rmxy0  43274  rmxp1  43283  rmyp1  43284  rmxm1  43285  rmym1  43286  jm2.24nn  43310  acongeq  43334  jm2.23  43347  jm2.15nn0  43354  jm2.16nn0  43355  jm2.27c  43358  jm2.27dlem2  43361  rmydioph  43365  rmxdioph  43367  expdiophlem2  43373  expdioph  43374  mpaaeu  43501  trclfvdecomr  44078  k0004val0  44504  hashnzfzclim  44672  sumsnd  45380  fmuldfeq  45937  stoweidlem3  46355  stoweidlem20  46372  stoweidlem34  46386  wallispilem4  46420  wallispi2lem1  46423  wallispi2lem2  46424  stirlinglem11  46436  dirkerper  46448  dirkertrigeqlem1  46450  dirkertrigeqlem3  46452  fourierdlem47  46505  fourierswlem  46582  smfmullem4  47146  ormklocald  47226  natlocalincr  47228  nthrucw  47238  ceilhalf1  47688  1oddALTV  48044  1nevenALTV  48045  2evenALTV  48046  nnsum3primes4  48142  nnsum3primesprm  48144  nnsum3primesgbe  48146  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  tgblthelfgott  48169  stgr1  48315  gpgusgralem  48410  1odd  48525  altgsumbcALT  48707  zlmodzxzsubm  48713  blen2  48939  blennngt2o2  48946  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974