Theorem 1z 12730

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

This proof depends on syntax axioms:   ∈ wcel 2144  1c1 11205  ℤcz 12697

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-i2m1 11272  ax-1ne0 11273  ax-rrecex 11276  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-neg 11548  df-nn 12340  df-z 12698

This theorem is used by:  1zzd  12731  peano2z  12741  peano2zm  12743  3halfnz  12782  peano5uzti  12793  nnuz  13008  1eluzge0  13011  2eluzge1  13013  eluz2nn  13019  eluz2b1  13050  uz2m1nn  13054  nninf  13060  1q  13096  nnrecq  13104  qbtwnxr  13334  fz1n  13679  fz10  13682  fz01en  13690  fznatpl1  13716  fz12pr  13719  fztpval  13724  fseq1p1m1  13736  elfzp1b  13739  elfzm1b  13740  4fvwrd4  13786  fzo1lb  13852  ige2m2fzo  13867  fz0add1fz1  13874  fzo12sn  13887  fzo13pr  13888  fzo1to4tp  13893  fzofzp1  13903  fzom1ne1  13924  fzostep1  13925  flge1nn  13965  fldiv4p1lem1div2  13979  modid0  14041  nnnfi  14113  fzennn  14115  fzen2  14116  f13idfv  14147  ser1const  14205  exp1  14214  zexpcl  14223  qexpclz  14228  m1expcl  14233  expp1z  14258  expm1  14259  facnn  14423  fac0  14424  fac1  14425  bcn1  14461  bcpasc  14469  bcnm1  14475  hashsng  14517  hashfz  14576  fz1isolem  14610  seqcoll  14613  hashge2el2difr  14630  ccat2s1p2  14783  s2f1o  15073  f1oun2prg  15074  swrd2lsw  15111  2swrd2eqwrdeq  15112  relexp1g  15185  climuni  15725  isercoll2  15842  iseraltlem1  15855  sum0  15893  sumsnf  15915  climcndslem1  16024  climcndslem2  16025  divcnvshft  16030  supcvg  16031  prod0  16116  prodsn  16135  prodsnf  16137  zrisefaccl  16193  zfallfaccl  16194  sin01gt0  16364  rpnnen2lem10  16397  nthruc  16426  iddvds  16445  1dvds  16446  dvdsle  16486  dvds1  16495  3dvds  16507  n2dvds1  16544  divalglem5  16573  divalg  16579  bitsfzolem  16610  gcdcllem1  16675  gcdcllem3  16677  gcdaddmlem  16702  gcdadd  16704  gcdid  16705  gcd1  16707  1gcd  16712  bezoutlem1  16718  nn0rppwr  16741  nn0expgcd  16744  lcmgcdlem  16787  lcm1  16791  3lcm2e6woprm  16796  lcmfunsnlem  16822  isprm3  16864  ge2nprmge4  16883  phicl2  16951  phi1  16956  dfphi2  16957  eulerthlem2  16965  prmdiv  16968  prmdiveq  16969  odzcllem  16976  oddprm  16994  pythagtriplem4  17003  pcpre1  17026  pc1  17039  pcrec  17042  pcmpt  17076  fldivp1  17081  expnprm  17086  pockthlem  17089  unbenlem  17092  prmreclem2  17101  prmrec  17106  igz  17118  4sqlem12  17140  4sqlem13  17141  4sqlem19  17147  vdwlem8  17172  vdwlem13  17177  prmo1  17221  fvprmselgcd1  17229  prmlem0  17289  1259lem4  17318  2503lem2  17322  4001lem1  17325  setsstruct  17360  chnub  18802  gsumpropd2lem  18874  efmnd1hash  19094  mulgfval  19285  mulg1  19297  mulgm1  19310  mulgp1  19323  mulgneg2  19324  cycsubgcl  19427  odinv  19781  efgs1b  19956  lt6abl  20115  pgpfac1lem2  20297  srgbinomlem4  20461  qsubdrg  21731  zsubrg  21732  gzsubrg  21733  zringmulg  21768  zringcyg  21781  mulgrhm  21789  mulgrhm2  21790  pzriprnglem7  21799  pzriprnglem9  21801  pzriprnglem12  21804  pzriprnglem13  21805  pzriprnglem14  21806  pzriprng1ALT  21808  fermltlchr  21841  chrnzr  21842  frgpcyg  21885  zrhpsgnmhm  21896  zrhpsgnodpm  21904  m2detleiblem1  22945  m2detleiblem2  22949  zfbas  24221  imasdsf1olem  24698  cphipval  25570  cmetcaulem  25615  bcthlem5  25655  ovolctb  25817  ovolunlem1a  25823  ovolunlem1  25824  ovoliunnul  25834  ovolicc1  25843  ovolicc2lem4  25847  voliunlem1  25877  volsup  25883  uniioombllem6  25915  vitalilem5  25939  plyeq0lem  26535  vieta1lem2  26640  elqaalem2  26649  1aa  26656  iaaOLD  26658  abelthlem6  26769  abelthlem9  26773  sin2pim  26820  cos2pim  26821  logbleb  27117  logblt  27118  1cubrlem  27175  leibpilem2  27275  emcllem5  27333  emcllem7  27335  lgamgulm2  27369  lgamcvglem  27373  gamcvg2lem  27392  lgam1  27397  wilthlem2  27402  wilthlem3  27403  ppip1le  27494  ppi1  27497  cht1  27498  chp1  27500  cht2  27505  ppieq0  27509  ppiub  27537  chpeq0  27541  chpchtsum  27552  chpub  27553  logfacbnd3  27556  logexprlim  27558  bposlem1  27617  bposlem2  27618  bposlem5  27621  bposlem6  27622  lgslem2  27631  lgsfcl2  27636  lgsval2lem  27640  lgsdir2lem1  27658  lgsdir2lem5  27662  1lgs  27673  lgsdchr  27688  lgsquad2lem2  27718  2sqlem9  27760  2sqlem10  27761  2sqblem  27764  2sqb  27765  dchrisumlem3  27824  log2sumbnd  27877  qabvle  27958  ostth3  27971  istrkg3ld  28929  tgldimor  28971  axlowdimlem3  29528  axlowdimlem6  29531  axlowdimlem7  29532  axlowdimlem16  29541  axlowdimlem17  29542  axlowdim  29545  usgrexmpldifpr  29845  dfpth2  30320  uhgrwkspthlem2  30346  pthdlem2  30360  0ewlk  30711  0pth  30722  1wlkdlem1  30734  ntrl2v2e  30765  eupth2lem3lem4  30838  ex-fl  31054  ipval2  31315  hlim0  31843  opsqrlem2  32749  iuninc  33203  nndiffz1  33425  0dp2dp  33522  cshw1s2  33568  cycpmco2lem4  33737  1fldgenq  33931  znfermltl  33969  zringfrac  34133  constrextdg2  34428  cos9thpiminplylem5  34465  lmatfvlem  34494  mdetpmtr1  34502  mdetpmtr12  34504  lmlim  34626  qqh0  34663  qqh1  34664  esumfzf  34748  esumfsup  34749  esumpcvgval  34757  esumcvg  34765  esumcvgsum  34767  esumsup  34768  dya2ub  34949  rrvsum  35133  dstfrvclim1  35157  ballotlem2  35168  ballotlemfc0  35172  ballotlemfcc  35173  signsvf0  35256  hgt750leme  35334  subfac1  36030  subfacp1lem1  36031  subfacp1lem2a  36032  subfacp1lem5  36036  subfacp1lem6  36037  cvmliftlem10  36146  divcnvlin  36591  faclimlem1  36601  fwddifnp1  37023  irrdiff  38341  qdiff  38342  poimirlem3  38635  poimirlem4  38636  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem24  38656  poimirlem27  38659  poimirlem28  38660  poimirlem31  38663  poimirlem32  38664  mblfinlem1  38669  mblfinlem2  38670  ovoliunnfl  38674  voliunnfl  38676  fdc  38773  heibor1lem  38837  rrncmslem  38860  lcmfunnnd  43156  lcm1un  43157  lcm2un  43158  lcmineqlem11  43183  lcmineqlem19  43191  aks4d1p1p2  43214  mapfzcons  43821  mzpexpmpt  43850  eldioph3b  43870  fz1eqin  43874  diophin  43877  diophun  43878  0dioph  43883  elnnrabdioph  43908  rabren3dioph  43916  irrapxlem1  43923  irrapxlem3  43925  rmxyadd  44022  rmxy1  44023  rmxy0  44024  rmxp1  44033  rmyp1  44034  rmxm1  44035  rmym1  44036  jm2.24nn  44060  acongeq  44084  jm2.23  44097  jm2.15nn0  44104  jm2.16nn0  44105  jm2.27c  44108  jm2.27dlem2  44111  rmydioph  44115  rmxdioph  44117  expdiophlem2  44123  expdioph  44124  mpaaeu  44246  trclfvdecomr  44822  k0004val0  45248  hashnzfzclim  45400  sumsnd  46137  fmuldfeq  46689  stoweidlem3  47107  stoweidlem20  47124  stoweidlem34  47138  wallispilem4  47172  wallispi2lem1  47175  wallispi2lem2  47176  stirlinglem11  47188  dirkerper  47200  dirkertrigeqlem1  47202  dirkertrigeqlem3  47204  fourierdlem47  47257  fourierswlem  47334  smfmullem4  47898  ormklocald  47980  sqrtnnaa  48007  sqrtnzqaa  48008  ceilhalf1  48502  nprmdvdsfacm1lem4  48802  ppivalnnprm  48804  ppivalnn  48811  1oddALTV  48882  1nevenALTV  48883  2evenALTV  48884  nnsum3primes4  48980  nnsum3primesprm  48982  nnsum3primesgbe  48984  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  tgblthelfgott  49007  stgr1  49153  gpgusgralem  49248  1odd  49362  altgsumbcALT  49559  zlmodzxzsubm  49565  blen2  49791  blennngt2o2  49798  nn0sumshdiglemA  49825  nn0sumshdiglemB  49826  crosspdotsumlem  51133  crosspaltd  51135  crossp3d  51136  veroquadgsumlem  51152