Theorem 1z 12647

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

Syntax hints:   ∈ wcel 2108  1c1 11156  ℤcz 12613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-z 12614

This theorem is referenced by:  1zzd  12648  peano2z  12658  peano2zm  12660  3halfnz  12697  peano5uzti  12708  nnuz  12921  eluz2nn  12924  eluzge3nn  12932  1eluzge0  12934  2eluzge1  12936  eluz2b1  12961  uz2m1nn  12965  nninf  12971  nnrecq  13014  qbtwnxr  13242  fz1n  13582  fz10  13585  fz01en  13592  fznatpl1  13618  fz12pr  13621  fztpval  13626  fseq1p1m1  13638  elfzp1b  13641  elfzm1b  13642  4fvwrd4  13688  fzo1lb  13753  ige2m2fzo  13767  fz0add1fz1  13774  fzo12sn  13787  fzo13pr  13788  fzo1to4tp  13793  fzofzp1  13803  fzostep1  13822  flge1nn  13861  fldiv4p1lem1div2  13875  modid0  13937  nnnfi  14007  fzennn  14009  fzen2  14010  f13idfv  14041  ser1const  14099  exp1  14108  zexpcl  14117  qexpcl  14118  qexpclz  14122  m1expcl  14127  expp1z  14152  expm1  14153  facnn  14314  fac0  14315  fac1  14316  bcn1  14352  bcpasc  14360  bcnm1  14366  hashsng  14408  hashfz  14466  fz1isolem  14500  seqcoll  14503  hashge2el2difr  14520  ccat2s1p2  14668  s2f1o  14955  f1oun2prg  14956  swrd2lsw  14991  2swrd2eqwrdeq  14992  relexp1g  15065  climuni  15588  isercoll2  15705  iseraltlem1  15718  sum0  15757  sumsnf  15779  climcndslem1  15885  climcndslem2  15886  divcnvshft  15891  supcvg  15892  prod0  15979  prodsn  15998  prodsnf  16000  zrisefaccl  16056  zfallfaccl  16057  sin01gt0  16226  rpnnen2lem10  16259  nthruc  16288  iddvds  16307  1dvds  16308  dvdsle  16347  dvds1  16356  3dvds  16368  n2dvds1  16405  divalglem5  16434  divalg  16440  bitsfzolem  16471  gcdcllem1  16536  gcdcllem3  16538  gcdaddmlem  16561  gcdadd  16563  gcdid  16564  gcd1  16565  1gcd  16570  bezoutlem1  16576  nn0rppwr  16598  nn0expgcd  16601  lcmgcdlem  16643  lcm1  16647  3lcm2e6woprm  16652  lcmfunsnlem  16678  isprm3  16720  ge2nprmge4  16738  phicl2  16805  phi1  16810  dfphi2  16811  eulerthlem2  16819  prmdiv  16822  prmdiveq  16823  odzcllem  16830  oddprm  16848  pythagtriplem4  16857  pcpre1  16880  pc1  16893  pcrec  16896  pcmpt  16930  fldivp1  16935  expnprm  16940  pockthlem  16943  unbenlem  16946  prmreclem2  16955  prmrec  16960  igz  16972  4sqlem12  16994  4sqlem13  16995  4sqlem19  17001  vdwlem8  17026  vdwlem13  17031  prmo1  17075  fvprmselgcd1  17083  prmlem0  17143  1259lem4  17171  2503lem2  17175  4001lem1  17178  setsstruct  17213  gsumpropd2lem  18692  efmnd1hash  18905  mulgfval  19087  mulg1  19099  mulgm1  19112  mulgp1  19125  mulgneg2  19126  cycsubgcl  19224  odinv  19579  efgs1b  19754  lt6abl  19913  pgpfac1lem2  20095  srgbinomlem4  20226  qsubdrg  21437  zsubrg  21438  gzsubrg  21439  zringmulg  21467  zringcyg  21480  mulgrhm  21488  mulgrhm2  21489  pzriprnglem7  21498  pzriprnglem9  21500  pzriprnglem12  21503  pzriprnglem13  21504  pzriprnglem14  21505  pzriprng1ALT  21507  fermltlchr  21544  chrnzr  21545  frgpcyg  21592  zrhpsgnmhm  21602  zrhpsgnodpm  21610  m2detleiblem1  22630  m2detleiblem2  22634  zfbas  23904  imasdsf1olem  24383  cphipval  25277  cmetcaulem  25322  bcthlem5  25362  ehl1eudis  25454  ovolctb  25525  ovolunlem1a  25531  ovolunlem1  25532  ovoliunnul  25542  ovolicc1  25551  ovolicc2lem4  25555  voliunlem1  25585  volsup  25591  uniioombllem6  25623  vitalilem5  25647  plyeq0lem  26249  vieta1lem2  26353  elqaalem2  26362  qaa  26365  iaa  26367  abelthlem6  26480  abelthlem9  26484  sin2pim  26527  cos2pim  26528  logbleb  26826  logblt  26827  1cubrlem  26884  leibpilem2  26984  emcllem5  27043  emcllem7  27045  lgamgulm2  27079  lgamcvglem  27083  gamcvg2lem  27102  lgam1  27107  wilthlem2  27112  wilthlem3  27113  ppip1le  27204  ppi1  27207  cht1  27208  chp1  27210  cht2  27215  ppieq0  27219  ppiub  27248  chpeq0  27252  chpchtsum  27263  chpub  27264  logfacbnd3  27267  logexprlim  27269  bposlem1  27328  bposlem2  27329  bposlem5  27332  bposlem6  27333  lgslem2  27342  lgsfcl2  27347  lgsval2lem  27351  lgsdir2lem1  27369  lgsdir2lem5  27373  1lgs  27384  lgsdchr  27399  lgsquad2lem2  27429  2sqlem9  27471  2sqlem10  27472  2sqblem  27475  2sqb  27476  dchrisumlem3  27535  log2sumbnd  27588  qabvle  27669  ostth3  27682  istrkg3ld  28469  tgldimor  28510  axlowdimlem3  28959  axlowdimlem6  28962  axlowdimlem7  28963  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  usgrexmpldifpr  29275  dfpth2  29749  uhgrwkspthlem2  29774  pthdlem2  29788  0ewlk  30133  0pth  30144  1wlkdlem1  30156  ntrl2v2e  30177  eupth2lem3lem4  30250  ex-fl  30466  ipval2  30726  hlim0  31254  opsqrlem2  32160  iuninc  32573  nndiffz1  32788  fzom1ne1  32803  0dp2dp  32891  cshw1s2  32945  chnub  33002  cycpmco2lem4  33149  1fldgenq  33324  znfermltl  33394  zringfrac  33582  constrextdg2  33790  lmatfvlem  33814  mdetpmtr1  33822  mdetpmtr12  33824  lmlim  33946  qqh0  33985  qqh1  33986  esumfzf  34070  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  esumcvgsum  34089  esumsup  34090  dya2ub  34272  rrvsum  34456  dstfrvclim1  34480  ballotlem2  34491  ballotlemfc0  34495  ballotlemfcc  34496  signsvf0  34595  hgt750leme  34673  subfac1  35183  subfacp1lem1  35184  subfacp1lem2a  35185  subfacp1lem5  35189  subfacp1lem6  35190  cvmliftlem10  35299  divcnvlin  35733  faclimlem1  35743  fwddifnp1  36166  irrdiff  37327  poimirlem3  37630  poimirlem4  37631  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  mblfinlem1  37664  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  fdc  37752  heibor1lem  37816  rrncmslem  37839  lcmfunnnd  42013  lcm1un  42014  lcm2un  42015  lcmineqlem11  42040  lcmineqlem19  42048  aks4d1p1p2  42071  mapfzcons  42727  mzpexpmpt  42756  eldioph3b  42776  fz1eqin  42780  diophin  42783  diophun  42784  0dioph  42789  elnnrabdioph  42818  rabren3dioph  42826  irrapxlem1  42833  irrapxlem3  42835  rmxyadd  42933  rmxy1  42934  rmxy0  42935  rmxp1  42944  rmyp1  42945  rmxm1  42946  rmym1  42947  jm2.24nn  42971  acongeq  42995  jm2.23  43008  jm2.15nn0  43015  jm2.16nn0  43016  jm2.27c  43019  jm2.27dlem2  43022  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  mpaaeu  43162  trclfvdecomr  43741  k0004val0  44167  hashnzfzclim  44341  sumsnd  45031  fmuldfeq  45598  stoweidlem3  46018  stoweidlem20  46035  stoweidlem34  46049  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem11  46099  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  fourierdlem47  46168  fourierswlem  46245  smfmullem4  46809  ormklocald  46889  natlocalincr  46891  tworepnotupword  46901  1oddALTV  47677  1nevenALTV  47678  2evenALTV  47679  nnsum3primes4  47775  nnsum3primesprm  47777  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  tgblthelfgott  47802  stgr1  47928  gpgusgralem  48011  1odd  48087  altgsumbcALT  48269  zlmodzxzsubm  48275  blen2  48506  blennngt2o2  48513  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541