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

Theorem 1z 10243
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 9943 . 2  |-  1  e.  NN
21nnzi 10237 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   1c1 8924   ZZcz 10214
This theorem is referenced by:  peano2z  10250  peano2zm  10252  peano5uzti  10291  nnuz  10453  eluz2b1  10479  uz2m1nn  10482  nninfm  10488  nnrecq  10529  qbtwnxr  10718  fz1n  11005  fz10  11007  fz01en  11011  fzprval  11037  fztpval  11038  4fvwrd4  11051  fseq1p1m1  11052  elfzm1b  11055  fzm1  11057  fzoss2  11093  fzofzp1  11116  elfznelfzo  11119  fzostep1  11124  injresinj  11127  flge1nn  11153  modnegd  11208  fzennn  11234  fzen2  11235  sermono  11282  seqf1olem2  11290  ser1const  11306  exp1  11314  zexpcl  11323  qexpcl  11324  qexpclz  11329  m1expcl  11331  expp1z  11355  expm1  11356  facnn  11495  fac0  11496  fac1  11497  bcn1  11531  bcp1nk  11535  bcpasc  11539  hashsng  11574  hashfz  11619  fz1isolem  11637  seqcoll  11639  s2f1o  11790  f1oun2prg  11791  climuni  12273  isercoll  12388  isercoll2  12389  iseraltlem1  12402  sum0  12442  sumsn  12461  fsumtscopo  12508  fsumparts  12512  binomlem  12535  climcndslem1  12556  climcndslem2  12557  climcnds  12558  divcnv  12560  supcvg  12562  arisum  12566  trireciplem  12568  trirecip  12569  expcnv  12570  geo2sum  12577  geo2lim  12579  geoisum1  12583  geoisum1c  12584  mertenslem1  12588  mertenslem2  12589  ege2le3  12619  sin01gt0  12718  rpnnen2lem10  12750  rpnnen2  12752  nthruc  12777  iddvds  12790  1dvds  12791  dvdsle  12822  dvds1  12825  3dvds  12839  divalglem5  12844  divalg  12850  bitsfzolem  12873  bitsfzo  12874  bitscmp  12877  gcdcllem1  12938  gcdcllem3  12940  gcdaddmlem  12955  gcdadd  12957  gcdid  12958  gcd1  12959  1gcd  12964  bezoutlem1  12965  gcdmultiple  12977  isprm3  13015  phicl2  13084  phi1  13089  dfphi2  13090  hashdvds  13091  phiprmpw  13092  eulerthlem2  13098  prmdiv  13101  prmdiveq  13102  odzcllem  13105  odzdvds  13108  odzphi  13109  oddprm  13116  pythagtriplem4  13120  iserodd  13136  pcpre1  13143  pc1  13156  pcrec  13159  pcid  13173  pcmptcl  13187  pcmpt  13188  fldivp1  13193  expnprm  13198  pockthlem  13200  unbenlem  13203  prmreclem2  13212  prmreclem4  13214  prmreclem6  13216  prmrec  13217  igz  13229  4sqlem12  13251  4sqlem13  13252  4sqlem19  13258  vdwapun  13269  vdwlem8  13283  vdwlem13  13288  prmlem0  13355  1259lem4  13380  2503lem2  13384  4001lem1  13387  mulg1  14824  mulgm1  14836  mulgp1  14843  mulgneg2  14844  mulgpropd  14850  cycsubgcl  14893  odinv  15124  sylow1lem1  15159  sylow3lem6  15193  efgs1b  15295  lt6abl  15431  pgpfac1lem2  15560  qsubdrg  16674  zsubrg  16675  gzsubrg  16676  zcyg  16695  mulgrhm  16710  mulgrhm2  16711  chrnzr  16734  znunit  16767  znrrg  16769  frgpcyg  16777  lmcnp  17290  lmmo  17366  1stcelcls  17445  1stccnp  17446  1stckgenlem  17506  1stckgen  17507  zfbas  17849  imasdsf1olem  18311  clmvneg1  18987  clmmulg  18989  lmnn  19087  cmetcaulem  19112  iscmet2  19118  causs  19122  caubl  19131  iscmet3i  19135  bcthlem5  19150  ovolsf  19236  ovolctb  19253  ovolunlem1a  19259  ovolunlem1  19260  ovoliunlem1  19265  ovoliun  19268  ovoliun2  19269  ovoliunnul  19270  ovolicc1  19279  ovolicc2lem2  19281  ovolicc2lem3  19282  ovolicc2lem4  19283  voliunlem1  19311  voliunlem2  19312  voliunlem3  19313  volsup  19317  ioombl1lem4  19322  uniioombllem2  19342  uniioombllem3  19344  uniioombllem6  19347  vitalilem4  19370  vitalilem5  19371  itg1climres  19473  mbfi1fseqlem6  19479  mbfi1flimlem  19481  mbfmullem2  19483  itg2monolem1  19509  itg2i1fseq  19514  itg2i1fseq2  19515  itg2addlem  19517  plyeq0lem  19996  dvply1  20068  vieta1lem2  20095  elqaalem2  20104  qaa  20107  iaa  20109  dvtaylp  20153  dvradcnv  20204  pserdvlem2  20211  pserdv2  20213  abelthlem6  20219  abelthlem9  20223  sin2pim  20260  cos2pim  20261  efif1olem2  20312  advlogexp  20413  logtayl  20418  logtaylsum  20419  logtayl2  20420  ang180lem3  20520  1cubrlem  20548  atantayl  20644  leibpilem2  20648  leibpi  20649  birthdaylem2  20658  dfef2  20676  divsqrsumlem  20685  emcllem4  20704  emcllem5  20705  emcllem6  20706  emcllem7  20707  wilthlem1  20718  wilthlem2  20719  wilthlem3  20720  basellem6  20735  basellem7  20736  basellem8  20737  basellem9  20738  muf  20790  ppip1le  20811  ppi1  20814  cht1  20815  chp1  20817  cht2  20822  ppieq0  20826  ppiub  20855  chpeq0  20859  chpchtsum  20870  chpub  20871  logfacbnd3  20874  logexprlim  20876  mersenne  20878  perfectlem1  20880  perfectlem2  20881  bposlem1  20935  bposlem2  20936  bposlem5  20939  bposlem6  20940  lgslem1  20947  lgslem2  20948  lgsfcl2  20953  lgsval2lem  20957  lgsdir2lem1  20974  lgsdir2lem3  20976  lgsdir2lem4  20977  lgsdir2lem5  20978  lgsqrlem1  20992  lgsdchr  20999  lgseisenlem1  21000  lgseisenlem2  21001  lgseisenlem4  21003  lgsquad2lem1  21009  lgsquad3  21012  m1lgs  21013  2sqlem9  21024  2sqlem10  21025  2sqlem11  21026  2sqblem  21028  2sqb  21029  dchrisumlema  21049  dchrisumlem3  21052  dchrmusum2  21055  dchrvmasumiflem1  21062  dchrvmaeq0  21065  dchrisum0re  21074  dchrisum0lem1b  21076  dchrisum0lem2a  21078  logdivsum  21094  log2sumbnd  21105  pntrlog2bndlem1  21138  pntpbnd2  21148  qabvle  21186  ostth3  21199  usgraexmpldifpr  21285  usgraexmpl  21286  0pth  21424  constr1trl  21436  2trllem3  21444  2trllem4  21445  constr2trl  21446  2pthonlem2  21448  redwlk  21454  fargshiftlem  21469  usgrcyclnl1  21475  usgrcyclnl2  21476  3v3e3cycl1  21479  constr3lem4  21482  constr3trllem3  21487  constr3trllem5  21489  constr3pthlem1  21490  constr3pthlem2  21491  constr3pthlem3  21492  4cycl4v4e  21501  4cycl4dv4e  21503  eupap1  21546  eupath2lem3  21549  ex-fl  21603  gx1  21698  gxm1  21704  nvlmle  22036  ipval2  22051  minvecolem3  22226  minvecolem4b  22228  minvecolem4  22230  h2hcau  22330  h2hlm  22331  hlimadd  22543  hlim0  22586  hhsscms  22627  occllem  22653  nlelchi  23412  opsqrlem2  23492  opsqrlem4  23494  hmopidmchi  23502  iuninc  23855  fzspl  23985  fzsplit3  23986  gsumpropd2lem  24049  zzsmulg  24081  lmlim  24137  rge0scvg  24139  lmxrge0  24141  lmdvg  24142  qqhval2lem  24164  qqh0  24167  qqh1  24168  rnlogblem  24195  logblt  24202  esumfzf  24255  esumfsup  24256  esumfsupre  24257  esumpcvgval  24264  esumcvg  24272  dya2ub  24414  rrvsum  24491  dstfrvclim1  24514  ballotlem2  24525  ballotlemfp1  24528  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemimin  24542  ballotlemic  24543  ballotlem1c  24544  ballotlemsdom  24548  ballotlemsel1i  24549  ballotlemsima  24552  ballotlemfrceq  24565  ballotlemfrcn0  24566  zetacvg  24578  lgamgulmlem4  24595  lgamgulmlem6  24597  lgamgulm2  24599  lgamcvglem  24603  lgamcvg2  24618  gamcvg  24619  gamcvg2lem  24622  regamcl  24624  relgamcl  24625  lgam1  24627  subfac1  24643  subfacp1lem1  24644  subfacp1lem2a  24645  subfacp1lem5  24649  subfacp1lem6  24650  cvmliftlem10  24760  sinccvg  24889  circum  24890  elfzp1b  24895  fznatpl1  24977  bcnm1  24980  divcnvshft  24990  divcnvlin  24991  prod0  25048  fprodser  25054  fprodzcl  25059  prodsn  25065  risefacval2  25095  fallfacval2  25096  zrisefaccl  25104  zfallfaccl  25105  risefall0lem  25110  faclimlem1  25120  faclimlem2  25121  faclim  25123  iprodfac  25124  faclim2  25125  axlowdimlem3  25597  axlowdimlem4  25598  axlowdimlem6  25600  axlowdimlem7  25601  axlowdimlem16  25610  axlowdimlem17  25611  axlowdim  25614  bpolydiflem  25814  ovoliunnfl  25953  voliunnfl  25955  fdc  26140  lmclim2  26155  geomcau  26156  heibor1lem  26209  heibor1  26210  bfplem1  26222  bfplem2  26223  rrncmslem  26232  rrncms  26233  mapfzcons  26463  mzpexpmpt  26493  fzsplit1nn0  26503  eldioph2lem1  26509  eldioph3b  26514  fz1eqin  26518  diophin  26522  diophun  26523  0dioph  26528  elnnrabdioph  26558  rabren3dioph  26567  irrapxlem1  26576  irrapxlem3  26578  pellexlem6  26588  rmspecnonsq  26661  rmxyadd  26675  rmxy1  26676  rmxy0  26677  rmxp1  26686  rmyp1  26687  rmxm1  26688  rmym1  26689  jm2.24nn  26715  acongeq  26739  jm2.22  26757  jm2.23  26758  jm2.25  26761  jm2.15nn0  26765  jm2.16nn0  26766  jm2.27c  26769  jm2.27dlem2  26772  rmydioph  26776  rmxdioph  26778  expdiophlem2  26784  expdioph  26785  mpaaeu  27024  sumsnd  27365  fmuldfeq  27381  fmul01lt1lem2  27383  fmul01lt1  27384  clim1fr1  27395  stoweidlem3  27420  stoweidlem7  27424  stoweidlem11  27428  stoweidlem14  27431  stoweidlem20  27437  stoweidlem26  27443  stoweidlem34  27451  stoweidlem51  27468  wallispilem4  27485  wallispilem5  27486  wallispi  27487  wallispi2lem1  27488  wallispi2lem2  27489  stirlinglem1  27491  stirlinglem5  27495  stirlinglem7  27497  stirlinglem8  27498  stirlinglem11  27501  stirlinglem12  27502  stirlinglem13  27503  stirlinglem14  27504  stirlinglem15  27505  stirlingr  27507
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-riota 6485  df-recs 6569  df-rdg 6604  df-er 6841  df-en 7046  df-dom 7047  df-sdom 7048  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-nn 9933  df-z 10215
  Copyright terms: Public domain W3C validator