MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1z Structured version   Unicode version

Theorem 1z 10312
Description: One is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
1z  |-  1  e.  ZZ

Proof of Theorem 1z
StepHypRef Expression
1 1nn 10012 . 2  |-  1  e.  NN
21nnzi 10306 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   1c1 8992   ZZcz 10283
This theorem is referenced by:  peano2z  10319  peano2zm  10321  peano5uzti  10360  nnuz  10522  eluz2b1  10548  uz2m1nn  10551  nninfm  10557  nnrecq  10598  qbtwnxr  10787  fz1n  11074  fz10  11076  fz01en  11080  fzprval  11107  fztpval  11108  4fvwrd4  11122  fseq1p1m1  11123  elfzm1b  11126  fzm1  11128  fzoss2  11164  fzo12sn  11184  fzofzp1  11190  elfznelfzo  11193  fzostep1  11198  injresinj  11201  flge1nn  11227  modnegd  11282  fzennn  11308  fzen2  11309  sermono  11356  seqf1olem2  11364  ser1const  11380  exp1  11388  zexpcl  11397  qexpcl  11398  qexpclz  11403  m1expcl  11405  expp1z  11429  expm1  11430  facnn  11569  fac0  11570  fac1  11571  bcn1  11605  bcp1nk  11609  bcpasc  11613  hashsng  11648  hashfz  11693  fz1isolem  11711  seqcoll  11713  s2f1o  11864  f1oun2prg  11865  climuni  12347  isercoll  12462  isercoll2  12463  iseraltlem1  12476  sum0  12516  sumsn  12535  fsumtscopo  12582  fsumparts  12586  binomlem  12609  climcndslem1  12630  climcndslem2  12631  climcnds  12632  divcnv  12634  supcvg  12636  arisum  12640  trireciplem  12642  trirecip  12643  expcnv  12644  geo2sum  12651  geo2lim  12653  geoisum1  12657  geoisum1c  12658  mertenslem1  12662  mertenslem2  12663  ege2le3  12693  sin01gt0  12792  rpnnen2lem10  12824  rpnnen2  12826  nthruc  12851  iddvds  12864  1dvds  12865  dvdsle  12896  dvds1  12899  3dvds  12913  divalglem5  12918  divalg  12924  bitsfzolem  12947  bitsfzo  12948  bitscmp  12951  gcdcllem1  13012  gcdcllem3  13014  gcdaddmlem  13029  gcdadd  13031  gcdid  13032  gcd1  13033  1gcd  13038  bezoutlem1  13039  gcdmultiple  13051  isprm3  13089  phicl2  13158  phi1  13163  dfphi2  13164  hashdvds  13165  phiprmpw  13166  eulerthlem2  13172  prmdiv  13175  prmdiveq  13176  odzcllem  13179  odzdvds  13182  odzphi  13183  oddprm  13190  pythagtriplem4  13194  iserodd  13210  pcpre1  13217  pc1  13230  pcrec  13233  pcid  13247  pcmptcl  13261  pcmpt  13262  fldivp1  13267  expnprm  13272  pockthlem  13274  unbenlem  13277  prmreclem2  13286  prmreclem4  13288  prmreclem6  13290  prmrec  13291  igz  13303  4sqlem12  13325  4sqlem13  13326  4sqlem19  13332  vdwapun  13343  vdwlem8  13357  vdwlem13  13362  prmlem0  13429  1259lem4  13454  2503lem2  13458  4001lem1  13461  mulg1  14898  mulgm1  14910  mulgp1  14917  mulgneg2  14918  mulgpropd  14924  cycsubgcl  14967  odinv  15198  sylow1lem1  15233  sylow3lem6  15267  efgs1b  15369  lt6abl  15505  pgpfac1lem2  15634  qsubdrg  16752  zsubrg  16753  gzsubrg  16754  zcyg  16773  mulgrhm  16788  mulgrhm2  16789  chrnzr  16812  znunit  16845  znrrg  16847  frgpcyg  16855  lmcnp  17369  lmmo  17445  1stcelcls  17525  1stccnp  17526  1stckgenlem  17586  1stckgen  17587  zfbas  17929  imasdsf1olem  18404  clmvneg1  19117  clmmulg  19119  lmnn  19217  cmetcaulem  19242  iscmet2  19248  causs  19252  caubl  19261  iscmet3i  19265  bcthlem5  19282  ovolsf  19370  ovolctb  19387  ovolunlem1a  19393  ovolunlem1  19394  ovoliunlem1  19399  ovoliun  19402  ovoliun2  19403  ovoliunnul  19404  ovolicc1  19413  ovolicc2lem2  19415  ovolicc2lem3  19416  ovolicc2lem4  19417  voliunlem1  19445  voliunlem2  19446  voliunlem3  19447  volsup  19451  ioombl1lem4  19456  uniioombllem2  19476  uniioombllem3  19478  uniioombllem6  19481  vitalilem4  19504  vitalilem5  19505  itg1climres  19607  mbfi1fseqlem6  19613  mbfi1flimlem  19615  mbfmullem2  19617  itg2monolem1  19643  itg2i1fseq  19648  itg2i1fseq2  19649  itg2addlem  19651  plyeq0lem  20130  dvply1  20202  vieta1lem2  20229  elqaalem2  20238  qaa  20241  iaa  20243  dvtaylp  20287  dvradcnv  20338  pserdvlem2  20345  pserdv2  20347  abelthlem6  20353  abelthlem9  20357  sin2pim  20394  cos2pim  20395  efif1olem2  20446  advlogexp  20547  logtayl  20552  logtaylsum  20553  logtayl2  20554  ang180lem3  20654  1cubrlem  20682  atantayl  20778  leibpilem2  20782  leibpi  20783  birthdaylem2  20792  dfef2  20810  divsqrsumlem  20819  emcllem4  20838  emcllem5  20839  emcllem6  20840  emcllem7  20841  wilthlem1  20852  wilthlem2  20853  wilthlem3  20854  basellem6  20869  basellem7  20870  basellem8  20871  basellem9  20872  muf  20924  ppip1le  20945  ppi1  20948  cht1  20949  chp1  20951  cht2  20956  ppieq0  20960  ppiub  20989  chpeq0  20993  chpchtsum  21004  chpub  21005  logfacbnd3  21008  logexprlim  21010  mersenne  21012  perfectlem1  21014  perfectlem2  21015  bposlem1  21069  bposlem2  21070  bposlem5  21073  bposlem6  21074  lgslem1  21081  lgslem2  21082  lgsfcl2  21087  lgsval2lem  21091  lgsdir2lem1  21108  lgsdir2lem3  21110  lgsdir2lem4  21111  lgsdir2lem5  21112  lgsqrlem1  21126  lgsdchr  21133  lgseisenlem1  21134  lgseisenlem2  21135  lgseisenlem4  21137  lgsquad2lem1  21143  lgsquad3  21146  m1lgs  21147  2sqlem9  21158  2sqlem10  21159  2sqlem11  21160  2sqblem  21162  2sqb  21163  dchrisumlema  21183  dchrisumlem3  21186  dchrmusum2  21189  dchrvmasumiflem1  21196  dchrvmaeq0  21199  dchrisum0re  21208  dchrisum0lem1b  21210  dchrisum0lem2a  21212  logdivsum  21228  log2sumbnd  21239  pntrlog2bndlem1  21272  pntpbnd2  21282  qabvle  21320  ostth3  21333  usgraexmpldifpr  21420  usgraexmpl  21421  2trllemD  21558  2trllemG  21559  0pth  21571  constr1trl  21589  constr2spthlem1  21595  redwlk  21607  fargshiftlem  21622  usgrcyclnl1  21628  usgrcyclnl2  21629  3v3e3cycl1  21632  constr3lem4  21635  constr3trllem3  21640  constr3trllem5  21642  constr3pthlem1  21643  constr3pthlem2  21644  constr3pthlem3  21645  4cycl4v4e  21654  4cycl4dv4e  21656  eupap1  21699  eupath2lem3  21702  ex-fl  21756  gx1  21851  gxm1  21857  nvlmle  22189  ipval2  22204  minvecolem3  22379  minvecolem4b  22381  minvecolem4  22383  h2hcau  22483  h2hlm  22484  hlimadd  22696  hlim0  22739  hhsscms  22780  occllem  22806  nlelchi  23565  opsqrlem2  23645  opsqrlem4  23647  hmopidmchi  23655  iuninc  24012  fzspl  24150  fzsplit3  24151  gsumpropd2lem  24221  zzsmulg  24266  lmlim  24334  rge0scvg  24336  lmxrge0  24338  lmdvg  24339  qqhval2lem  24366  qqh0  24369  qqh1  24370  rnlogblem  24400  logblt  24407  esumfzf  24460  esumfsup  24461  esumfsupre  24462  esumpcvgval  24469  esumcvg  24477  dya2ub  24621  rrvsum  24713  dstfrvclim1  24736  ballotlem2  24747  ballotlemfp1  24750  ballotlemfc0  24751  ballotlemfcc  24752  ballotlemimin  24764  ballotlemic  24765  ballotlem1c  24766  ballotlemsdom  24770  ballotlemsel1i  24771  ballotlemsima  24774  ballotlemfrceq  24787  ballotlemfrcn0  24788  zetacvg  24800  lgamgulmlem4  24817  lgamgulmlem6  24819  lgamgulm2  24821  lgamcvglem  24825  lgamcvg2  24840  gamcvg  24841  gamcvg2lem  24844  regamcl  24846  relgamcl  24847  lgam1  24849  subfac1  24865  subfacp1lem1  24866  subfacp1lem2a  24867  subfacp1lem5  24871  subfacp1lem6  24872  cvmliftlem10  24982  sinccvg  25111  circum  25112  elfzp1b  25117  fznatpl1  25199  bcnm1  25202  divcnvshft  25212  divcnvlin  25213  prod0  25270  fprodser  25276  fprodzcl  25281  prodsn  25287  iprodgam  25320  risefacval2  25327  fallfacval2  25328  zrisefaccl  25337  zfallfaccl  25338  risefall0lem  25343  binomfallfaclem2  25357  faclimlem1  25363  faclimlem2  25364  faclim  25366  iprodfac  25367  faclim2  25368  axlowdimlem3  25884  axlowdimlem4  25885  axlowdimlem6  25887  axlowdimlem7  25888  axlowdimlem16  25897  axlowdimlem17  25898  axlowdim  25901  bpolydiflem  26101  mblfinlem1  26244  mblfinlem2  26245  ovoliunnfl  26249  voliunnfl  26251  fdc  26450  lmclim2  26465  geomcau  26466  heibor1lem  26519  heibor1  26520  bfplem1  26532  bfplem2  26533  rrncmslem  26542  rrncms  26543  mapfzcons  26773  mzpexpmpt  26803  fzsplit1nn0  26813  eldioph2lem1  26819  eldioph3b  26824  fz1eqin  26828  diophin  26832  diophun  26833  0dioph  26838  elnnrabdioph  26868  rabren3dioph  26877  irrapxlem1  26886  irrapxlem3  26888  pellexlem6  26898  rmspecnonsq  26971  rmxyadd  26985  rmxy1  26986  rmxy0  26987  rmxp1  26996  rmyp1  26997  rmxm1  26998  rmym1  26999  jm2.24nn  27025  acongeq  27049  jm2.22  27067  jm2.23  27068  jm2.25  27071  jm2.15nn0  27075  jm2.16nn0  27076  jm2.27c  27079  jm2.27dlem2  27082  rmydioph  27086  rmxdioph  27088  expdiophlem2  27094  expdioph  27095  mpaaeu  27333  sumsnd  27674  fmuldfeq  27690  fmul01lt1lem2  27692  fmul01lt1  27693  clim1fr1  27704  stoweidlem3  27729  stoweidlem7  27733  stoweidlem11  27737  stoweidlem14  27740  stoweidlem20  27746  stoweidlem26  27752  stoweidlem34  27760  stoweidlem51  27777  wallispilem4  27794  wallispilem5  27795  wallispi  27796  wallispi2lem1  27797  wallispi2lem2  27798  stirlinglem1  27800  stirlinglem5  27804  stirlinglem7  27806  stirlinglem8  27807  stirlinglem11  27810  stirlinglem12  27811  stirlinglem13  27812  stirlinglem14  27813  stirlinglem15  27814  stirlingr  27816  f13idfv  28083  1eluzge0  28101  2eluzge1  28103  ubmelm1fzo  28128  fzo1fzo0n0  28129  2submod  28153  modid0  28160  modidmul0  28161  prmgt1  28224  modprm1div  28225
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-riota 6550  df-recs 6634  df-rdg 6669  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-nn 10002  df-z 10284
  Copyright terms: Public domain W3C validator