Theorem 1z 12548

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

Syntax hints:   ∈ wcel 2114  1c1 11030  ℤcz 12515

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 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-nn 12166  df-z 12516

This theorem is referenced by:  1zzd  12549  peano2z  12559  peano2zm  12561  3halfnz  12599  peano5uzti  12610  nnuz  12818  1eluzge0  12821  2eluzge1  12823  eluz2nn  12829  eluz2b1  12860  uz2m1nn  12864  nninf  12870  nnrecq  12913  qbtwnxr  13143  fz1n  13487  fz10  13490  fz01en  13497  fznatpl1  13523  fz12pr  13526  fztpval  13531  fseq1p1m1  13543  elfzp1b  13546  elfzm1b  13547  4fvwrd4  13593  fzo1lb  13659  ige2m2fzo  13674  fz0add1fz1  13681  fzo12sn  13694  fzo13pr  13695  fzo1to4tp  13700  fzofzp1  13710  fzom1ne1  13731  fzostep1  13732  flge1nn  13771  fldiv4p1lem1div2  13785  modid0  13847  nnnfi  13919  fzennn  13921  fzen2  13922  f13idfv  13953  ser1const  14011  exp1  14020  zexpcl  14029  qexpcl  14030  qexpclz  14034  m1expcl  14039  expp1z  14064  expm1  14065  facnn  14228  fac0  14229  fac1  14230  bcn1  14266  bcpasc  14274  bcnm1  14280  hashsng  14322  hashfz  14380  fz1isolem  14414  seqcoll  14417  hashge2el2difr  14434  ccat2s1p2  14584  s2f1o  14869  f1oun2prg  14870  swrd2lsw  14905  2swrd2eqwrdeq  14906  relexp1g  14979  climuni  15505  isercoll2  15622  iseraltlem1  15635  sum0  15674  sumsnf  15696  climcndslem1  15805  climcndslem2  15806  divcnvshft  15811  supcvg  15812  prod0  15899  prodsn  15918  prodsnf  15920  zrisefaccl  15976  zfallfaccl  15977  sin01gt0  16148  rpnnen2lem10  16181  nthruc  16210  iddvds  16229  1dvds  16230  dvdsle  16270  dvds1  16279  3dvds  16291  n2dvds1  16328  divalglem5  16357  divalg  16363  bitsfzolem  16394  gcdcllem1  16459  gcdcllem3  16461  gcdaddmlem  16484  gcdadd  16486  gcdid  16487  gcd1  16488  1gcd  16493  bezoutlem1  16499  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  lcm1  16570  3lcm2e6woprm  16575  lcmfunsnlem  16601  isprm3  16643  ge2nprmge4  16662  phicl2  16729  phi1  16734  dfphi2  16735  eulerthlem2  16743  prmdiv  16746  prmdiveq  16747  odzcllem  16754  oddprm  16772  pythagtriplem4  16781  pcpre1  16804  pc1  16817  pcrec  16820  pcmpt  16854  fldivp1  16859  expnprm  16864  pockthlem  16867  unbenlem  16870  prmreclem2  16879  prmrec  16884  igz  16896  4sqlem12  16918  4sqlem13  16919  4sqlem19  16925  vdwlem8  16950  vdwlem13  16955  prmo1  16999  fvprmselgcd1  17007  prmlem0  17067  1259lem4  17095  2503lem2  17099  4001lem1  17102  setsstruct  17137  chnub  18579  gsumpropd2lem  18638  efmnd1hash  18851  mulgfval  19036  mulg1  19048  mulgm1  19061  mulgp1  19074  mulgneg2  19075  cycsubgcl  19172  odinv  19527  efgs1b  19702  lt6abl  19861  pgpfac1lem2  20043  srgbinomlem4  20201  qsubdrg  21409  zsubrg  21410  gzsubrg  21411  zringmulg  21446  zringcyg  21459  mulgrhm  21467  mulgrhm2  21468  pzriprnglem7  21477  pzriprnglem9  21479  pzriprnglem12  21482  pzriprnglem13  21483  pzriprnglem14  21484  pzriprng1ALT  21486  fermltlchr  21519  chrnzr  21520  frgpcyg  21563  zrhpsgnmhm  21574  zrhpsgnodpm  21582  m2detleiblem1  22599  m2detleiblem2  22603  zfbas  23871  imasdsf1olem  24348  cphipval  25220  cmetcaulem  25265  bcthlem5  25305  ehl1eudis  25397  ovolctb  25467  ovolunlem1a  25473  ovolunlem1  25474  ovoliunnul  25484  ovolicc1  25493  ovolicc2lem4  25497  voliunlem1  25527  volsup  25533  uniioombllem6  25565  vitalilem5  25589  plyeq0lem  26185  vieta1lem2  26288  elqaalem2  26297  qaa  26300  iaa  26302  abelthlem6  26414  abelthlem9  26418  sin2pim  26462  cos2pim  26463  logbleb  26760  logblt  26761  1cubrlem  26818  leibpilem2  26918  emcllem5  26977  emcllem7  26979  lgamgulm2  27013  lgamcvglem  27017  gamcvg2lem  27036  lgam1  27041  wilthlem2  27046  wilthlem3  27047  ppip1le  27138  ppi1  27141  cht1  27142  chp1  27144  cht2  27149  ppieq0  27153  ppiub  27181  chpeq0  27185  chpchtsum  27196  chpub  27197  logfacbnd3  27200  logexprlim  27202  bposlem1  27261  bposlem2  27262  bposlem5  27265  bposlem6  27266  lgslem2  27275  lgsfcl2  27280  lgsval2lem  27284  lgsdir2lem1  27302  lgsdir2lem5  27306  1lgs  27317  lgsdchr  27332  lgsquad2lem2  27362  2sqlem9  27404  2sqlem10  27405  2sqblem  27408  2sqb  27409  dchrisumlem3  27468  log2sumbnd  27521  qabvle  27602  ostth3  27615  istrkg3ld  28543  tgldimor  28584  axlowdimlem3  29027  axlowdimlem6  29030  axlowdimlem7  29031  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  usgrexmpldifpr  29341  dfpth2  29812  uhgrwkspthlem2  29837  pthdlem2  29851  0ewlk  30199  0pth  30210  1wlkdlem1  30222  ntrl2v2e  30243  eupth2lem3lem4  30316  ex-fl  30532  ipval2  30793  hlim0  31321  opsqrlem2  32227  iuninc  32645  nndiffz1  32874  0dp2dp  32983  cshw1s2  33035  cycpmco2lem4  33205  1fldgenq  33398  znfermltl  33441  zringfrac  33629  constrextdg2  33909  cos9thpiminplylem5  33946  lmatfvlem  33975  mdetpmtr1  33983  mdetpmtr12  33985  lmlim  34107  qqh0  34144  qqh1  34145  esumfzf  34229  esumfsup  34230  esumpcvgval  34238  esumcvg  34246  esumcvgsum  34248  esumsup  34249  dya2ub  34430  rrvsum  34614  dstfrvclim1  34638  ballotlem2  34649  ballotlemfc0  34653  ballotlemfcc  34654  signsvf0  34740  hgt750leme  34818  subfac1  35376  subfacp1lem1  35377  subfacp1lem2a  35378  subfacp1lem5  35382  subfacp1lem6  35383  cvmliftlem10  35492  divcnvlin  35931  faclimlem1  35941  fwddifnp1  36363  irrdiff  37656  poimirlem3  37958  poimirlem4  37959  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem24  37979  poimirlem27  37982  poimirlem28  37983  poimirlem31  37986  poimirlem32  37987  mblfinlem1  37992  mblfinlem2  37993  ovoliunnfl  37997  voliunnfl  37999  fdc  38080  heibor1lem  38144  rrncmslem  38167  lcmfunnnd  42465  lcm1un  42466  lcm2un  42467  lcmineqlem11  42492  lcmineqlem19  42500  aks4d1p1p2  42523  mapfzcons  43162  mzpexpmpt  43191  eldioph3b  43211  fz1eqin  43215  diophin  43218  diophun  43219  0dioph  43224  elnnrabdioph  43253  rabren3dioph  43261  irrapxlem1  43268  irrapxlem3  43270  rmxyadd  43367  rmxy1  43368  rmxy0  43369  rmxp1  43378  rmyp1  43379  rmxm1  43380  rmym1  43381  jm2.24nn  43405  acongeq  43429  jm2.23  43442  jm2.15nn0  43449  jm2.16nn0  43450  jm2.27c  43453  jm2.27dlem2  43456  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  mpaaeu  43596  trclfvdecomr  44173  k0004val0  44599  hashnzfzclim  44767  sumsnd  45475  fmuldfeq  46031  stoweidlem3  46449  stoweidlem20  46466  stoweidlem34  46480  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem11  46530  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem3  46546  fourierdlem47  46599  fourierswlem  46676  smfmullem4  47240  ormklocald  47320  natlocalincr  47322  nthrucw  47332  ceilhalf1  47798  nprmdvdsfacm1lem4  48098  ppivalnnprm  48100  ppivalnn  48107  1oddALTV  48178  1nevenALTV  48179  2evenALTV  48180  nnsum3primes4  48276  nnsum3primesprm  48278  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  tgblthelfgott  48303  stgr1  48449  gpgusgralem  48544  1odd  48659  altgsumbcALT  48841  zlmodzxzsubm  48847  blen2  49073  blennngt2o2  49080  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108