Theorem 1z 12673

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

Syntax hints:   ∈ wcel 2108  1c1 11185  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-z 12640

This theorem is referenced by:  1zzd  12674  peano2z  12684  peano2zm  12686  3halfnz  12722  peano5uzti  12733  nnuz  12946  eluz2nn  12949  eluzge3nn  12955  1eluzge0  12957  2eluzge1  12959  eluz2b1  12984  uz2m1nn  12988  nninf  12994  nnrecq  13037  qbtwnxr  13262  fz1n  13602  fz10  13605  fz01en  13612  fznatpl1  13638  fz12pr  13641  fztpval  13646  fseq1p1m1  13658  elfzp1b  13661  elfzm1b  13662  4fvwrd4  13705  ige2m2fzo  13779  fz0add1fz1  13786  fzo12sn  13799  fzo13pr  13800  fzo1to4tp  13804  fzofzp1  13814  fzostep1  13833  flge1nn  13872  fldiv4p1lem1div2  13886  modid0  13948  nnnfi  14017  fzennn  14019  fzen2  14020  f13idfv  14051  ser1const  14109  exp1  14118  zexpcl  14127  qexpcl  14128  qexpclz  14132  m1expcl  14137  expp1z  14162  expm1  14163  facnn  14324  fac0  14325  fac1  14326  bcn1  14362  bcpasc  14370  bcnm1  14376  hashsng  14418  hashfz  14476  fz1isolem  14510  seqcoll  14513  hashge2el2difr  14530  ccat2s1p2  14678  s2f1o  14965  f1oun2prg  14966  swrd2lsw  15001  2swrd2eqwrdeq  15002  relexp1g  15075  climuni  15598  isercoll2  15717  iseraltlem1  15730  sum0  15769  sumsnf  15791  climcndslem1  15897  climcndslem2  15898  divcnvshft  15903  supcvg  15904  prod0  15991  prodsn  16010  prodsnf  16012  zrisefaccl  16068  zfallfaccl  16069  sin01gt0  16238  rpnnen2lem10  16271  nthruc  16300  iddvds  16318  1dvds  16319  dvdsle  16358  dvds1  16367  3dvds  16379  n2dvds1  16416  divalglem5  16445  divalg  16451  bitsfzolem  16480  gcdcllem1  16545  gcdcllem3  16547  gcdaddmlem  16570  gcdadd  16572  gcdid  16573  gcd1  16574  1gcd  16580  bezoutlem1  16586  nn0rppwr  16608  nn0expgcd  16611  lcmgcdlem  16653  lcm1  16657  3lcm2e6woprm  16662  lcmfunsnlem  16688  isprm3  16730  ge2nprmge4  16748  phicl2  16815  phi1  16820  dfphi2  16821  eulerthlem2  16829  prmdiv  16832  prmdiveq  16833  odzcllem  16839  oddprm  16857  pythagtriplem4  16866  pcpre1  16889  pc1  16902  pcrec  16905  pcmpt  16939  fldivp1  16944  expnprm  16949  pockthlem  16952  unbenlem  16955  prmreclem2  16964  prmrec  16969  igz  16981  4sqlem12  17003  4sqlem13  17004  4sqlem19  17010  vdwlem8  17035  vdwlem13  17040  prmo1  17084  fvprmselgcd1  17092  prmlem0  17153  1259lem4  17181  2503lem2  17185  4001lem1  17188  setsstruct  17223  gsumpropd2lem  18717  efmnd1hash  18927  mulgfval  19109  mulg1  19121  mulgm1  19134  mulgp1  19147  mulgneg2  19148  cycsubgcl  19246  odinv  19603  efgs1b  19778  lt6abl  19937  pgpfac1lem2  20119  srgbinomlem4  20256  qsubdrg  21460  zsubrg  21461  gzsubrg  21462  zringmulg  21490  zringcyg  21503  mulgrhm  21511  mulgrhm2  21512  pzriprnglem7  21521  pzriprnglem9  21523  pzriprnglem12  21526  pzriprnglem13  21527  pzriprnglem14  21528  pzriprng1ALT  21530  fermltlchr  21567  chrnzr  21568  frgpcyg  21615  zrhpsgnmhm  21625  zrhpsgnodpm  21633  m2detleiblem1  22651  m2detleiblem2  22655  zfbas  23925  imasdsf1olem  24404  cphipval  25296  cmetcaulem  25341  bcthlem5  25381  ehl1eudis  25473  ovolctb  25544  ovolunlem1a  25550  ovolunlem1  25551  ovoliunnul  25561  ovolicc1  25570  ovolicc2lem4  25574  voliunlem1  25604  volsup  25610  uniioombllem6  25642  vitalilem5  25666  plyeq0lem  26269  vieta1lem2  26371  elqaalem2  26380  qaa  26383  iaa  26385  abelthlem6  26498  abelthlem9  26502  sin2pim  26545  cos2pim  26546  logbleb  26844  logblt  26845  1cubrlem  26902  leibpilem2  27002  emcllem5  27061  emcllem7  27063  lgamgulm2  27097  lgamcvglem  27101  gamcvg2lem  27120  lgam1  27125  wilthlem2  27130  wilthlem3  27131  ppip1le  27222  ppi1  27225  cht1  27226  chp1  27228  cht2  27233  ppieq0  27237  ppiub  27266  chpeq0  27270  chpchtsum  27281  chpub  27282  logfacbnd3  27285  logexprlim  27287  bposlem1  27346  bposlem2  27347  bposlem5  27350  bposlem6  27351  lgslem2  27360  lgsfcl2  27365  lgsval2lem  27369  lgsdir2lem1  27387  lgsdir2lem5  27391  1lgs  27402  lgsdchr  27417  lgsquad2lem2  27447  2sqlem9  27489  2sqlem10  27490  2sqblem  27493  2sqb  27494  dchrisumlem3  27553  log2sumbnd  27606  qabvle  27687  ostth3  27700  istrkg3ld  28487  tgldimor  28528  axlowdimlem3  28977  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  usgrexmpldifpr  29293  uhgrwkspthlem2  29790  pthdlem2  29804  0ewlk  30146  0pth  30157  1wlkdlem1  30169  ntrl2v2e  30190  eupth2lem3lem4  30263  ex-fl  30479  ipval2  30739  hlim0  31267  opsqrlem2  32173  iuninc  32583  nndiffz1  32791  fzom1ne1  32806  0dp2dp  32873  cshw1s2  32927  chnub  32984  cycpmco2lem4  33122  1fldgenq  33289  znfermltl  33359  zringfrac  33547  lmatfvlem  33761  mdetpmtr1  33769  mdetpmtr12  33771  lmlim  33893  qqh0  33930  qqh1  33931  esumfzf  34033  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  esumcvgsum  34052  esumsup  34053  dya2ub  34235  rrvsum  34419  dstfrvclim1  34442  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  signsvf0  34557  hgt750leme  34635  subfac1  35146  subfacp1lem1  35147  subfacp1lem2a  35148  subfacp1lem5  35152  subfacp1lem6  35153  cvmliftlem10  35262  divcnvlin  35695  faclimlem1  35705  fwddifnp1  36129  irrdiff  37292  poimirlem3  37583  poimirlem4  37584  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  mblfinlem1  37617  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  fdc  37705  heibor1lem  37769  rrncmslem  37792  lcmfunnnd  41969  lcm1un  41970  lcm2un  41971  lcmineqlem11  41996  lcmineqlem19  42004  aks4d1p1p2  42027  mapfzcons  42672  mzpexpmpt  42701  eldioph3b  42721  fz1eqin  42725  diophin  42728  diophun  42729  0dioph  42734  elnnrabdioph  42763  rabren3dioph  42771  irrapxlem1  42778  irrapxlem3  42780  rmxyadd  42878  rmxy1  42879  rmxy0  42880  rmxp1  42889  rmyp1  42890  rmxm1  42891  rmym1  42892  jm2.24nn  42916  acongeq  42940  jm2.23  42953  jm2.15nn0  42960  jm2.16nn0  42961  jm2.27c  42964  jm2.27dlem2  42967  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  mpaaeu  43107  trclfvdecomr  43690  k0004val0  44116  hashnzfzclim  44291  sumsnd  44926  fmuldfeq  45504  stoweidlem3  45924  stoweidlem20  45941  stoweidlem34  45955  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem11  46005  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  fourierdlem47  46074  fourierswlem  46151  smfmullem4  46715  natlocalincr  46795  tworepnotupword  46805  1oddALTV  47564  1nevenALTV  47565  2evenALTV  47566  nnsum3primes4  47662  nnsum3primesprm  47664  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  tgblthelfgott  47689  1odd  47894  altgsumbcALT  48078  zlmodzxzsubm  48084  blen2  48319  blennngt2o2  48326  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354