Theorem 1z 12013

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

Syntax hints:   ∈ wcel 2114  1c1 10538  ℤcz 11982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-neg 10873  df-nn 11639  df-z 11983

This theorem is referenced by:  1zzd  12014  peano2z  12024  peano2zm  12026  3halfnz  12062  peano5uzti  12073  nnuz  12282  eluz2nn  12285  eluzge3nn  12291  1eluzge0  12293  2eluzge1  12295  eluz2b1  12320  uz2m1nn  12324  nninf  12330  nnrecq  12372  qbtwnxr  12594  fz1n  12926  fz10  12929  fz01en  12936  fznatpl1  12962  fz12pr  12965  fztpval  12970  fseq1p1m1  12982  elfzp1b  12985  elfzm1b  12986  4fvwrd4  13028  ige2m2fzo  13101  fz0add1fz1  13108  fzo12sn  13121  fzo13pr  13122  fzo1to4tp  13126  fzofzp1  13135  fzostep1  13154  flge1nn  13192  fldiv4p1lem1div2  13206  modid0  13266  nnnfi  13335  fzennn  13337  fzen2  13338  f13idfv  13369  ser1const  13427  exp1  13436  zexpcl  13445  qexpcl  13446  qexpclz  13451  m1expcl  13453  expp1z  13479  expm1  13480  facnn  13636  fac0  13637  fac1  13638  bcn1  13674  bcpasc  13682  bcnm1  13688  hashsng  13731  hashfz  13789  fz1isolem  13820  seqcoll  13823  hashge2el2difr  13840  ccat2s1p2  13986  ccat2s1p2OLD  13988  s2f1o  14278  f1oun2prg  14279  swrd2lsw  14314  2swrd2eqwrdeq  14315  relexp1g  14385  climuni  14909  isercoll2  15025  iseraltlem1  15038  sum0  15078  sumsnf  15099  climcndslem1  15204  climcndslem2  15205  divcnvshft  15210  supcvg  15211  prod0  15297  prodsn  15316  prodsnf  15318  zrisefaccl  15374  zfallfaccl  15375  sin01gt0  15543  rpnnen2lem10  15576  nthruc  15605  iddvds  15623  1dvds  15624  dvdsle  15660  dvds1  15669  3dvds  15680  n2dvds1  15717  divalglem5  15748  divalg  15754  bitsfzolem  15783  gcdcllem1  15848  gcdcllem3  15850  gcdaddmlem  15872  gcdadd  15874  gcdid  15875  gcd1  15876  1gcd  15881  bezoutlem1  15887  gcdmultipleOLD  15900  lcmgcdlem  15950  lcm1  15954  3lcm2e6woprm  15959  lcmfunsnlem  15985  isprm3  16027  ge2nprmge4  16045  phicl2  16105  phi1  16110  dfphi2  16111  eulerthlem2  16119  prmdiv  16122  prmdiveq  16123  odzcllem  16129  oddprm  16147  pythagtriplem4  16156  pcpre1  16179  pc1  16192  pcrec  16195  pcmpt  16228  fldivp1  16233  expnprm  16238  pockthlem  16241  unbenlem  16244  prmreclem2  16253  prmrec  16258  igz  16270  4sqlem12  16292  4sqlem13  16293  4sqlem19  16299  vdwlem8  16324  vdwlem13  16329  prmo1  16373  fvprmselgcd1  16381  prmgaplem7  16393  prmlem0  16439  1259lem4  16467  2503lem2  16471  4001lem1  16474  setsstruct  16523  gsumpropd2lem  17889  efmnd1hash  18057  mulgfval  18226  mulg1  18235  mulgm1  18248  mulgp1  18260  mulgneg2  18261  cycsubgcl  18349  odinv  18688  efgs1b  18862  lt6abl  19015  pgpfac1lem2  19197  srgbinomlem4  19293  qsubdrg  20597  zsubrg  20598  gzsubrg  20599  zringmulg  20625  zringcyg  20638  mulgrhm  20645  mulgrhm2  20646  chrnzr  20677  frgpcyg  20720  zrhpsgnmhm  20728  zrhpsgnodpm  20736  m2detleiblem1  21233  m2detleiblem2  21237  zfbas  22504  imasdsf1olem  22983  cphipval  23846  cmetcaulem  23891  bcthlem5  23931  ehl1eudis  24023  ovolctb  24091  ovolunlem1a  24097  ovolunlem1  24098  ovoliunnul  24108  ovolicc1  24117  ovolicc2lem4  24121  voliunlem1  24151  volsup  24157  uniioombllem6  24189  vitalilem5  24213  plyeq0lem  24800  vieta1lem2  24900  elqaalem2  24909  qaa  24912  iaa  24914  abelthlem6  25024  abelthlem9  25028  sin2pim  25071  cos2pim  25072  logbleb  25361  logblt  25362  1cubrlem  25419  leibpilem2  25519  emcllem5  25577  emcllem7  25579  lgamgulm2  25613  lgamcvglem  25617  gamcvg2lem  25636  lgam1  25641  wilthlem2  25646  wilthlem3  25647  ppip1le  25738  ppi1  25741  cht1  25742  chp1  25744  cht2  25749  ppieq0  25753  ppiub  25780  chpeq0  25784  chpchtsum  25795  chpub  25796  logfacbnd3  25799  logexprlim  25801  bposlem1  25860  bposlem2  25861  bposlem5  25864  bposlem6  25865  lgslem2  25874  lgsfcl2  25879  lgsval2lem  25883  lgsdir2lem1  25901  lgsdir2lem5  25905  1lgs  25916  lgsdchr  25931  lgsquad2lem2  25961  2sqlem9  26003  2sqlem10  26004  2sqblem  26007  2sqb  26008  dchrisumlem3  26067  log2sumbnd  26120  qabvle  26201  ostth3  26214  istrkg3ld  26247  tgldimor  26288  axlowdimlem3  26730  axlowdimlem6  26733  axlowdimlem7  26734  axlowdimlem16  26743  axlowdimlem17  26744  axlowdim  26747  usgrexmpldifpr  27040  uhgrwkspthlem2  27535  pthdlem2  27549  0ewlk  27893  0pth  27904  1wlkdlem1  27916  ntrl2v2e  27937  eupth2lem3lem4  28010  ex-fl  28226  ipval2  28484  hlim0  29012  opsqrlem2  29918  iuninc  30312  nndiffz1  30509  fzom1ne1  30524  0dp2dp  30585  cshw1s2  30634  cycpmco2lem4  30771  lmatfvlem  31080  mdetpmtr1  31088  mdetpmtr12  31090  lmlim  31190  qqh0  31225  qqh1  31226  esumfzf  31328  esumfsup  31329  esumpcvgval  31337  esumcvg  31345  esumcvgsum  31347  esumsup  31348  dya2ub  31528  rrvsum  31712  dstfrvclim1  31735  ballotlem2  31746  ballotlemfc0  31750  ballotlemfcc  31751  signsvf0  31850  hgt750leme  31929  subfac1  32425  subfacp1lem1  32426  subfacp1lem2a  32427  subfacp1lem5  32431  subfacp1lem6  32432  cvmliftlem10  32541  divcnvlin  32964  faclimlem1  32975  fwddifnp1  33626  poimirlem3  34910  poimirlem4  34911  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem24  34931  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  poimirlem32  34939  mblfinlem1  34944  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  fdc  35035  heibor1lem  35102  rrncmslem  35125  nn0rppwr  39202  nn0expgcd  39204  mapfzcons  39333  mzpexpmpt  39362  eldioph3b  39382  fz1eqin  39386  diophin  39389  diophun  39390  0dioph  39395  elnnrabdioph  39424  rabren3dioph  39432  irrapxlem1  39439  irrapxlem3  39441  rmxyadd  39538  rmxy1  39539  rmxy0  39540  rmxp1  39549  rmyp1  39550  rmxm1  39551  rmym1  39552  jm2.24nn  39576  acongeq  39600  jm2.23  39613  jm2.15nn0  39620  jm2.16nn0  39621  jm2.27c  39624  jm2.27dlem2  39627  rmydioph  39631  rmxdioph  39633  expdiophlem2  39639  expdioph  39640  mpaaeu  39770  trclfvdecomr  40093  k0004val0  40524  hashnzfzclim  40674  sumsnd  41303  fmuldfeq  41884  stoweidlem3  42308  stoweidlem20  42325  stoweidlem34  42339  wallispilem4  42373  wallispi2lem1  42376  wallispi2lem2  42377  stirlinglem11  42389  dirkerper  42401  dirkertrigeqlem1  42403  dirkertrigeqlem3  42405  fourierdlem47  42458  fourierswlem  42535  smfmullem4  43089  1oddALTV  43875  1nevenALTV  43876  2evenALTV  43877  nnsum3primes4  43973  nnsum3primesprm  43975  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  tgblthelfgott  44000  1odd  44098  altgsumbcALT  44421  zlmodzxzsubm  44427  blen2  44665  blennngt2o2  44672  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700