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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 10878 . 2 1 ∈ ℕ
21nnzi 11234 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  1c1 9793  cz 11210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-z 11211
This theorem is referenced by:  1zzd  11241  peano2z  11251  peano2zm  11253  3halfnz  11288  peano5uzti  11299  nnuz  11555  eluz2nn  11558  eluzge3nn  11562  1eluzge0  11564  2eluzge1  11566  eluz2b1  11591  uz2m1nn  11595  nninf  11601  nnrecq  11643  qbtwnxr  11864  fz1n  12185  fz10  12188  fz01en  12195  fznatpl1  12220  fzprval  12226  fztpval  12227  fseq1p1m1  12238  elfzp1b  12241  elfzm1b  12242  4fvwrd4  12283  ige2m2fzo  12353  fzo12sn  12373  fzo13pr  12374  fzo1to4tp  12378  fzofzp1  12386  fzostep1  12401  flge1nn  12439  fldiv4p1lem1div2  12453  modid0  12513  nnnfi  12582  fzennn  12584  fzen2  12585  f13idfv  12617  ser1const  12674  exp1  12683  zexpcl  12692  qexpcl  12693  qexpclz  12698  m1expcl  12700  expp1z  12726  expm1  12727  facnn  12879  fac0  12880  fac1  12881  bcn1  12917  bcpasc  12925  bcnm1  12931  hashsng  12972  hashfz  13026  fz1isolem  13054  seqcoll  13057  hashge2el2difr  13068  ccat2s1p2  13204  s2f1o  13457  f1oun2prg  13458  swrd2lsw  13489  2swrd2eqwrdeq  13490  relexp1g  13560  climuni  14077  isercoll2  14193  iseraltlem1  14206  sum0  14245  sumsn  14265  climcndslem1  14366  climcndslem2  14367  divcnvshft  14372  supcvg  14373  prod0  14458  prodsn  14477  prodsnf  14479  zrisefaccl  14536  zfallfaccl  14537  sin01gt0  14705  rpnnen2lem10  14737  nthruc  14765  iddvds  14779  1dvds  14780  dvdsle  14816  dvds1  14825  3dvds  14836  3dvdsOLD  14837  divalglem5  14904  divalg  14910  bitsfzolem  14940  bitsfzo  14941  gcdcllem1  15005  gcdcllem3  15007  gcdaddmlem  15029  gcdadd  15031  gcdid  15032  gcd1  15033  1gcd  15038  bezoutlem1  15040  gcdmultiple  15053  lcmgcdlem  15103  lcm1  15107  3lcm2e6woprm  15112  lcmfunsnlem  15138  isprm3  15180  prmgt1  15193  phicl2  15257  phi1  15262  dfphi2  15263  eulerthlem2  15271  prmdiv  15274  prmdiveq  15275  odzcllem  15281  oddprm  15299  pythagtriplem4  15308  pcpre1  15331  pc1  15344  pcrec  15347  pcmpt  15380  fldivp1  15385  expnprm  15390  pockthlem  15393  unbenlem  15396  prmreclem2  15405  prmrec  15410  igz  15422  4sqlem12  15444  4sqlem13  15445  4sqlem19  15451  vdwlem8  15476  vdwlem13  15481  prmo1  15525  fvprmselgcd1  15533  prmgaplem7  15545  prmlem0  15596  1259lem4  15625  2503lem2  15629  4001lem1  15632  gsumpropd2lem  17042  mulg1  17317  mulgm1  17331  mulgp1  17343  mulgneg2  17344  cycsubgcl  17389  odinv  17747  efgs1b  17918  lt6abl  18065  pgpfac1lem2  18243  srgbinomlem4  18312  qsubdrg  19563  zsubrg  19564  gzsubrg  19565  zringmulg  19591  zringcyg  19601  mulgrhm  19610  mulgrhm2  19611  chrnzr  19642  frgpcyg  19686  zrhpsgnmhm  19694  zrhpsgnodpm  19702  m2detleiblem1  20191  m2detleiblem2  20195  zfbas  21452  imasdsf1olem  21929  cmetcaulem  22812  bcthlem5  22850  ovolctb  22982  ovolunlem1a  22988  ovolunlem1  22989  ovoliunnul  22999  ovolicc1  23008  ovolicc2lem4  23012  voliunlem1  23042  volsup  23048  uniioombllem6  23079  vitalilem5  23104  plyeq0lem  23687  vieta1lem2  23787  elqaalem2  23796  qaa  23799  iaa  23801  abelthlem6  23911  abelthlem9  23915  sin2pim  23958  cos2pim  23959  logbleb  24238  logblt  24239  1cubrlem  24285  leibpilem2  24385  emcllem5  24443  emcllem7  24445  lgamgulm2  24479  lgamcvglem  24483  gamcvg2lem  24502  lgam1  24507  wilthlem2  24512  wilthlem3  24513  ppip1le  24604  ppi1  24607  cht1  24608  chp1  24610  cht2  24615  ppieq0  24619  ppiub  24646  chpeq0  24650  chpchtsum  24661  chpub  24662  logfacbnd3  24665  logexprlim  24667  bposlem1  24726  bposlem2  24727  bposlem5  24730  bposlem6  24731  lgslem2  24740  lgsfcl2  24745  lgsval2lem  24749  lgsdir2lem1  24767  lgsdir2lem5  24771  1lgs  24782  lgsdchr  24797  lgsquad2lem2  24827  2sqlem9  24869  2sqlem10  24870  2sqblem  24873  2sqb  24874  dchrisumlem3  24897  log2sumbnd  24950  qabvle  25031  ostth3  25044  istrkg3ld  25077  tgldimor  25114  axlowdimlem3  25542  axlowdimlem4  25543  axlowdimlem6  25545  axlowdimlem7  25546  axlowdimlem16  25555  axlowdimlem17  25556  axlowdim  25559  usgraexmpldifpr  25694  2trllemD  25853  2trllemG  25854  0pth  25866  constr1trl  25884  constr2spthlem1  25890  fargshiftlem  25928  usgrcyclnl1  25934  3v3e3cycl1  25938  constr3lem4  25941  constr3trllem3  25946  constr3trllem5  25948  constr3pthlem1  25949  constr3pthlem2  25950  constr3pthlem3  25951  eupap1  26269  eupath2lem3  26272  ex-fl  26462  ipval2  26747  hlim0  27282  opsqrlem2  28190  iuninc  28567  nndiffz1  28742  lmatfvlem  29015  mdetpmtr1  29023  mdetpmtr12  29025  lmlim  29127  qqh0  29162  qqh1  29163  esumfzf  29264  esumfsup  29265  esumpcvgval  29273  esumcvg  29281  esumcvgsum  29283  esumsup  29284  dya2ub  29465  rrvsum  29649  dstfrvclim1  29672  ballotlem2  29683  ballotlemfc0  29687  ballotlemfcc  29688  signsvf0  29789  subfac1  30220  subfacp1lem1  30221  subfacp1lem2a  30222  subfacp1lem5  30226  subfacp1lem6  30227  cvmliftlem10  30336  divcnvlin  30677  faclimlem1  30688  fwddifnp1  31248  poimirlem3  32378  poimirlem4  32379  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem24  32399  poimirlem27  32402  poimirlem28  32403  poimirlem31  32406  poimirlem32  32407  mblfinlem1  32412  mblfinlem2  32413  ovoliunnfl  32417  voliunnfl  32419  fdc  32507  heibor1lem  32574  rrncmslem  32597  mapfzcons  36093  mzpexpmpt  36122  eldioph3b  36142  fz1eqin  36146  diophin  36150  diophun  36151  0dioph  36156  elnnrabdioph  36185  rabren3dioph  36193  irrapxlem1  36200  irrapxlem3  36202  rmxyadd  36300  rmxy1  36301  rmxy0  36302  rmxp1  36311  rmyp1  36312  rmxm1  36313  rmym1  36314  jm2.24nn  36340  acongeq  36364  jm2.23  36377  jm2.15nn0  36384  jm2.16nn0  36385  jm2.27c  36388  jm2.27dlem2  36391  rmydioph  36395  rmxdioph  36397  expdiophlem2  36403  expdioph  36404  mpaaeu  36535  trclfvdecomr  36835  k0004val0  37268  hashnzfzclim  37339  sumsnd  38004  sumsnf  38433  fmuldfeq  38447  stoweidlem3  38693  stoweidlem20  38710  stoweidlem34  38724  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem11  38774  dirkerper  38786  dirkertrigeqlem1  38788  dirkertrigeqlem3  38790  fourierdlem47  38843  fourierswlem  38920  smfmullem4  39476  1oddALTV  39937  1nevenALTV  39938  2evenALTV  39939  nnsum3primes4  40002  nnsum3primesprm  40004  nnsum3primesgbe  40006  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  tgblthelfgott  40027  tgblthelfgottOLD  40034  uhgr1wlkspthlem2  40955  pthdlem2  40969  wwlksnextproplem1  41110  0ewlk  41277  0pth-av  41288  11wlkdlem1  41299  ntrl2v2e  41320  eupth2lem3lem4  41394  1odd  41596  altgsumbcALT  41919  zlmodzxzsubm  41925  blen2  42172  blennngt2o2  42179  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator