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

Theorem 1z 10342
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 10042 . 2  |-  1  e.  NN
21nnzi 10336 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1727   1c1 9022   ZZcz 10313
This theorem is referenced by:  peano2z  10349  peano2zm  10351  peano5uzti  10390  nnuz  10552  eluz2b1  10578  uz2m1nn  10581  nninfm  10587  nnrecq  10628  qbtwnxr  10817  fz1n  11104  fz10  11106  fz01en  11110  fzprval  11137  fztpval  11138  4fvwrd4  11152  fseq1p1m1  11153  elfzm1b  11156  fzm1  11158  fzoss2  11194  fzo12sn  11214  fzofzp1  11220  elfznelfzo  11223  fzostep1  11228  injresinj  11231  flge1nn  11257  modnegd  11312  fzennn  11338  fzen2  11339  sermono  11386  seqf1olem2  11394  ser1const  11410  exp1  11418  zexpcl  11427  qexpcl  11428  qexpclz  11433  m1expcl  11435  expp1z  11459  expm1  11460  facnn  11599  fac0  11600  fac1  11601  bcn1  11635  bcp1nk  11639  bcpasc  11643  hashsng  11678  hashfz  11723  fz1isolem  11741  seqcoll  11743  s2f1o  11894  f1oun2prg  11895  climuni  12377  isercoll  12492  isercoll2  12493  iseraltlem1  12506  sum0  12546  sumsn  12565  fsumtscopo  12612  fsumparts  12616  binomlem  12639  climcndslem1  12660  climcndslem2  12661  climcnds  12662  divcnv  12664  supcvg  12666  arisum  12670  trireciplem  12672  trirecip  12673  expcnv  12674  geo2sum  12681  geo2lim  12683  geoisum1  12687  geoisum1c  12688  mertenslem1  12692  mertenslem2  12693  ege2le3  12723  sin01gt0  12822  rpnnen2lem10  12854  rpnnen2  12856  nthruc  12881  iddvds  12894  1dvds  12895  dvdsle  12926  dvds1  12929  3dvds  12943  divalglem5  12948  divalg  12954  bitsfzolem  12977  bitsfzo  12978  bitscmp  12981  gcdcllem1  13042  gcdcllem3  13044  gcdaddmlem  13059  gcdadd  13061  gcdid  13062  gcd1  13063  1gcd  13068  bezoutlem1  13069  gcdmultiple  13081  isprm3  13119  phicl2  13188  phi1  13193  dfphi2  13194  hashdvds  13195  phiprmpw  13196  eulerthlem2  13202  prmdiv  13205  prmdiveq  13206  odzcllem  13209  odzdvds  13212  odzphi  13213  oddprm  13220  pythagtriplem4  13224  iserodd  13240  pcpre1  13247  pc1  13260  pcrec  13263  pcid  13277  pcmptcl  13291  pcmpt  13292  fldivp1  13297  expnprm  13302  pockthlem  13304  unbenlem  13307  prmreclem2  13316  prmreclem4  13318  prmreclem6  13320  prmrec  13321  igz  13333  4sqlem12  13355  4sqlem13  13356  4sqlem19  13362  vdwapun  13373  vdwlem8  13387  vdwlem13  13392  prmlem0  13459  1259lem4  13484  2503lem2  13488  4001lem1  13491  mulg1  14928  mulgm1  14940  mulgp1  14947  mulgneg2  14948  mulgpropd  14954  cycsubgcl  14997  odinv  15228  sylow1lem1  15263  sylow3lem6  15297  efgs1b  15399  lt6abl  15535  pgpfac1lem2  15664  qsubdrg  16782  zsubrg  16783  gzsubrg  16784  zcyg  16803  mulgrhm  16818  mulgrhm2  16819  chrnzr  16842  znunit  16875  znrrg  16877  frgpcyg  16885  lmcnp  17399  lmmo  17475  1stcelcls  17555  1stccnp  17556  1stckgenlem  17616  1stckgen  17617  zfbas  17959  imasdsf1olem  18434  clmvneg1  19147  clmmulg  19149  lmnn  19247  cmetcaulem  19272  iscmet2  19278  causs  19282  caubl  19291  iscmet3i  19295  bcthlem5  19312  ovolsf  19400  ovolctb  19417  ovolunlem1a  19423  ovolunlem1  19424  ovoliunlem1  19429  ovoliun  19432  ovoliun2  19433  ovoliunnul  19434  ovolicc1  19443  ovolicc2lem2  19445  ovolicc2lem3  19446  ovolicc2lem4  19447  voliunlem1  19475  voliunlem2  19476  voliunlem3  19477  volsup  19481  ioombl1lem4  19486  uniioombllem2  19506  uniioombllem3  19508  uniioombllem6  19511  vitalilem4  19534  vitalilem5  19535  itg1climres  19635  mbfi1fseqlem6  19641  mbfi1flimlem  19643  mbfmullem2  19645  itg2monolem1  19671  itg2i1fseq  19676  itg2i1fseq2  19677  itg2addlem  19679  plyeq0lem  20160  dvply1  20232  vieta1lem2  20259  elqaalem2  20268  qaa  20271  iaa  20273  dvtaylp  20317  dvradcnv  20368  pserdvlem2  20375  pserdv2  20377  abelthlem6  20383  abelthlem9  20387  sin2pim  20424  cos2pim  20425  efif1olem2  20476  advlogexp  20577  logtayl  20582  logtaylsum  20583  logtayl2  20584  ang180lem3  20684  1cubrlem  20712  atantayl  20808  leibpilem2  20812  leibpi  20813  birthdaylem2  20822  dfef2  20840  divsqrsumlem  20849  emcllem4  20868  emcllem5  20869  emcllem6  20870  emcllem7  20871  wilthlem1  20882  wilthlem2  20883  wilthlem3  20884  basellem6  20899  basellem7  20900  basellem8  20901  basellem9  20902  muf  20954  ppip1le  20975  ppi1  20978  cht1  20979  chp1  20981  cht2  20986  ppieq0  20990  ppiub  21019  chpeq0  21023  chpchtsum  21034  chpub  21035  logfacbnd3  21038  logexprlim  21040  mersenne  21042  perfectlem1  21044  perfectlem2  21045  bposlem1  21099  bposlem2  21100  bposlem5  21103  bposlem6  21104  lgslem1  21111  lgslem2  21112  lgsfcl2  21117  lgsval2lem  21121  lgsdir2lem1  21138  lgsdir2lem3  21140  lgsdir2lem4  21141  lgsdir2lem5  21142  lgsqrlem1  21156  lgsdchr  21163  lgseisenlem1  21164  lgseisenlem2  21165  lgseisenlem4  21167  lgsquad2lem1  21173  lgsquad3  21176  m1lgs  21177  2sqlem9  21188  2sqlem10  21189  2sqlem11  21190  2sqblem  21192  2sqb  21193  dchrisumlema  21213  dchrisumlem3  21216  dchrmusum2  21219  dchrvmasumiflem1  21226  dchrvmaeq0  21229  dchrisum0re  21238  dchrisum0lem1b  21240  dchrisum0lem2a  21242  logdivsum  21258  log2sumbnd  21269  pntrlog2bndlem1  21302  pntpbnd2  21312  qabvle  21350  ostth3  21363  usgraexmpldifpr  21450  usgraexmpl  21451  2trllemD  21588  2trllemG  21589  0pth  21601  constr1trl  21619  constr2spthlem1  21625  redwlk  21637  fargshiftlem  21652  usgrcyclnl1  21658  usgrcyclnl2  21659  3v3e3cycl1  21662  constr3lem4  21665  constr3trllem3  21670  constr3trllem5  21672  constr3pthlem1  21673  constr3pthlem2  21674  constr3pthlem3  21675  4cycl4v4e  21684  4cycl4dv4e  21686  eupap1  21729  eupath2lem3  21732  ex-fl  21786  gx1  21881  gxm1  21887  nvlmle  22219  ipval2  22234  minvecolem3  22409  minvecolem4b  22411  minvecolem4  22413  h2hcau  22513  h2hlm  22514  hlimadd  22726  hlim0  22769  hhsscms  22810  occllem  22836  nlelchi  23595  opsqrlem2  23675  opsqrlem4  23677  hmopidmchi  23685  iuninc  24042  fzspl  24180  fzsplit3  24181  gsumpropd2lem  24251  zzsmulg  24296  lmlim  24364  rge0scvg  24366  lmxrge0  24368  lmdvg  24369  qqhval2lem  24396  qqh0  24399  qqh1  24400  rnlogblem  24430  logblt  24437  esumfzf  24490  esumfsup  24491  esumfsupre  24492  esumpcvgval  24499  esumcvg  24507  dya2ub  24651  rrvsum  24743  dstfrvclim1  24766  ballotlem2  24777  ballotlemfp1  24780  ballotlemfc0  24781  ballotlemfcc  24782  ballotlemimin  24794  ballotlemic  24795  ballotlem1c  24796  ballotlemsdom  24800  ballotlemsel1i  24801  ballotlemsima  24804  ballotlemfrceq  24817  ballotlemfrcn0  24818  zetacvg  24830  lgamgulmlem4  24847  lgamgulmlem6  24849  lgamgulm2  24851  lgamcvglem  24855  lgamcvg2  24870  gamcvg  24871  gamcvg2lem  24874  regamcl  24876  relgamcl  24877  lgam1  24879  subfac1  24895  subfacp1lem1  24896  subfacp1lem2a  24897  subfacp1lem5  24901  subfacp1lem6  24902  cvmliftlem10  25012  sinccvg  25141  circum  25142  elfzp1b  25147  fznatpl1  25229  bcnm1  25232  divcnvshft  25242  divcnvlin  25243  prod0  25300  fprodser  25306  fprodzcl  25311  prodsn  25317  iprodgam  25350  risefacval2  25357  fallfacval2  25358  zrisefaccl  25367  zfallfaccl  25368  risefall0lem  25373  binomfallfaclem2  25387  faclimlem1  25393  faclimlem2  25394  faclim  25396  iprodfac  25397  faclim2  25398  axlowdimlem3  25914  axlowdimlem4  25915  axlowdimlem6  25917  axlowdimlem7  25918  axlowdimlem16  25927  axlowdimlem17  25928  axlowdim  25931  bpolydiflem  26131  mblfinlem1  26279  mblfinlem2  26280  ovoliunnfl  26284  voliunnfl  26286  fdc  26487  lmclim2  26502  geomcau  26503  heibor1lem  26556  heibor1  26557  bfplem1  26569  bfplem2  26570  rrncmslem  26579  rrncms  26580  mapfzcons  26810  mzpexpmpt  26840  fzsplit1nn0  26850  eldioph2lem1  26856  eldioph3b  26861  fz1eqin  26865  diophin  26869  diophun  26870  0dioph  26875  elnnrabdioph  26905  rabren3dioph  26914  irrapxlem1  26923  irrapxlem3  26925  pellexlem6  26935  rmspecnonsq  27008  rmxyadd  27022  rmxy1  27023  rmxy0  27024  rmxp1  27033  rmyp1  27034  rmxm1  27035  rmym1  27036  jm2.24nn  27062  acongeq  27086  jm2.22  27104  jm2.23  27105  jm2.25  27108  jm2.15nn0  27112  jm2.16nn0  27113  jm2.27c  27116  jm2.27dlem2  27119  rmydioph  27123  rmxdioph  27125  expdiophlem2  27131  expdioph  27132  mpaaeu  27370  sumsnd  27711  fmuldfeq  27727  fmul01lt1lem2  27729  fmul01lt1  27730  clim1fr1  27741  stoweidlem3  27766  stoweidlem7  27770  stoweidlem11  27774  stoweidlem14  27777  stoweidlem20  27783  stoweidlem26  27789  stoweidlem34  27797  stoweidlem51  27814  wallispilem4  27831  wallispilem5  27832  wallispi  27833  wallispi2lem1  27834  wallispi2lem2  27835  stirlinglem1  27837  stirlinglem5  27841  stirlinglem7  27843  stirlinglem8  27844  stirlinglem11  27847  stirlinglem12  27848  stirlinglem13  27849  stirlinglem14  27850  stirlinglem15  27851  stirlingr  27853  f13idfv  28124  1eluzge0  28147  2eluzge1  28149  ubmelm1fzo  28174  fzo1fzo0n0  28175  2submod  28199  modid0  28206  modidmul0  28207  prmgt1  28281  modprm1div  28282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-mulcom 9085  ax-addass 9086  ax-mulass 9087  ax-distr 9088  ax-i2m1 9089  ax-1ne0 9090  ax-1rid 9091  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094  ax-pre-lttri 9095  ax-pre-lttrn 9096  ax-pre-ltadd 9097  ax-pre-mulgt0 9098
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 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-riota 6578  df-recs 6662  df-rdg 6697  df-er 6934  df-en 7139  df-dom 7140  df-sdom 7141  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157  df-sub 9324  df-neg 9325  df-nn 10032  df-z 10314
  Copyright terms: Public domain W3C validator