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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 10908 . 2 1 ∈ ℕ
21nnzi 11278 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  1c1 9816  cz 11254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-z 11255
This theorem is referenced by:  1zzd  11285  peano2z  11295  peano2zm  11297  3halfnz  11332  peano5uzti  11343  nnuz  11599  eluz2nn  11602  eluzge3nn  11606  1eluzge0  11608  2eluzge1  11610  eluz2b1  11635  uz2m1nn  11639  nninf  11645  nnrecq  11687  qbtwnxr  11905  fz1n  12230  fz10  12233  fz01en  12240  fznatpl1  12265  fzprval  12271  fztpval  12272  fseq1p1m1  12283  elfzp1b  12286  elfzm1b  12287  4fvwrd4  12328  ige2m2fzo  12398  fzo12sn  12418  fzo13pr  12419  fzo1to4tp  12423  fzofzp1  12431  fzostep1  12446  flge1nn  12484  fldiv4p1lem1div2  12498  modid0  12558  nnnfi  12627  fzennn  12629  fzen2  12630  f13idfv  12662  ser1const  12719  exp1  12728  zexpcl  12737  qexpcl  12738  qexpclz  12743  m1expcl  12745  expp1z  12771  expm1  12772  facnn  12924  fac0  12925  fac1  12926  bcn1  12962  bcpasc  12970  bcnm1  12976  hashsng  13020  hashfz  13074  fz1isolem  13102  seqcoll  13105  hashge2el2difr  13118  ccat2s1p2  13258  s2f1o  13511  f1oun2prg  13512  swrd2lsw  13543  2swrd2eqwrdeq  13544  relexp1g  13614  climuni  14131  isercoll2  14247  iseraltlem1  14260  sum0  14299  sumsn  14319  climcndslem1  14420  climcndslem2  14421  divcnvshft  14426  supcvg  14427  prod0  14512  prodsn  14531  prodsnf  14533  zrisefaccl  14590  zfallfaccl  14591  sin01gt0  14759  rpnnen2lem10  14791  nthruc  14819  iddvds  14833  1dvds  14834  dvdsle  14870  dvds1  14879  3dvds  14890  3dvdsOLD  14891  divalglem5  14958  divalg  14964  bitsfzolem  14994  bitsfzo  14995  gcdcllem1  15059  gcdcllem3  15061  gcdaddmlem  15083  gcdadd  15085  gcdid  15086  gcd1  15087  1gcd  15092  bezoutlem1  15094  gcdmultiple  15107  lcmgcdlem  15157  lcm1  15161  3lcm2e6woprm  15166  lcmfunsnlem  15192  isprm3  15234  prmgt1  15247  phicl2  15311  phi1  15316  dfphi2  15317  eulerthlem2  15325  prmdiv  15328  prmdiveq  15329  odzcllem  15335  oddprm  15353  pythagtriplem4  15362  pcpre1  15385  pc1  15398  pcrec  15401  pcmpt  15434  fldivp1  15439  expnprm  15444  pockthlem  15447  unbenlem  15450  prmreclem2  15459  prmrec  15464  igz  15476  4sqlem12  15498  4sqlem13  15499  4sqlem19  15505  vdwlem8  15530  vdwlem13  15535  prmo1  15579  fvprmselgcd1  15587  prmgaplem7  15599  prmlem0  15650  1259lem4  15679  2503lem2  15683  4001lem1  15686  gsumpropd2lem  17096  mulg1  17371  mulgm1  17385  mulgp1  17397  mulgneg2  17398  cycsubgcl  17443  odinv  17801  efgs1b  17972  lt6abl  18119  pgpfac1lem2  18297  srgbinomlem4  18366  qsubdrg  19617  zsubrg  19618  gzsubrg  19619  zringmulg  19645  zringcyg  19658  mulgrhm  19665  mulgrhm2  19666  chrnzr  19697  frgpcyg  19741  zrhpsgnmhm  19749  zrhpsgnodpm  19757  m2detleiblem1  20249  m2detleiblem2  20253  zfbas  21510  imasdsf1olem  21988  cphipval  22850  cmetcaulem  22894  bcthlem5  22933  ovolctb  23065  ovolunlem1a  23071  ovolunlem1  23072  ovoliunnul  23082  ovolicc1  23091  ovolicc2lem4  23095  voliunlem1  23125  volsup  23131  uniioombllem6  23162  vitalilem5  23187  plyeq0lem  23770  vieta1lem2  23870  elqaalem2  23879  qaa  23882  iaa  23884  abelthlem6  23994  abelthlem9  23998  sin2pim  24041  cos2pim  24042  logbleb  24321  logblt  24322  1cubrlem  24368  leibpilem2  24468  emcllem5  24526  emcllem7  24528  lgamgulm2  24562  lgamcvglem  24566  gamcvg2lem  24585  lgam1  24590  wilthlem2  24595  wilthlem3  24596  ppip1le  24687  ppi1  24690  cht1  24691  chp1  24693  cht2  24698  ppieq0  24702  ppiub  24729  chpeq0  24733  chpchtsum  24744  chpub  24745  logfacbnd3  24748  logexprlim  24750  bposlem1  24809  bposlem2  24810  bposlem5  24813  bposlem6  24814  lgslem2  24823  lgsfcl2  24828  lgsval2lem  24832  lgsdir2lem1  24850  lgsdir2lem5  24854  1lgs  24865  lgsdchr  24880  lgsquad2lem2  24910  2sqlem9  24952  2sqlem10  24953  2sqblem  24956  2sqb  24957  dchrisumlem3  24980  log2sumbnd  25033  qabvle  25114  ostth3  25127  istrkg3ld  25160  tgldimor  25197  axlowdimlem3  25624  axlowdimlem4  25625  axlowdimlem6  25627  axlowdimlem7  25628  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  usgraexmpldifpr  25928  2trllemD  26087  2trllemG  26088  0pth  26100  constr1trl  26118  constr2spthlem1  26124  fargshiftlem  26162  usgrcyclnl1  26168  3v3e3cycl1  26172  constr3lem4  26175  constr3trllem3  26180  constr3trllem5  26182  constr3pthlem1  26183  constr3pthlem2  26184  constr3pthlem3  26185  eupap1  26503  eupath2lem3  26506  ex-fl  26696  ipval2  26946  hlim0  27476  opsqrlem2  28384  iuninc  28761  nndiffz1  28936  lmatfvlem  29209  mdetpmtr1  29217  mdetpmtr12  29219  lmlim  29321  qqh0  29356  qqh1  29357  esumfzf  29458  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  esumcvgsum  29477  esumsup  29478  dya2ub  29659  rrvsum  29843  dstfrvclim1  29866  ballotlem2  29877  ballotlemfc0  29881  ballotlemfcc  29882  signsvf0  29983  subfac1  30414  subfacp1lem1  30415  subfacp1lem2a  30416  subfacp1lem5  30420  subfacp1lem6  30421  cvmliftlem10  30530  divcnvlin  30871  faclimlem1  30882  fwddifnp1  31442  poimirlem3  32582  poimirlem4  32583  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  mblfinlem1  32616  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  fdc  32711  heibor1lem  32778  rrncmslem  32801  mapfzcons  36297  mzpexpmpt  36326  eldioph3b  36346  fz1eqin  36350  diophin  36354  diophun  36355  0dioph  36360  elnnrabdioph  36389  rabren3dioph  36397  irrapxlem1  36404  irrapxlem3  36406  rmxyadd  36504  rmxy1  36505  rmxy0  36506  rmxp1  36515  rmyp1  36516  rmxm1  36517  rmym1  36518  jm2.24nn  36544  acongeq  36568  jm2.23  36581  jm2.15nn0  36588  jm2.16nn0  36589  jm2.27c  36592  jm2.27dlem2  36595  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  mpaaeu  36739  trclfvdecomr  37039  k0004val0  37472  hashnzfzclim  37543  sumsnd  38208  sumsnf  38636  fmuldfeq  38650  stoweidlem3  38896  stoweidlem20  38913  stoweidlem34  38927  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem11  38977  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  fourierdlem47  39046  fourierswlem  39123  smfmullem4  39679  1oddALTV  40139  1nevenALTV  40140  2evenALTV  40141  nnsum3primes4  40204  nnsum3primesprm  40206  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  tgblthelfgott  40229  tgblthelfgottOLD  40236  uhgr1wlkspthlem2  40960  pthdlem2  40974  wwlksnextproplem1  41115  0ewlk  41282  0pth-av  41293  11wlkdlem1  41304  ntrl2v2e  41325  eupth2lem3lem4  41399  1odd  41601  altgsumbcALT  41924  zlmodzxzsubm  41930  blen2  42177  blennngt2o2  42184  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator