Theorem 1z 12615

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

Syntax hints:   ∈ wcel 2145  1c1 11089  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-neg 11432  df-nn 12225  df-z 12583

This theorem is referenced by:  1zzd  12616  peano2z  12626  peano2zm  12628  3halfnz  12666  peano5uzti  12677  nnuz  12892  1eluzge0  12895  2eluzge1  12897  eluz2nn  12903  eluz2b1  12934  uz2m1nn  12938  nninf  12944  nnrecq  12987  qbtwnxr  13217  fz1n  13561  fz10  13564  fz01en  13571  fznatpl1  13597  fz12pr  13600  fztpval  13605  fseq1p1m1  13617  elfzp1b  13620  elfzm1b  13621  4fvwrd4  13667  fzo1lb  13733  ige2m2fzo  13748  fz0add1fz1  13755  fzo12sn  13768  fzo13pr  13769  fzo1to4tp  13774  fzofzp1  13784  fzom1ne1  13805  fzostep1  13806  flge1nn  13845  fldiv4p1lem1div2  13859  modid0  13921  nnnfi  13993  fzennn  13995  fzen2  13996  f13idfv  14027  ser1const  14085  exp1  14094  zexpcl  14103  qexpcl  14104  qexpclz  14108  m1expcl  14113  expp1z  14138  expm1  14139  facnn  14302  fac0  14303  fac1  14304  bcn1  14340  bcpasc  14348  bcnm1  14354  hashsng  14396  hashfz  14454  fz1isolem  14488  seqcoll  14491  hashge2el2difr  14508  ccat2s1p2  14658  s2f1o  14943  f1oun2prg  14944  swrd2lsw  14979  2swrd2eqwrdeq  14980  relexp1g  15053  climuni  15593  isercoll2  15710  iseraltlem1  15723  sum0  15762  sumsnf  15784  climcndslem1  15893  climcndslem2  15894  divcnvshft  15899  supcvg  15900  prod0  15987  prodsn  16006  prodsnf  16008  zrisefaccl  16064  zfallfaccl  16065  sin01gt0  16236  rpnnen2lem10  16269  nthruc  16298  iddvds  16317  1dvds  16318  dvdsle  16358  dvds1  16367  3dvds  16379  n2dvds1  16416  divalglem5  16445  divalg  16451  bitsfzolem  16482  gcdcllem1  16547  gcdcllem3  16549  gcdaddmlem  16572  gcdadd  16574  gcdid  16575  gcd1  16576  1gcd  16581  bezoutlem1  16587  nn0rppwr  16609  nn0expgcd  16612  lcmgcdlem  16654  lcm1  16658  3lcm2e6woprm  16663  lcmfunsnlem  16689  isprm3  16731  ge2nprmge4  16750  phicl2  16817  phi1  16822  dfphi2  16823  eulerthlem2  16831  prmdiv  16834  prmdiveq  16835  odzcllem  16842  oddprm  16860  pythagtriplem4  16869  pcpre1  16892  pc1  16905  pcrec  16908  pcmpt  16942  fldivp1  16947  expnprm  16952  pockthlem  16955  unbenlem  16958  prmreclem2  16967  prmrec  16972  igz  16984  4sqlem12  17006  4sqlem13  17007  4sqlem19  17013  vdwlem8  17038  vdwlem13  17043  prmo1  17087  fvprmselgcd1  17095  prmlem0  17155  1259lem4  17184  2503lem2  17188  4001lem1  17191  setsstruct  17226  chnub  18668  gsumpropd2lem  18727  efmnd1hash  18941  mulgfval  19126  mulg1  19138  mulgm1  19151  mulgp1  19164  mulgneg2  19165  cycsubgcl  19268  odinv  19622  efgs1b  19797  lt6abl  19956  pgpfac1lem2  20138  srgbinomlem4  20302  qsubdrg  21529  zsubrg  21530  gzsubrg  21531  zringmulg  21566  zringcyg  21579  mulgrhm  21587  mulgrhm2  21588  pzriprnglem7  21597  pzriprnglem9  21599  pzriprnglem12  21602  pzriprnglem13  21603  pzriprnglem14  21604  pzriprng1ALT  21606  fermltlchr  21639  chrnzr  21640  frgpcyg  21683  zrhpsgnmhm  21694  zrhpsgnodpm  21702  m2detleiblem1  22742  m2detleiblem2  22746  zfbas  24014  imasdsf1olem  24491  cphipval  25363  cmetcaulem  25408  bcthlem5  25448  ehl1eudis  25540  ovolctb  25610  ovolunlem1a  25616  ovolunlem1  25617  ovoliunnul  25627  ovolicc1  25636  ovolicc2lem4  25640  voliunlem1  25670  volsup  25676  uniioombllem6  25708  vitalilem5  25732  plyeq0lem  26328  vieta1lem2  26433  elqaalem2  26442  qaa  26445  iaa  26447  abelthlem6  26557  abelthlem9  26561  sin2pim  26608  cos2pim  26609  logbleb  26906  logblt  26907  1cubrlem  26964  leibpilem2  27064  emcllem5  27122  emcllem7  27124  lgamgulm2  27158  lgamcvglem  27162  gamcvg2lem  27181  lgam1  27186  wilthlem2  27191  wilthlem3  27192  ppip1le  27283  ppi1  27286  cht1  27287  chp1  27289  cht2  27294  ppieq0  27298  ppiub  27326  chpeq0  27330  chpchtsum  27341  chpub  27342  logfacbnd3  27345  logexprlim  27347  bposlem1  27406  bposlem2  27407  bposlem5  27410  bposlem6  27411  lgslem2  27420  lgsfcl2  27425  lgsval2lem  27429  lgsdir2lem1  27447  lgsdir2lem5  27451  1lgs  27462  lgsdchr  27477  lgsquad2lem2  27507  2sqlem9  27549  2sqlem10  27550  2sqblem  27553  2sqb  27554  dchrisumlem3  27613  log2sumbnd  27666  qabvle  27747  ostth3  27760  istrkg3ld  28688  tgldimor  28729  axlowdimlem3  29203  axlowdimlem6  29206  axlowdimlem7  29207  axlowdimlem16  29216  axlowdimlem17  29217  axlowdim  29220  usgrexmpldifpr  29517  dfpth2  29987  uhgrwkspthlem2  30012  pthdlem2  30026  0ewlk  30374  0pth  30385  1wlkdlem1  30397  ntrl2v2e  30418  eupth2lem3lem4  30491  ex-fl  30707  ipval2  30968  hlim0  31496  opsqrlem2  32402  iuninc  32815  nndiffz1  33043  0dp2dp  33141  cshw1s2  33193  cycpmco2lem4  33362  1fldgenq  33558  znfermltl  33596  zringfrac  33761  constrextdg2  34056  cos9thpiminplylem5  34093  lmatfvlem  34122  mdetpmtr1  34130  mdetpmtr12  34132  lmlim  34254  qqh0  34291  qqh1  34292  esumfzf  34376  esumfsup  34377  esumpcvgval  34385  esumcvg  34393  esumcvgsum  34395  esumsup  34396  dya2ub  34577  rrvsum  34761  dstfrvclim1  34785  ballotlem2  34796  ballotlemfc0  34800  ballotlemfcc  34801  signsvf0  34884  hgt750leme  34962  subfac1  35541  subfacp1lem1  35542  subfacp1lem2a  35543  subfacp1lem5  35547  subfacp1lem6  35548  cvmliftlem10  35657  divcnvlin  36096  faclimlem1  36106  fwddifnp1  36528  irrdiff  37830  qdiff  37831  poimirlem3  38134  poimirlem4  38135  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem24  38155  poimirlem27  38158  poimirlem28  38159  poimirlem31  38162  poimirlem32  38163  mblfinlem1  38168  mblfinlem2  38169  ovoliunnfl  38173  voliunnfl  38175  fdc  38256  heibor1lem  38320  rrncmslem  38343  lcmfunnnd  42641  lcm1un  42642  lcm2un  42643  lcmineqlem11  42668  lcmineqlem19  42676  aks4d1p1p2  42699  mapfzcons  43309  mzpexpmpt  43338  eldioph3b  43358  fz1eqin  43362  diophin  43365  diophun  43366  0dioph  43371  elnnrabdioph  43396  rabren3dioph  43404  irrapxlem1  43411  irrapxlem3  43413  rmxyadd  43510  rmxy1  43511  rmxy0  43512  rmxp1  43521  rmyp1  43522  rmxm1  43523  rmym1  43524  jm2.24nn  43548  acongeq  43572  jm2.23  43585  jm2.15nn0  43592  jm2.16nn0  43593  jm2.27c  43596  jm2.27dlem2  43599  rmydioph  43603  rmxdioph  43605  expdiophlem2  43611  expdioph  43612  mpaaeu  43739  trclfvdecomr  44316  k0004val0  44742  hashnzfzclim  44896  sumsnd  45604  fmuldfeq  46157  stoweidlem3  46575  stoweidlem20  46592  stoweidlem34  46606  wallispilem4  46640  wallispi2lem1  46643  wallispi2lem2  46644  stirlinglem11  46656  dirkerper  46668  dirkertrigeqlem1  46670  dirkertrigeqlem3  46672  fourierdlem47  46725  fourierswlem  46802  smfmullem4  47366  ormklocald  47448  natlocalincr  47450  nthrucw  47460  ceilhalf1  47930  nprmdvdsfacm1lem4  48230  ppivalnnprm  48232  ppivalnn  48239  1oddALTV  48310  1nevenALTV  48311  2evenALTV  48312  nnsum3primes4  48408  nnsum3primesprm  48410  nnsum3primesgbe  48412  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  tgblthelfgott  48435  stgr1  48581  gpgusgralem  48676  1odd  48791  altgsumbcALT  48984  zlmodzxzsubm  48990  blen2  49216  blennngt2o2  49223  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251