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

Theorem 1z 10300
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 10000 . 2  |-  1  e.  NN
21nnzi 10294 1  |-  1  e.  ZZ
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   1c1 8980   ZZcz 10271
This theorem is referenced by:  peano2z  10307  peano2zm  10309  peano5uzti  10348  nnuz  10510  eluz2b1  10536  uz2m1nn  10539  nninfm  10545  nnrecq  10586  qbtwnxr  10775  fz1n  11062  fz10  11064  fz01en  11068  fzprval  11095  fztpval  11096  4fvwrd4  11109  fseq1p1m1  11110  elfzm1b  11113  fzm1  11115  fzoss2  11151  fzo12sn  11171  fzofzp1  11177  elfznelfzo  11180  fzostep1  11185  injresinj  11188  flge1nn  11214  modnegd  11269  fzennn  11295  fzen2  11296  sermono  11343  seqf1olem2  11351  ser1const  11367  exp1  11375  zexpcl  11384  qexpcl  11385  qexpclz  11390  m1expcl  11392  expp1z  11416  expm1  11417  facnn  11556  fac0  11557  fac1  11558  bcn1  11592  bcp1nk  11596  bcpasc  11600  hashsng  11635  hashfz  11680  fz1isolem  11698  seqcoll  11700  s2f1o  11851  f1oun2prg  11852  climuni  12334  isercoll  12449  isercoll2  12450  iseraltlem1  12463  sum0  12503  sumsn  12522  fsumtscopo  12569  fsumparts  12573  binomlem  12596  climcndslem1  12617  climcndslem2  12618  climcnds  12619  divcnv  12621  supcvg  12623  arisum  12627  trireciplem  12629  trirecip  12630  expcnv  12631  geo2sum  12638  geo2lim  12640  geoisum1  12644  geoisum1c  12645  mertenslem1  12649  mertenslem2  12650  ege2le3  12680  sin01gt0  12779  rpnnen2lem10  12811  rpnnen2  12813  nthruc  12838  iddvds  12851  1dvds  12852  dvdsle  12883  dvds1  12886  3dvds  12900  divalglem5  12905  divalg  12911  bitsfzolem  12934  bitsfzo  12935  bitscmp  12938  gcdcllem1  12999  gcdcllem3  13001  gcdaddmlem  13016  gcdadd  13018  gcdid  13019  gcd1  13020  1gcd  13025  bezoutlem1  13026  gcdmultiple  13038  isprm3  13076  phicl2  13145  phi1  13150  dfphi2  13151  hashdvds  13152  phiprmpw  13153  eulerthlem2  13159  prmdiv  13162  prmdiveq  13163  odzcllem  13166  odzdvds  13169  odzphi  13170  oddprm  13177  pythagtriplem4  13181  iserodd  13197  pcpre1  13204  pc1  13217  pcrec  13220  pcid  13234  pcmptcl  13248  pcmpt  13249  fldivp1  13254  expnprm  13259  pockthlem  13261  unbenlem  13264  prmreclem2  13273  prmreclem4  13275  prmreclem6  13277  prmrec  13278  igz  13290  4sqlem12  13312  4sqlem13  13313  4sqlem19  13319  vdwapun  13330  vdwlem8  13344  vdwlem13  13349  prmlem0  13416  1259lem4  13441  2503lem2  13445  4001lem1  13448  mulg1  14885  mulgm1  14897  mulgp1  14904  mulgneg2  14905  mulgpropd  14911  cycsubgcl  14954  odinv  15185  sylow1lem1  15220  sylow3lem6  15254  efgs1b  15356  lt6abl  15492  pgpfac1lem2  15621  qsubdrg  16739  zsubrg  16740  gzsubrg  16741  zcyg  16760  mulgrhm  16775  mulgrhm2  16776  chrnzr  16799  znunit  16832  znrrg  16834  frgpcyg  16842  lmcnp  17356  lmmo  17432  1stcelcls  17512  1stccnp  17513  1stckgenlem  17573  1stckgen  17574  zfbas  17916  imasdsf1olem  18391  clmvneg1  19104  clmmulg  19106  lmnn  19204  cmetcaulem  19229  iscmet2  19235  causs  19239  caubl  19248  iscmet3i  19252  bcthlem5  19269  ovolsf  19357  ovolctb  19374  ovolunlem1a  19380  ovolunlem1  19381  ovoliunlem1  19386  ovoliun  19389  ovoliun2  19390  ovoliunnul  19391  ovolicc1  19400  ovolicc2lem2  19402  ovolicc2lem3  19403  ovolicc2lem4  19404  voliunlem1  19432  voliunlem2  19433  voliunlem3  19434  volsup  19438  ioombl1lem4  19443  uniioombllem2  19463  uniioombllem3  19465  uniioombllem6  19468  vitalilem4  19491  vitalilem5  19492  itg1climres  19594  mbfi1fseqlem6  19600  mbfi1flimlem  19602  mbfmullem2  19604  itg2monolem1  19630  itg2i1fseq  19635  itg2i1fseq2  19636  itg2addlem  19638  plyeq0lem  20117  dvply1  20189  vieta1lem2  20216  elqaalem2  20225  qaa  20228  iaa  20230  dvtaylp  20274  dvradcnv  20325  pserdvlem2  20332  pserdv2  20334  abelthlem6  20340  abelthlem9  20344  sin2pim  20381  cos2pim  20382  efif1olem2  20433  advlogexp  20534  logtayl  20539  logtaylsum  20540  logtayl2  20541  ang180lem3  20641  1cubrlem  20669  atantayl  20765  leibpilem2  20769  leibpi  20770  birthdaylem2  20779  dfef2  20797  divsqrsumlem  20806  emcllem4  20825  emcllem5  20826  emcllem6  20827  emcllem7  20828  wilthlem1  20839  wilthlem2  20840  wilthlem3  20841  basellem6  20856  basellem7  20857  basellem8  20858  basellem9  20859  muf  20911  ppip1le  20932  ppi1  20935  cht1  20936  chp1  20938  cht2  20943  ppieq0  20947  ppiub  20976  chpeq0  20980  chpchtsum  20991  chpub  20992  logfacbnd3  20995  logexprlim  20997  mersenne  20999  perfectlem1  21001  perfectlem2  21002  bposlem1  21056  bposlem2  21057  bposlem5  21060  bposlem6  21061  lgslem1  21068  lgslem2  21069  lgsfcl2  21074  lgsval2lem  21078  lgsdir2lem1  21095  lgsdir2lem3  21097  lgsdir2lem4  21098  lgsdir2lem5  21099  lgsqrlem1  21113  lgsdchr  21120  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem4  21124  lgsquad2lem1  21130  lgsquad3  21133  m1lgs  21134  2sqlem9  21145  2sqlem10  21146  2sqlem11  21147  2sqblem  21149  2sqb  21150  dchrisumlema  21170  dchrisumlem3  21173  dchrmusum2  21176  dchrvmasumiflem1  21183  dchrvmaeq0  21186  dchrisum0re  21195  dchrisum0lem1b  21197  dchrisum0lem2a  21199  logdivsum  21215  log2sumbnd  21226  pntrlog2bndlem1  21259  pntpbnd2  21269  qabvle  21307  ostth3  21320  usgraexmpldifpr  21407  usgraexmpl  21408  2trllemD  21545  2trllemG  21546  0pth  21558  constr1trl  21576  constr2spthlem1  21582  redwlk  21594  fargshiftlem  21609  usgrcyclnl1  21615  usgrcyclnl2  21616  3v3e3cycl1  21619  constr3lem4  21622  constr3trllem3  21627  constr3trllem5  21629  constr3pthlem1  21630  constr3pthlem2  21631  constr3pthlem3  21632  4cycl4v4e  21641  4cycl4dv4e  21643  eupap1  21686  eupath2lem3  21689  ex-fl  21743  gx1  21838  gxm1  21844  nvlmle  22176  ipval2  22191  minvecolem3  22366  minvecolem4b  22368  minvecolem4  22370  h2hcau  22470  h2hlm  22471  hlimadd  22683  hlim0  22726  hhsscms  22767  occllem  22793  nlelchi  23552  opsqrlem2  23632  opsqrlem4  23634  hmopidmchi  23642  iuninc  23999  fzspl  24137  fzsplit3  24138  gsumpropd2lem  24208  zzsmulg  24253  lmlim  24321  rge0scvg  24323  lmxrge0  24325  lmdvg  24326  qqhval2lem  24353  qqh0  24356  qqh1  24357  rnlogblem  24387  logblt  24394  esumfzf  24447  esumfsup  24448  esumfsupre  24449  esumpcvgval  24456  esumcvg  24464  dya2ub  24608  rrvsum  24700  dstfrvclim1  24723  ballotlem2  24734  ballotlemfp1  24737  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemimin  24751  ballotlemic  24752  ballotlem1c  24753  ballotlemsdom  24757  ballotlemsel1i  24758  ballotlemsima  24761  ballotlemfrceq  24774  ballotlemfrcn0  24775  zetacvg  24787  lgamgulmlem4  24804  lgamgulmlem6  24806  lgamgulm2  24808  lgamcvglem  24812  lgamcvg2  24827  gamcvg  24828  gamcvg2lem  24831  regamcl  24833  relgamcl  24834  lgam1  24836  subfac1  24852  subfacp1lem1  24853  subfacp1lem2a  24854  subfacp1lem5  24858  subfacp1lem6  24859  cvmliftlem10  24969  sinccvg  25098  circum  25099  elfzp1b  25104  fznatpl1  25186  bcnm1  25189  divcnvshft  25199  divcnvlin  25200  prod0  25258  fprodser  25264  fprodzcl  25269  prodsn  25275  iprodgam  25308  risefacval2  25315  fallfacval2  25316  zrisefaccl  25325  zfallfaccl  25326  risefall0lem  25331  binomfallfaclem2  25345  faclimlem1  25351  faclimlem2  25352  faclim  25354  iprodfac  25355  faclim2  25356  axlowdimlem3  25831  axlowdimlem4  25832  axlowdimlem6  25834  axlowdimlem7  25835  axlowdimlem16  25844  axlowdimlem17  25845  axlowdim  25848  bpolydiflem  26048  mblfinlem  26190  ovoliunnfl  26194  voliunnfl  26196  fdc  26386  lmclim2  26401  geomcau  26402  heibor1lem  26455  heibor1  26456  bfplem1  26468  bfplem2  26469  rrncmslem  26478  rrncms  26479  mapfzcons  26709  mzpexpmpt  26739  fzsplit1nn0  26749  eldioph2lem1  26755  eldioph3b  26760  fz1eqin  26764  diophin  26768  diophun  26769  0dioph  26774  elnnrabdioph  26804  rabren3dioph  26813  irrapxlem1  26822  irrapxlem3  26824  pellexlem6  26834  rmspecnonsq  26907  rmxyadd  26921  rmxy1  26922  rmxy0  26923  rmxp1  26932  rmyp1  26933  rmxm1  26934  rmym1  26935  jm2.24nn  26961  acongeq  26985  jm2.22  27003  jm2.23  27004  jm2.25  27007  jm2.15nn0  27011  jm2.16nn0  27012  jm2.27c  27015  jm2.27dlem2  27018  rmydioph  27022  rmxdioph  27024  expdiophlem2  27030  expdioph  27031  mpaaeu  27270  sumsnd  27611  fmuldfeq  27627  fmul01lt1lem2  27629  fmul01lt1  27630  clim1fr1  27641  stoweidlem3  27666  stoweidlem7  27670  stoweidlem11  27674  stoweidlem14  27677  stoweidlem20  27683  stoweidlem26  27689  stoweidlem34  27697  stoweidlem51  27714  wallispilem4  27731  wallispilem5  27732  wallispi  27733  wallispi2lem1  27734  wallispi2lem2  27735  stirlinglem1  27737  stirlinglem5  27741  stirlinglem7  27743  stirlinglem8  27744  stirlinglem11  27747  stirlinglem12  27748  stirlinglem13  27749  stirlinglem14  27750  stirlinglem15  27751  stirlingr  27753  f13idfv  28013  ubmelm1fzo  28039  fzo1fzo0n0  28040  2submod  28058  modid0  28065  modidmul0  28066  prmgt1  28107  modprm1div  28108  shwrdssizelem1a  28165
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055  ax-pre-mulgt0 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-riota 6540  df-recs 6624  df-rdg 6659  df-er 6896  df-en 7101  df-dom 7102  df-sdom 7103  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-sub 9282  df-neg 9283  df-nn 9990  df-z 10272
  Copyright terms: Public domain W3C validator