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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 10572 . 2
21nnzi 10913 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  1c1 9514   cz 10889
This theorem is referenced by:  1zzd  10920  peano2z  10930  peano2zm  10932  peano5uzti  10977  nnuz  11145  eluz2nn  11148  eluzge3nn  11151  1eluzge0  11153  2eluzge1  11156  eluz2b1  11182  uz2m1nn  11185  nninfm  11191  nnrecq  11234  qbtwnxr  11428  fz1n  11733  fz10  11735  fz01en  11742  fznatpl1  11763  fzprval  11769  fztpval  11770  fseq1p1m1  11781  elfzp1b  11784  elfzm1b  11785  4fvwrd4  11822  ige2m2fzo  11879  fzo12sn  11898  fzofzp1  11909  fzostep1  11922  flge1nn  11955  modid0  12021  modidmul0  12022  fzennn  12078  fzen2  12079  f13idfv  12106  ser1const  12163  exp1  12172  zexpcl  12181  qexpcl  12182  qexpclz  12187  m1expcl  12189  expp1z  12214  expm1  12215  facnn  12355  fac0  12356  fac1  12357  bcn1  12391  bcpasc  12399  hashsng  12438  hashfz  12485  fz1isolem  12510  seqcoll  12512  ccat2s1p2  12633  s2f1o  12864  f1oun2prg  12865  swrd2lsw  12890  2swrd2eqwrdeq  12891  climuni  13375  isercoll2  13491  iseraltlem1  13504  sum0  13543  sumsn  13563  climcndslem1  13661  climcndslem2  13662  supcvg  13667  prod0  13750  prodsn  13767  sin01gt0  13925  rpnnen2lem10  13957  nthruc  13984  iddvds  13997  1dvds  13998  dvdsle  14031  dvds1  14034  3dvds  14050  divalglem5  14055  divalg  14061  bitsfzolem  14084  bitsfzo  14085  gcdcllem1  14149  gcdcllem3  14151  gcdaddmlem  14166  gcdadd  14168  gcdid  14169  gcd1  14170  1gcd  14175  bezoutlem1  14176  gcdmultiple  14188  isprm3  14226  prmgt1  14236  phicl2  14298  phi1  14303  dfphi2  14304  eulerthlem2  14312  prmdiv  14315  prmdiveq  14316  odzcllem  14319  oddprm  14339  pythagtriplem4  14343  pcpre1  14366  pc1  14379  pcrec  14382  pcmpt  14411  fldivp1  14416  expnprm  14421  pockthlem  14423  unbenlem  14426  prmreclem2  14435  prmrec  14440  igz  14452  4sqlem12  14474  4sqlem13  14475  4sqlem19  14481  vdwlem8  14506  vdwlem13  14511  prmlem0  14591  1259lem4  14616  2503lem2  14620  4001lem1  14623  gsumpropd2lem  15900  mulg1  16149  mulgm1  16161  mulgp1  16168  mulgneg2  16169  cycsubgcl  16227  odinv  16583  efgs1b  16754  lt6abl  16897  pgpfac1lem2  17126  srgbinomlem4  17194  qsubdrg  18470  zsubrg  18471  gzsubrg  18472  zringmulg  18496  zrngmulg  18503  zringcyg  18513  zcyg  18518  mulgrhm  18532  mulgrhm2  18533  mulgrhmOLD  18535  chrnzr  18567  frgpcyg  18612  zrhpsgnmhm  18620  zrhpsgnodpm  18628  m2detleiblem1  19126  m2detleiblem2  19130  zfbas  20397  imasdsf1olem  20876  cmetcaulem  21727  bcthlem5  21767  ovolctb  21901  ovolunlem1a  21907  ovolunlem1  21908  ovoliunnul  21918  ovolicc1  21927  ovolicc2lem4  21931  voliunlem1  21960  volsup  21966  uniioombllem6  21997  vitalilem5  22021  plyeq0lem  22607  vieta1lem2  22707  elqaalem2  22716  qaa  22719  iaa  22721  abelthlem6  22831  abelthlem9  22835  sin2pim  22878  cos2pim  22879  1cubrlem  23172  leibpilem2  23272  emcllem5  23329  emcllem7  23331  wilthlem2  23343  wilthlem3  23344  ppip1le  23435  ppi1  23438  cht1  23439  chp1  23441  cht2  23446  ppieq0  23450  ppiub  23479  chpeq0  23483  chpchtsum  23494  chpub  23495  logfacbnd3  23498  logexprlim  23500  bposlem1  23559  bposlem2  23560  bposlem5  23563  bposlem6  23564  lgslem2  23572  lgsfcl2  23577  lgsval2lem  23581  lgsdir2lem1  23598  lgsdir2lem5  23602  lgsdchr  23623  2sqlem9  23648  2sqlem10  23649  2sqblem  23652  2sqb  23653  dchrisumlem3  23676  log2sumbnd  23729  qabvle  23810  ostth3  23823  tgldimor  23893  axlowdimlem3  24247  axlowdimlem4  24248  axlowdimlem6  24250  axlowdimlem7  24251  axlowdimlem16  24260  axlowdimlem17  24261  axlowdim  24264  usgraexmpldifpr  24400  usgraexmpl  24401  2trllemD  24559  2trllemG  24560  0pth  24572  constr1trl  24590  constr2spthlem1  24596  fargshiftlem  24634  usgrcyclnl1  24640  3v3e3cycl1  24644  constr3lem4  24647  constr3trllem3  24652  constr3trllem5  24654  constr3pthlem1  24655  constr3pthlem2  24656  constr3pthlem3  24657  eupap1  24976  eupath2lem3  24979  ex-fl  25168  gx1  25264  gxm1  25270  ipval2  25617  hlim0  26153  opsqrlem2  27060  iuninc  27428  nndiffz1  27596  lmlim  27929  qqh0  27965  qqh1  27966  logblt  28022  esumfzf  28075  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  dya2ub  28241  rrvsum  28393  dstfrvclim1  28416  ballotlem2  28427  ballotlemfc0  28431  ballotlemfcc  28432  signsvf0  28537  lgamgulm2  28578  lgamcvglem  28582  gamcvg2lem  28601  lgam1  28606  subfac1  28622  subfacp1lem1  28623  subfacp1lem2a  28624  subfacp1lem5  28628  subfacp1lem6  28629  cvmliftlem10  28739  bcnm1  29109  divcnvshft  29117  divcnvlin  29118  zrisefaccl  29142  zfallfaccl  29143  faclimlem1  29168  mblfinlem1  30051  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  fdc  30238  heibor1lem  30305  rrncmslem  30328  mapfzcons  30648  mzpexpmpt  30677  eldioph3b  30698  fz1eqin  30702  diophin  30706  diophun  30707  0dioph  30712  elnnrabdioph  30740  rabren3dioph  30749  irrapxlem1  30758  irrapxlem3  30760  rmxyadd  30857  rmxy1  30858  rmxy0  30859  rmxp1  30868  rmyp1  30869  rmxm1  30870  rmym1  30871  jm2.24nn  30897  acongeq  30921  jm2.23  30938  jm2.15nn0  30945  jm2.16nn0  30946  jm2.27c  30949  jm2.27dlem2  30952  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  expdioph  30965  mpaaeu  31099  lcmgcdlem  31212  hashnzfzclim  31227  sumsnd  31401  sumsnf  31570  fmuldfeq  31577  prodsnf  31587  stoweidlem3  31785  stoweidlem20  31802  stoweidlem34  31816  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  stirlinglem11  31866  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  fourierdlem47  31936  fourierswlem  32013  1odd  32499  altgsumbcALT  32942  zlmodzxzsubm  32948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-nn 10562  df-z 10890
  Copyright terms: Public domain W3C validator