Theorem 1z 12557

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

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

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-z 12525

This theorem is referenced by:  1zzd  12558  peano2z  12568  peano2zm  12570  3halfnz  12608  peano5uzti  12619  nnuz  12827  1eluzge0  12830  2eluzge1  12832  eluz2nn  12838  eluz2b1  12869  uz2m1nn  12873  nninf  12879  nnrecq  12922  qbtwnxr  13152  fz1n  13496  fz10  13499  fz01en  13506  fznatpl1  13532  fz12pr  13535  fztpval  13540  fseq1p1m1  13552  elfzp1b  13555  elfzm1b  13556  4fvwrd4  13602  fzo1lb  13668  ige2m2fzo  13683  fz0add1fz1  13690  fzo12sn  13703  fzo13pr  13704  fzo1to4tp  13709  fzofzp1  13719  fzom1ne1  13740  fzostep1  13741  flge1nn  13780  fldiv4p1lem1div2  13794  modid0  13856  nnnfi  13928  fzennn  13930  fzen2  13931  f13idfv  13962  ser1const  14020  exp1  14029  zexpcl  14038  qexpcl  14039  qexpclz  14043  m1expcl  14048  expp1z  14073  expm1  14074  facnn  14237  fac0  14238  fac1  14239  bcn1  14275  bcpasc  14283  bcnm1  14289  hashsng  14331  hashfz  14389  fz1isolem  14423  seqcoll  14426  hashge2el2difr  14443  ccat2s1p2  14593  s2f1o  14878  f1oun2prg  14879  swrd2lsw  14914  2swrd2eqwrdeq  14915  relexp1g  14988  climuni  15514  isercoll2  15631  iseraltlem1  15644  sum0  15683  sumsnf  15705  climcndslem1  15814  climcndslem2  15815  divcnvshft  15820  supcvg  15821  prod0  15908  prodsn  15927  prodsnf  15929  zrisefaccl  15985  zfallfaccl  15986  sin01gt0  16157  rpnnen2lem10  16190  nthruc  16219  iddvds  16238  1dvds  16239  dvdsle  16279  dvds1  16288  3dvds  16300  n2dvds1  16337  divalglem5  16366  divalg  16372  bitsfzolem  16403  gcdcllem1  16468  gcdcllem3  16470  gcdaddmlem  16493  gcdadd  16495  gcdid  16496  gcd1  16497  1gcd  16502  bezoutlem1  16508  nn0rppwr  16530  nn0expgcd  16533  lcmgcdlem  16575  lcm1  16579  3lcm2e6woprm  16584  lcmfunsnlem  16610  isprm3  16652  ge2nprmge4  16671  phicl2  16738  phi1  16743  dfphi2  16744  eulerthlem2  16752  prmdiv  16755  prmdiveq  16756  odzcllem  16763  oddprm  16781  pythagtriplem4  16790  pcpre1  16813  pc1  16826  pcrec  16829  pcmpt  16863  fldivp1  16868  expnprm  16873  pockthlem  16876  unbenlem  16879  prmreclem2  16888  prmrec  16893  igz  16905  4sqlem12  16927  4sqlem13  16928  4sqlem19  16934  vdwlem8  16959  vdwlem13  16964  prmo1  17008  fvprmselgcd1  17016  prmlem0  17076  1259lem4  17104  2503lem2  17108  4001lem1  17111  setsstruct  17146  chnub  18588  gsumpropd2lem  18647  efmnd1hash  18860  mulgfval  19045  mulg1  19057  mulgm1  19070  mulgp1  19083  mulgneg2  19084  cycsubgcl  19181  odinv  19536  efgs1b  19711  lt6abl  19870  pgpfac1lem2  20052  srgbinomlem4  20210  qsubdrg  21399  zsubrg  21400  gzsubrg  21401  zringmulg  21436  zringcyg  21449  mulgrhm  21457  mulgrhm2  21458  pzriprnglem7  21467  pzriprnglem9  21469  pzriprnglem12  21472  pzriprnglem13  21473  pzriprnglem14  21474  pzriprng1ALT  21476  fermltlchr  21509  chrnzr  21510  frgpcyg  21553  zrhpsgnmhm  21564  zrhpsgnodpm  21572  m2detleiblem1  22589  m2detleiblem2  22593  zfbas  23861  imasdsf1olem  24338  cphipval  25210  cmetcaulem  25255  bcthlem5  25295  ehl1eudis  25387  ovolctb  25457  ovolunlem1a  25463  ovolunlem1  25464  ovoliunnul  25474  ovolicc1  25483  ovolicc2lem4  25487  voliunlem1  25517  volsup  25523  uniioombllem6  25555  vitalilem5  25579  plyeq0lem  26175  vieta1lem2  26277  elqaalem2  26286  qaa  26289  iaa  26291  abelthlem6  26401  abelthlem9  26405  sin2pim  26449  cos2pim  26450  logbleb  26747  logblt  26748  1cubrlem  26805  leibpilem2  26905  emcllem5  26963  emcllem7  26965  lgamgulm2  26999  lgamcvglem  27003  gamcvg2lem  27022  lgam1  27027  wilthlem2  27032  wilthlem3  27033  ppip1le  27124  ppi1  27127  cht1  27128  chp1  27130  cht2  27135  ppieq0  27139  ppiub  27167  chpeq0  27171  chpchtsum  27182  chpub  27183  logfacbnd3  27186  logexprlim  27188  bposlem1  27247  bposlem2  27248  bposlem5  27251  bposlem6  27252  lgslem2  27261  lgsfcl2  27266  lgsval2lem  27270  lgsdir2lem1  27288  lgsdir2lem5  27292  1lgs  27303  lgsdchr  27318  lgsquad2lem2  27348  2sqlem9  27390  2sqlem10  27391  2sqblem  27394  2sqb  27395  dchrisumlem3  27454  log2sumbnd  27507  qabvle  27588  ostth3  27601  istrkg3ld  28529  tgldimor  28570  axlowdimlem3  29013  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  usgrexmpldifpr  29327  dfpth2  29797  uhgrwkspthlem2  29822  pthdlem2  29836  0ewlk  30184  0pth  30195  1wlkdlem1  30207  ntrl2v2e  30228  eupth2lem3lem4  30301  ex-fl  30517  ipval2  30778  hlim0  31306  opsqrlem2  32212  iuninc  32630  nndiffz1  32859  0dp2dp  32968  cshw1s2  33020  cycpmco2lem4  33190  1fldgenq  33383  znfermltl  33426  zringfrac  33614  constrextdg2  33893  cos9thpiminplylem5  33930  lmatfvlem  33959  mdetpmtr1  33967  mdetpmtr12  33969  lmlim  34091  qqh0  34128  qqh1  34129  esumfzf  34213  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  esumcvgsum  34232  esumsup  34233  dya2ub  34414  rrvsum  34598  dstfrvclim1  34622  ballotlem2  34633  ballotlemfc0  34637  ballotlemfcc  34638  signsvf0  34724  hgt750leme  34802  subfac1  35360  subfacp1lem1  35361  subfacp1lem2a  35362  subfacp1lem5  35366  subfacp1lem6  35367  cvmliftlem10  35476  divcnvlin  35915  faclimlem1  35925  fwddifnp1  36347  irrdiff  37640  qdiff  37641  poimirlem3  37944  poimirlem4  37945  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  poimirlem27  37968  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  mblfinlem1  37978  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  fdc  38066  heibor1lem  38130  rrncmslem  38153  lcmfunnnd  42451  lcm1un  42452  lcm2un  42453  lcmineqlem11  42478  lcmineqlem19  42486  aks4d1p1p2  42509  mapfzcons  43148  mzpexpmpt  43177  eldioph3b  43197  fz1eqin  43201  diophin  43204  diophun  43205  0dioph  43210  elnnrabdioph  43235  rabren3dioph  43243  irrapxlem1  43250  irrapxlem3  43252  rmxyadd  43349  rmxy1  43350  rmxy0  43351  rmxp1  43360  rmyp1  43361  rmxm1  43362  rmym1  43363  jm2.24nn  43387  acongeq  43411  jm2.23  43424  jm2.15nn0  43431  jm2.16nn0  43432  jm2.27c  43435  jm2.27dlem2  43438  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  mpaaeu  43578  trclfvdecomr  44155  k0004val0  44581  hashnzfzclim  44749  sumsnd  45457  fmuldfeq  46013  stoweidlem3  46431  stoweidlem20  46448  stoweidlem34  46462  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem11  46512  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  fourierdlem47  46581  fourierswlem  46658  smfmullem4  47222  ormklocald  47304  natlocalincr  47306  nthrucw  47316  ceilhalf1  47786  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  ppivalnn  48095  1oddALTV  48166  1nevenALTV  48167  2evenALTV  48168  nnsum3primes4  48264  nnsum3primesprm  48266  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  tgblthelfgott  48291  stgr1  48437  gpgusgralem  48532  1odd  48647  altgsumbcALT  48829  zlmodzxzsubm  48835  blen2  49061  blennngt2o2  49068  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096