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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 11637 . 2 1 ∈ ℕ
21nnzi 11994 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10526  cz 11969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-i2m1 10593  ax-1ne0 10594  ax-rrecex 10597  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-neg 10861  df-nn 11627  df-z 11970
This theorem is referenced by:  1zzd  12001  peano2z  12011  peano2zm  12013  3halfnz  12049  peano5uzti  12060  nnuz  12269  eluz2nn  12272  eluzge3nn  12278  1eluzge0  12280  2eluzge1  12282  eluz2b1  12307  uz2m1nn  12311  nninf  12317  nnrecq  12359  qbtwnxr  12581  fz1n  12913  fz10  12916  fz01en  12923  fznatpl1  12949  fz12pr  12952  fztpval  12957  fseq1p1m1  12969  elfzp1b  12972  elfzm1b  12973  4fvwrd4  13015  ige2m2fzo  13088  fz0add1fz1  13095  fzo12sn  13108  fzo13pr  13109  fzo1to4tp  13113  fzofzp1  13122  fzostep1  13141  flge1nn  13179  fldiv4p1lem1div2  13193  modid0  13253  nnnfi  13322  fzennn  13324  fzen2  13325  f13idfv  13356  ser1const  13414  exp1  13423  zexpcl  13432  qexpcl  13433  qexpclz  13438  m1expcl  13440  expp1z  13466  expm1  13467  facnn  13623  fac0  13624  fac1  13625  bcn1  13661  bcpasc  13669  bcnm1  13675  hashsng  13718  hashfz  13776  fz1isolem  13807  seqcoll  13810  hashge2el2difr  13827  ccat2s1p2  13974  ccat2s1p2OLD  13976  s2f1o  14266  f1oun2prg  14267  swrd2lsw  14302  2swrd2eqwrdeq  14303  relexp1g  14373  climuni  14897  isercoll2  15013  iseraltlem1  15026  sum0  15066  sumsnf  15087  climcndslem1  15192  climcndslem2  15193  divcnvshft  15198  supcvg  15199  prod0  15285  prodsn  15304  prodsnf  15306  zrisefaccl  15362  zfallfaccl  15363  sin01gt0  15531  rpnnen2lem10  15564  nthruc  15593  iddvds  15611  1dvds  15612  dvdsle  15648  dvds1  15657  3dvds  15668  n2dvds1  15705  divalglem5  15736  divalg  15742  bitsfzolem  15771  gcdcllem1  15836  gcdcllem3  15838  gcdaddmlem  15860  gcdadd  15862  gcdid  15863  gcd1  15864  1gcd  15869  bezoutlem1  15875  gcdmultipleOLD  15888  lcmgcdlem  15938  lcm1  15942  3lcm2e6woprm  15947  lcmfunsnlem  15973  isprm3  16015  ge2nprmge4  16033  phicl2  16093  phi1  16098  dfphi2  16099  eulerthlem2  16107  prmdiv  16110  prmdiveq  16111  odzcllem  16117  oddprm  16135  pythagtriplem4  16144  pcpre1  16167  pc1  16180  pcrec  16183  pcmpt  16216  fldivp1  16221  expnprm  16226  pockthlem  16229  unbenlem  16232  prmreclem2  16241  prmrec  16246  igz  16258  4sqlem12  16280  4sqlem13  16281  4sqlem19  16287  vdwlem8  16312  vdwlem13  16317  prmo1  16361  fvprmselgcd1  16369  prmgaplem7  16381  prmlem0  16427  1259lem4  16455  2503lem2  16459  4001lem1  16462  setsstruct  16511  gsumpropd2lem  17877  mulgfval  18164  mulg1  18173  mulgm1  18186  mulgp1  18198  mulgneg2  18199  cycsubgcl  18287  odinv  18617  efgs1b  18791  lt6abl  18944  pgpfac1lem2  19126  srgbinomlem4  19222  qsubdrg  20525  zsubrg  20526  gzsubrg  20527  zringmulg  20553  zringcyg  20566  mulgrhm  20573  mulgrhm2  20574  chrnzr  20605  frgpcyg  20648  zrhpsgnmhm  20656  zrhpsgnodpm  20664  m2detleiblem1  21161  m2detleiblem2  21165  zfbas  22432  imasdsf1olem  22910  cphipval  23773  cmetcaulem  23818  bcthlem5  23858  ehl1eudis  23950  ovolctb  24018  ovolunlem1a  24024  ovolunlem1  24025  ovoliunnul  24035  ovolicc1  24044  ovolicc2lem4  24048  voliunlem1  24078  volsup  24084  uniioombllem6  24116  vitalilem5  24140  plyeq0lem  24727  vieta1lem2  24827  elqaalem2  24836  qaa  24839  iaa  24841  abelthlem6  24951  abelthlem9  24955  sin2pim  24998  cos2pim  24999  logbleb  25288  logblt  25289  1cubrlem  25346  leibpilem2  25446  emcllem5  25504  emcllem7  25506  lgamgulm2  25540  lgamcvglem  25544  gamcvg2lem  25563  lgam1  25568  wilthlem2  25573  wilthlem3  25574  ppip1le  25665  ppi1  25668  cht1  25669  chp1  25671  cht2  25676  ppieq0  25680  ppiub  25707  chpeq0  25711  chpchtsum  25722  chpub  25723  logfacbnd3  25726  logexprlim  25728  bposlem1  25787  bposlem2  25788  bposlem5  25791  bposlem6  25792  lgslem2  25801  lgsfcl2  25806  lgsval2lem  25810  lgsdir2lem1  25828  lgsdir2lem5  25832  1lgs  25843  lgsdchr  25858  lgsquad2lem2  25888  2sqlem9  25930  2sqlem10  25931  2sqblem  25934  2sqb  25935  dchrisumlem3  25994  log2sumbnd  26047  qabvle  26128  ostth3  26141  istrkg3ld  26174  tgldimor  26215  axlowdimlem3  26657  axlowdimlem6  26660  axlowdimlem7  26661  axlowdimlem16  26670  axlowdimlem17  26671  axlowdim  26674  usgrexmpldifpr  26967  uhgrwkspthlem2  27462  pthdlem2  27476  0ewlk  27820  0pth  27831  1wlkdlem1  27843  ntrl2v2e  27864  eupth2lem3lem4  27937  ex-fl  28153  ipval2  28411  hlim0  28939  opsqrlem2  29845  iuninc  30240  nndiffz1  30435  fzom1ne1  30450  0dp2dp  30512  cshw1s2  30561  cycpmco2lem4  30698  lmatfvlem  30979  mdetpmtr1  30987  mdetpmtr12  30989  lmlim  31089  qqh0  31124  qqh1  31125  esumfzf  31227  esumfsup  31228  esumpcvgval  31236  esumcvg  31244  esumcvgsum  31246  esumsup  31247  dya2ub  31427  rrvsum  31611  dstfrvclim1  31634  ballotlem2  31645  ballotlemfc0  31649  ballotlemfcc  31650  signsvf0  31749  hgt750leme  31828  subfac1  32322  subfacp1lem1  32323  subfacp1lem2a  32324  subfacp1lem5  32328  subfacp1lem6  32329  cvmliftlem10  32438  divcnvlin  32861  faclimlem1  32872  fwddifnp1  33523  poimirlem3  34776  poimirlem4  34777  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem24  34797  poimirlem27  34800  poimirlem28  34801  poimirlem31  34804  poimirlem32  34805  mblfinlem1  34810  mblfinlem2  34811  ovoliunnfl  34815  voliunnfl  34817  fdc  34901  heibor1lem  34968  rrncmslem  34991  nn0rppwr  39060  nn0expgcd  39062  mapfzcons  39191  mzpexpmpt  39220  eldioph3b  39240  fz1eqin  39244  diophin  39247  diophun  39248  0dioph  39253  elnnrabdioph  39282  rabren3dioph  39290  irrapxlem1  39297  irrapxlem3  39299  rmxyadd  39396  rmxy1  39397  rmxy0  39398  rmxp1  39407  rmyp1  39408  rmxm1  39409  rmym1  39410  jm2.24nn  39434  acongeq  39458  jm2.23  39471  jm2.15nn0  39478  jm2.16nn0  39479  jm2.27c  39482  jm2.27dlem2  39485  rmydioph  39489  rmxdioph  39491  expdiophlem2  39497  expdioph  39498  mpaaeu  39628  trclfvdecomr  39951  k0004val0  40382  hashnzfzclim  40531  sumsnd  41160  fmuldfeq  41740  stoweidlem3  42165  stoweidlem20  42182  stoweidlem34  42196  wallispilem4  42230  wallispi2lem1  42233  wallispi2lem2  42234  stirlinglem11  42246  dirkerper  42258  dirkertrigeqlem1  42260  dirkertrigeqlem3  42262  fourierdlem47  42315  fourierswlem  42392  smfmullem4  42946  1oddALTV  43732  1nevenALTV  43733  2evenALTV  43734  nnsum3primes4  43830  nnsum3primesprm  43832  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  tgblthelfgott  43857  1odd  43955  efmnd1hash  43989  altgsumbcALT  44329  zlmodzxzsubm  44335  blen2  44573  blennngt2o2  44580  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator