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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 11286 . 2 1 ∈ ℕ
21nnzi 11647 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  1c1 10189  cz 11623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-z 11624
This theorem is referenced by:  1zzd  11654  peano2z  11664  peano2zm  11666  3halfnz  11702  peano5uzti  11713  nnuz  11922  eluz2nn  11925  eluzge3nn  11929  1eluzge0  11931  2eluzge1  11933  eluz2b1  11959  uz2m1nn  11963  nninf  11969  nnrecq  12011  qbtwnxr  12232  fz1n  12565  fz10  12568  fz01en  12575  fznatpl1  12601  fzprval  12607  fztpval  12608  fseq1p1m1  12620  elfzp1b  12623  elfzm1b  12624  4fvwrd4  12666  ige2m2fzo  12738  fz0add1fz1  12745  fzo12sn  12758  fzo13pr  12759  fzo1to4tp  12763  fzofzp1  12772  fzostep1  12791  flge1nn  12829  fldiv4p1lem1div2  12843  modid0  12903  nnnfi  12972  fzennn  12974  fzen2  12975  f13idfv  13006  ser1const  13063  exp1  13072  zexpcl  13081  qexpcl  13082  qexpclz  13087  m1expcl  13089  expp1z  13115  expm1  13116  facnn  13265  fac0  13266  fac1  13267  bcn1  13303  bcpasc  13311  bcnm1  13317  hashsng  13360  hashfz  13414  fz1isolem  13445  seqcoll  13448  hashge2el2difr  13463  ccat2s1p2  13603  s2f1o  13946  f1oun2prg  13947  swrd2lsw  13982  2swrd2eqwrdeq  13983  2swrd2eqwrdeqOLD  13984  relexp1g  14052  climuni  14569  isercoll2  14685  iseraltlem1  14698  sum0  14738  sumsnf  14759  climcndslem1  14866  climcndslem2  14867  divcnvshft  14872  supcvg  14873  prod0  14957  prodsn  14976  prodsnf  14978  zrisefaccl  15034  zfallfaccl  15035  sin01gt0  15203  rpnnen2lem10  15235  nthruc  15264  iddvds  15281  1dvds  15282  dvdsle  15318  dvds1  15327  3dvds  15338  divalglem5  15403  divalg  15409  bitsfzolem  15438  bitsfzo  15439  gcdcllem1  15503  gcdcllem3  15505  gcdaddmlem  15527  gcdadd  15529  gcdid  15530  gcd1  15531  1gcd  15536  bezoutlem1  15538  gcdmultiple  15551  lcmgcdlem  15601  lcm1  15605  3lcm2e6woprm  15610  lcmfunsnlem  15636  isprm3  15677  prmgt1  15690  phicl2  15753  phi1  15758  dfphi2  15759  eulerthlem2  15767  prmdiv  15770  prmdiveq  15771  odzcllem  15777  oddprm  15795  pythagtriplem4  15804  pcpre1  15827  pc1  15840  pcrec  15843  pcmpt  15876  fldivp1  15881  expnprm  15886  pockthlem  15889  unbenlem  15892  prmreclem2  15901  prmrec  15906  igz  15918  4sqlem12  15940  4sqlem13  15941  4sqlem19  15947  vdwlem8  15972  vdwlem13  15977  prmo1  16021  fvprmselgcd1  16029  prmgaplem7  16041  prmlem0  16087  1259lem4  16115  2503lem2  16119  4001lem1  16122  setsstruct  16172  gsumpropd2lem  17540  mulg1  17816  mulgm1  17829  mulgp1  17840  mulgneg2  17841  cycsubgcl  17885  odinv  18243  efgs1b  18414  lt6abl  18561  pgpfac1lem2  18740  srgbinomlem4  18809  qsubdrg  20070  zsubrg  20071  gzsubrg  20072  zringmulg  20098  zringcyg  20111  mulgrhm  20118  mulgrhm2  20119  chrnzr  20150  frgpcyg  20193  zrhpsgnmhm  20201  zrhpsgnodpm  20209  m2detleiblem1  20706  m2detleiblem2  20710  zfbas  21978  imasdsf1olem  22456  cphipval  23319  cmetcaulem  23364  bcthlem5  23404  ovolctb  23547  ovolunlem1a  23553  ovolunlem1  23554  ovoliunnul  23564  ovolicc1  23573  ovolicc2lem4  23577  voliunlem1  23607  volsup  23613  uniioombllem6  23645  vitalilem5  23669  plyeq0lem  24256  vieta1lem2  24356  elqaalem2  24365  qaa  24368  iaa  24370  abelthlem6  24480  abelthlem9  24484  sin2pim  24528  cos2pim  24529  logbleb  24811  logblt  24812  1cubrlem  24858  leibpilem2  24958  emcllem5  25016  emcllem7  25018  lgamgulm2  25052  lgamcvglem  25056  gamcvg2lem  25075  lgam1  25080  wilthlem2  25085  wilthlem3  25086  ppip1le  25177  ppi1  25180  cht1  25181  chp1  25183  cht2  25188  ppieq0  25192  ppiub  25219  chpeq0  25223  chpchtsum  25234  chpub  25235  logfacbnd3  25238  logexprlim  25240  bposlem1  25299  bposlem2  25300  bposlem5  25303  bposlem6  25304  lgslem2  25313  lgsfcl2  25318  lgsval2lem  25322  lgsdir2lem1  25340  lgsdir2lem5  25344  1lgs  25355  lgsdchr  25370  lgsquad2lem2  25400  2sqlem9  25442  2sqlem10  25443  2sqblem  25446  2sqb  25447  dchrisumlem3  25470  log2sumbnd  25523  qabvle  25604  ostth3  25617  istrkg3ld  25650  tgldimor  25687  axlowdimlem3  26114  axlowdimlem4  26115  axlowdimlem6  26117  axlowdimlem7  26118  axlowdimlem16  26127  axlowdimlem17  26128  axlowdim  26131  usgrexmpldifpr  26428  uhgrwkspthlem2  26940  pthdlem2  26954  clwwlkccatlem  27194  0ewlk  27349  0pth  27360  1wlkdlem1  27372  ntrl2v2e  27393  eupth2lem3lem4  27466  ex-fl  27697  ipval2  27952  hlim0  28482  opsqrlem2  29390  iuninc  29761  nndiffz1  29931  0dp2dp  29998  lmatfvlem  30262  mdetpmtr1  30270  mdetpmtr12  30272  lmlim  30374  qqh0  30409  qqh1  30410  esumfzf  30512  esumfsup  30513  esumpcvgval  30521  esumcvg  30529  esumcvgsum  30531  esumsup  30532  dya2ub  30713  rrvsum  30898  dstfrvclim1  30921  ballotlem2  30932  ballotlemfc0  30936  ballotlemfcc  30937  signsvf0  31039  hgt750leme  31118  subfac1  31539  subfacp1lem1  31540  subfacp1lem2a  31541  subfacp1lem5  31545  subfacp1lem6  31546  cvmliftlem10  31655  divcnvlin  31994  faclimlem1  32005  fwddifnp1  32647  poimirlem3  33768  poimirlem4  33769  poimirlem16  33781  poimirlem17  33782  poimirlem19  33784  poimirlem20  33785  poimirlem24  33789  poimirlem27  33792  poimirlem28  33793  poimirlem31  33796  poimirlem32  33797  mblfinlem1  33802  mblfinlem2  33803  ovoliunnfl  33807  voliunnfl  33809  fdc  33895  heibor1lem  33962  rrncmslem  33985  mapfzcons  37889  mzpexpmpt  37918  eldioph3b  37938  fz1eqin  37942  diophin  37946  diophun  37947  0dioph  37952  elnnrabdioph  37981  rabren3dioph  37989  irrapxlem1  37996  irrapxlem3  37998  rmxyadd  38095  rmxy1  38096  rmxy0  38097  rmxp1  38106  rmyp1  38107  rmxm1  38108  rmym1  38109  jm2.24nn  38135  acongeq  38159  jm2.23  38172  jm2.15nn0  38179  jm2.16nn0  38180  jm2.27c  38183  jm2.27dlem2  38186  rmydioph  38190  rmxdioph  38192  expdiophlem2  38198  expdioph  38199  mpaaeu  38329  trclfvdecomr  38627  k0004val0  39058  hashnzfzclim  39127  sumsnd  39769  fmuldfeq  40385  stoweidlem3  40789  stoweidlem20  40806  stoweidlem34  40820  wallispilem4  40854  wallispi2lem1  40857  wallispi2lem2  40858  stirlinglem11  40870  dirkerper  40882  dirkertrigeqlem1  40884  dirkertrigeqlem3  40886  fourierdlem47  40939  fourierswlem  41016  smfmullem4  41573  1oddALTV  42209  1nevenALTV  42210  2evenALTV  42211  nnsum3primes4  42284  nnsum3primesprm  42286  nnsum3primesgbe  42288  nnsum4primesodd  42292  nnsum4primesoddALTV  42293  nnsum4primeseven  42296  nnsum4primesevenALTV  42297  tgblthelfgott  42311  1odd  42412  altgsumbcALT  42732  zlmodzxzsubm  42738  blen2  42980  blennngt2o2  42987  nn0sumshdiglemA  43014  nn0sumshdiglemB  43015
  Copyright terms: Public domain W3C validator