Theorem 1z 12570

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

Syntax hints:   ∈ wcel 2109  1c1 11076  ℤcz 12536

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-z 12537

This theorem is referenced by:  1zzd  12571  peano2z  12581  peano2zm  12583  3halfnz  12620  peano5uzti  12631  nnuz  12843  1eluzge0  12846  2eluzge1  12848  eluz2nn  12854  eluz2b1  12885  uz2m1nn  12889  nninf  12895  nnrecq  12938  qbtwnxr  13167  fz1n  13510  fz10  13513  fz01en  13520  fznatpl1  13546  fz12pr  13549  fztpval  13554  fseq1p1m1  13566  elfzp1b  13569  elfzm1b  13570  4fvwrd4  13616  fzo1lb  13681  ige2m2fzo  13696  fz0add1fz1  13703  fzo12sn  13716  fzo13pr  13717  fzo1to4tp  13722  fzofzp1  13732  fzostep1  13751  flge1nn  13790  fldiv4p1lem1div2  13804  modid0  13866  nnnfi  13938  fzennn  13940  fzen2  13941  f13idfv  13972  ser1const  14030  exp1  14039  zexpcl  14048  qexpcl  14049  qexpclz  14053  m1expcl  14058  expp1z  14083  expm1  14084  facnn  14247  fac0  14248  fac1  14249  bcn1  14285  bcpasc  14293  bcnm1  14299  hashsng  14341  hashfz  14399  fz1isolem  14433  seqcoll  14436  hashge2el2difr  14453  ccat2s1p2  14602  s2f1o  14889  f1oun2prg  14890  swrd2lsw  14925  2swrd2eqwrdeq  14926  relexp1g  14999  climuni  15525  isercoll2  15642  iseraltlem1  15655  sum0  15694  sumsnf  15716  climcndslem1  15822  climcndslem2  15823  divcnvshft  15828  supcvg  15829  prod0  15916  prodsn  15935  prodsnf  15937  zrisefaccl  15993  zfallfaccl  15994  sin01gt0  16165  rpnnen2lem10  16198  nthruc  16227  iddvds  16246  1dvds  16247  dvdsle  16287  dvds1  16296  3dvds  16308  n2dvds1  16345  divalglem5  16374  divalg  16380  bitsfzolem  16411  gcdcllem1  16476  gcdcllem3  16478  gcdaddmlem  16501  gcdadd  16503  gcdid  16504  gcd1  16505  1gcd  16510  bezoutlem1  16516  nn0rppwr  16538  nn0expgcd  16541  lcmgcdlem  16583  lcm1  16587  3lcm2e6woprm  16592  lcmfunsnlem  16618  isprm3  16660  ge2nprmge4  16678  phicl2  16745  phi1  16750  dfphi2  16751  eulerthlem2  16759  prmdiv  16762  prmdiveq  16763  odzcllem  16770  oddprm  16788  pythagtriplem4  16797  pcpre1  16820  pc1  16833  pcrec  16836  pcmpt  16870  fldivp1  16875  expnprm  16880  pockthlem  16883  unbenlem  16886  prmreclem2  16895  prmrec  16900  igz  16912  4sqlem12  16934  4sqlem13  16935  4sqlem19  16941  vdwlem8  16966  vdwlem13  16971  prmo1  17015  fvprmselgcd1  17023  prmlem0  17083  1259lem4  17111  2503lem2  17115  4001lem1  17118  setsstruct  17153  gsumpropd2lem  18613  efmnd1hash  18826  mulgfval  19008  mulg1  19020  mulgm1  19033  mulgp1  19046  mulgneg2  19047  cycsubgcl  19145  odinv  19498  efgs1b  19673  lt6abl  19832  pgpfac1lem2  20014  srgbinomlem4  20145  qsubdrg  21343  zsubrg  21344  gzsubrg  21345  zringmulg  21373  zringcyg  21386  mulgrhm  21394  mulgrhm2  21395  pzriprnglem7  21404  pzriprnglem9  21406  pzriprnglem12  21409  pzriprnglem13  21410  pzriprnglem14  21411  pzriprng1ALT  21413  fermltlchr  21446  chrnzr  21447  frgpcyg  21490  zrhpsgnmhm  21500  zrhpsgnodpm  21508  m2detleiblem1  22518  m2detleiblem2  22522  zfbas  23790  imasdsf1olem  24268  cphipval  25150  cmetcaulem  25195  bcthlem5  25235  ehl1eudis  25327  ovolctb  25398  ovolunlem1a  25404  ovolunlem1  25405  ovoliunnul  25415  ovolicc1  25424  ovolicc2lem4  25428  voliunlem1  25458  volsup  25464  uniioombllem6  25496  vitalilem5  25520  plyeq0lem  26122  vieta1lem2  26226  elqaalem2  26235  qaa  26238  iaa  26240  abelthlem6  26353  abelthlem9  26357  sin2pim  26401  cos2pim  26402  logbleb  26700  logblt  26701  1cubrlem  26758  leibpilem2  26858  emcllem5  26917  emcllem7  26919  lgamgulm2  26953  lgamcvglem  26957  gamcvg2lem  26976  lgam1  26981  wilthlem2  26986  wilthlem3  26987  ppip1le  27078  ppi1  27081  cht1  27082  chp1  27084  cht2  27089  ppieq0  27093  ppiub  27122  chpeq0  27126  chpchtsum  27137  chpub  27138  logfacbnd3  27141  logexprlim  27143  bposlem1  27202  bposlem2  27203  bposlem5  27206  bposlem6  27207  lgslem2  27216  lgsfcl2  27221  lgsval2lem  27225  lgsdir2lem1  27243  lgsdir2lem5  27247  1lgs  27258  lgsdchr  27273  lgsquad2lem2  27303  2sqlem9  27345  2sqlem10  27346  2sqblem  27349  2sqb  27350  dchrisumlem3  27409  log2sumbnd  27462  qabvle  27543  ostth3  27556  istrkg3ld  28395  tgldimor  28436  axlowdimlem3  28878  axlowdimlem6  28881  axlowdimlem7  28882  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  usgrexmpldifpr  29192  dfpth2  29666  uhgrwkspthlem2  29691  pthdlem2  29705  0ewlk  30050  0pth  30061  1wlkdlem1  30073  ntrl2v2e  30094  eupth2lem3lem4  30167  ex-fl  30383  ipval2  30643  hlim0  31171  opsqrlem2  32077  iuninc  32496  nndiffz1  32716  fzom1ne1  32731  0dp2dp  32836  cshw1s2  32889  chnub  32945  cycpmco2lem4  33093  1fldgenq  33279  znfermltl  33344  zringfrac  33532  constrextdg2  33746  cos9thpiminplylem5  33783  lmatfvlem  33812  mdetpmtr1  33820  mdetpmtr12  33822  lmlim  33944  qqh0  33981  qqh1  33982  esumfzf  34066  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  esumcvgsum  34085  esumsup  34086  dya2ub  34268  rrvsum  34452  dstfrvclim1  34476  ballotlem2  34487  ballotlemfc0  34491  ballotlemfcc  34492  signsvf0  34578  hgt750leme  34656  subfac1  35172  subfacp1lem1  35173  subfacp1lem2a  35174  subfacp1lem5  35178  subfacp1lem6  35179  cvmliftlem10  35288  divcnvlin  35727  faclimlem1  35737  fwddifnp1  36160  irrdiff  37321  poimirlem3  37624  poimirlem4  37625  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  mblfinlem1  37658  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  fdc  37746  heibor1lem  37810  rrncmslem  37833  lcmfunnnd  42007  lcm1un  42008  lcm2un  42009  lcmineqlem11  42034  lcmineqlem19  42042  aks4d1p1p2  42065  mapfzcons  42711  mzpexpmpt  42740  eldioph3b  42760  fz1eqin  42764  diophin  42767  diophun  42768  0dioph  42773  elnnrabdioph  42802  rabren3dioph  42810  irrapxlem1  42817  irrapxlem3  42819  rmxyadd  42917  rmxy1  42918  rmxy0  42919  rmxp1  42928  rmyp1  42929  rmxm1  42930  rmym1  42931  jm2.24nn  42955  acongeq  42979  jm2.23  42992  jm2.15nn0  42999  jm2.16nn0  43000  jm2.27c  43003  jm2.27dlem2  43006  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  mpaaeu  43146  trclfvdecomr  43724  k0004val0  44150  hashnzfzclim  44318  sumsnd  45027  fmuldfeq  45588  stoweidlem3  46008  stoweidlem20  46025  stoweidlem34  46039  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem11  46089  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  fourierdlem47  46158  fourierswlem  46235  smfmullem4  46799  ormklocald  46879  natlocalincr  46881  tworepnotupword  46891  ceilhalf1  47339  1oddALTV  47695  1nevenALTV  47696  2evenALTV  47697  nnsum3primes4  47793  nnsum3primesprm  47795  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  tgblthelfgott  47820  stgr1  47964  gpgusgralem  48051  1odd  48163  altgsumbcALT  48345  zlmodzxzsubm  48351  blen2  48578  blennngt2o2  48585  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613