Theorem 1z 12333

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

Syntax hints:   ∈ wcel 2109  1c1 10856  ℤcz 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-neg 11191  df-nn 11957  df-z 12303

This theorem is referenced by:  1zzd  12334  peano2z  12344  peano2zm  12346  3halfnz  12382  peano5uzti  12393  nnuz  12603  eluz2nn  12606  eluzge3nn  12612  1eluzge0  12614  2eluzge1  12616  eluz2b1  12641  uz2m1nn  12645  nninf  12651  nnrecq  12694  qbtwnxr  12916  fz1n  13256  fz10  13259  fz01en  13266  fznatpl1  13292  fz12pr  13295  fztpval  13300  fseq1p1m1  13312  elfzp1b  13315  elfzm1b  13316  4fvwrd4  13358  ige2m2fzo  13431  fz0add1fz1  13438  fzo12sn  13451  fzo13pr  13452  fzo1to4tp  13456  fzofzp1  13465  fzostep1  13484  flge1nn  13522  fldiv4p1lem1div2  13536  modid0  13598  nnnfi  13667  fzennn  13669  fzen2  13670  f13idfv  13701  ser1const  13760  exp1  13769  zexpcl  13778  qexpcl  13779  qexpclz  13784  m1expcl  13786  expp1z  13813  expm1  13814  facnn  13970  fac0  13971  fac1  13972  bcn1  14008  bcpasc  14016  bcnm1  14022  hashsng  14065  hashfz  14123  fz1isolem  14156  seqcoll  14159  hashge2el2difr  14176  ccat2s1p2  14318  ccat2s1p2OLD  14320  s2f1o  14610  f1oun2prg  14611  swrd2lsw  14646  2swrd2eqwrdeq  14647  relexp1g  14718  climuni  15242  isercoll2  15361  iseraltlem1  15374  sum0  15414  sumsnf  15436  climcndslem1  15542  climcndslem2  15543  divcnvshft  15548  supcvg  15549  prod0  15634  prodsn  15653  prodsnf  15655  zrisefaccl  15711  zfallfaccl  15712  sin01gt0  15880  rpnnen2lem10  15913  nthruc  15942  iddvds  15960  1dvds  15961  dvdsle  16000  dvds1  16009  3dvds  16021  n2dvds1  16058  divalglem5  16087  divalg  16093  bitsfzolem  16122  gcdcllem1  16187  gcdcllem3  16189  gcdaddmlem  16212  gcdadd  16214  gcdid  16215  gcd1  16216  1gcd  16222  bezoutlem1  16228  gcdmultipleOLD  16241  lcmgcdlem  16292  lcm1  16296  3lcm2e6woprm  16301  lcmfunsnlem  16327  isprm3  16369  ge2nprmge4  16387  phicl2  16450  phi1  16455  dfphi2  16456  eulerthlem2  16464  prmdiv  16467  prmdiveq  16468  odzcllem  16474  oddprm  16492  pythagtriplem4  16501  pcpre1  16524  pc1  16537  pcrec  16540  pcmpt  16574  fldivp1  16579  expnprm  16584  pockthlem  16587  unbenlem  16590  prmreclem2  16599  prmrec  16604  igz  16616  4sqlem12  16638  4sqlem13  16639  4sqlem19  16645  vdwlem8  16670  vdwlem13  16675  prmo1  16719  fvprmselgcd1  16727  prmgaplem7  16739  prmlem0  16788  1259lem4  16816  2503lem2  16820  4001lem1  16823  setsstruct  16858  gsumpropd2lem  18344  efmnd1hash  18512  mulgfval  18683  mulg1  18692  mulgm1  18705  mulgp1  18717  mulgneg2  18718  cycsubgcl  18806  odinv  19149  efgs1b  19323  lt6abl  19477  pgpfac1lem2  19659  srgbinomlem4  19760  qsubdrg  20631  zsubrg  20632  gzsubrg  20633  zringmulg  20659  zringcyg  20672  mulgrhm  20680  mulgrhm2  20681  chrnzr  20715  frgpcyg  20762  zrhpsgnmhm  20770  zrhpsgnodpm  20778  m2detleiblem1  21754  m2detleiblem2  21758  zfbas  23028  imasdsf1olem  23507  cphipval  24388  cmetcaulem  24433  bcthlem5  24473  ehl1eudis  24565  ovolctb  24635  ovolunlem1a  24641  ovolunlem1  24642  ovoliunnul  24652  ovolicc1  24661  ovolicc2lem4  24665  voliunlem1  24695  volsup  24701  uniioombllem6  24733  vitalilem5  24757  plyeq0lem  25352  vieta1lem2  25452  elqaalem2  25461  qaa  25464  iaa  25466  abelthlem6  25576  abelthlem9  25580  sin2pim  25623  cos2pim  25624  logbleb  25914  logblt  25915  1cubrlem  25972  leibpilem2  26072  emcllem5  26130  emcllem7  26132  lgamgulm2  26166  lgamcvglem  26170  gamcvg2lem  26189  lgam1  26194  wilthlem2  26199  wilthlem3  26200  ppip1le  26291  ppi1  26294  cht1  26295  chp1  26297  cht2  26302  ppieq0  26306  ppiub  26333  chpeq0  26337  chpchtsum  26348  chpub  26349  logfacbnd3  26352  logexprlim  26354  bposlem1  26413  bposlem2  26414  bposlem5  26417  bposlem6  26418  lgslem2  26427  lgsfcl2  26432  lgsval2lem  26436  lgsdir2lem1  26454  lgsdir2lem5  26458  1lgs  26469  lgsdchr  26484  lgsquad2lem2  26514  2sqlem9  26556  2sqlem10  26557  2sqblem  26560  2sqb  26561  dchrisumlem3  26620  log2sumbnd  26673  qabvle  26754  ostth3  26767  istrkg3ld  26803  tgldimor  26844  axlowdimlem3  27293  axlowdimlem6  27296  axlowdimlem7  27297  axlowdimlem16  27306  axlowdimlem17  27307  axlowdim  27310  usgrexmpldifpr  27606  uhgrwkspthlem2  28101  pthdlem2  28115  0ewlk  28457  0pth  28468  1wlkdlem1  28480  ntrl2v2e  28501  eupth2lem3lem4  28574  ex-fl  28790  ipval2  29048  hlim0  29576  opsqrlem2  30482  iuninc  30879  nndiffz1  31086  fzom1ne1  31101  0dp2dp  31162  cshw1s2  31211  cycpmco2lem4  31375  znfermltl  31541  lmatfvlem  31744  mdetpmtr1  31752  mdetpmtr12  31754  lmlim  31876  qqh0  31913  qqh1  31914  esumfzf  32016  esumfsup  32017  esumpcvgval  32025  esumcvg  32033  esumcvgsum  32035  esumsup  32036  dya2ub  32216  rrvsum  32400  dstfrvclim1  32423  ballotlem2  32434  ballotlemfc0  32438  ballotlemfcc  32439  signsvf0  32538  hgt750leme  32617  subfac1  33119  subfacp1lem1  33120  subfacp1lem2a  33121  subfacp1lem5  33125  subfacp1lem6  33126  cvmliftlem10  33235  divcnvlin  33677  faclimlem1  33688  fwddifnp1  34446  irrdiff  35476  poimirlem3  35759  poimirlem4  35760  poimirlem16  35772  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem24  35780  poimirlem27  35783  poimirlem28  35784  poimirlem31  35787  poimirlem32  35788  mblfinlem1  35793  mblfinlem2  35794  ovoliunnfl  35798  voliunnfl  35800  fdc  35882  heibor1lem  35946  rrncmslem  35969  lcmfunnnd  40000  lcm1un  40001  lcm2un  40002  lcmineqlem11  40027  lcmineqlem19  40035  aks4d1p1p2  40058  nn0rppwr  40313  nn0expgcd  40315  mapfzcons  40518  mzpexpmpt  40547  eldioph3b  40567  fz1eqin  40571  diophin  40574  diophun  40575  0dioph  40580  elnnrabdioph  40609  rabren3dioph  40617  irrapxlem1  40624  irrapxlem3  40626  rmxyadd  40723  rmxy1  40724  rmxy0  40725  rmxp1  40734  rmyp1  40735  rmxm1  40736  rmym1  40737  jm2.24nn  40761  acongeq  40785  jm2.23  40798  jm2.15nn0  40805  jm2.16nn0  40806  jm2.27c  40809  jm2.27dlem2  40812  rmydioph  40816  rmxdioph  40818  expdiophlem2  40824  expdioph  40825  mpaaeu  40955  trclfvdecomr  41289  k0004val0  41717  hashnzfzclim  41893  sumsnd  42522  fmuldfeq  43078  stoweidlem3  43498  stoweidlem20  43515  stoweidlem34  43529  wallispilem4  43563  wallispi2lem1  43566  wallispi2lem2  43567  stirlinglem11  43579  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem3  43595  fourierdlem47  43648  fourierswlem  43725  smfmullem4  44279  1oddALTV  45094  1nevenALTV  45095  2evenALTV  45096  nnsum3primes4  45192  nnsum3primesprm  45194  nnsum3primesgbe  45196  nnsum4primesodd  45200  nnsum4primesoddALTV  45201  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  tgblthelfgott  45219  1odd  45317  altgsumbcALT  45641  zlmodzxzsubm  45647  blen2  45883  blennngt2o2  45890  nn0sumshdiglemA  45917  nn0sumshdiglemB  45918