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

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

Proof of Theorem 1z
StepHypRef Expression
1 1nn 11069 . 2 1 ∈ ℕ
21nnzi 11439 1 1 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  1c1 9975  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-z 11416
This theorem is referenced by:  1zzd  11446  peano2z  11456  peano2zm  11458  3halfnz  11494  peano5uzti  11505  nnuz  11761  eluz2nn  11764  eluzge3nn  11768  1eluzge0  11770  2eluzge1  11772  eluz2b1  11797  uz2m1nn  11801  nninf  11807  nnrecq  11849  qbtwnxr  12069  fz1n  12397  fz10  12400  fz01en  12407  fznatpl1  12433  fzprval  12439  fztpval  12440  fseq1p1m1  12452  elfzp1b  12455  elfzm1b  12456  4fvwrd4  12498  ige2m2fzo  12570  fz0add1fz1  12577  fzo12sn  12591  fzo13pr  12592  fzo1to4tp  12596  fzofzp1  12605  fzostep1  12624  flge1nn  12662  fldiv4p1lem1div2  12676  modid0  12736  nnnfi  12805  fzennn  12807  fzen2  12808  f13idfv  12840  ser1const  12897  exp1  12906  zexpcl  12915  qexpcl  12916  qexpclz  12921  m1expcl  12923  expp1z  12949  expm1  12950  facnn  13102  fac0  13103  fac1  13104  bcn1  13140  bcpasc  13148  bcnm1  13154  hashsng  13197  hashfz  13252  fz1isolem  13283  seqcoll  13286  hashge2el2difr  13301  ccat2s1p2  13450  s2f1o  13707  f1oun2prg  13708  swrd2lsw  13741  2swrd2eqwrdeq  13742  relexp1g  13810  climuni  14327  isercoll2  14443  iseraltlem1  14456  sum0  14496  sumsnf  14517  sumsn  14519  climcndslem1  14625  climcndslem2  14626  divcnvshft  14631  supcvg  14632  prod0  14717  prodsn  14736  prodsnf  14738  zrisefaccl  14795  zfallfaccl  14796  sin01gt0  14964  rpnnen2lem10  14996  nthruc  15025  iddvds  15042  1dvds  15043  dvdsle  15079  dvds1  15088  3dvds  15099  3dvdsOLD  15100  divalglem5  15167  divalg  15173  bitsfzolem  15203  bitsfzo  15204  gcdcllem1  15268  gcdcllem3  15270  gcdaddmlem  15292  gcdadd  15294  gcdid  15295  gcd1  15296  1gcd  15301  bezoutlem1  15303  gcdmultiple  15316  lcmgcdlem  15366  lcm1  15370  3lcm2e6woprm  15375  lcmfunsnlem  15401  isprm3  15443  prmgt1  15456  phicl2  15520  phi1  15525  dfphi2  15526  eulerthlem2  15534  prmdiv  15537  prmdiveq  15538  odzcllem  15544  oddprm  15562  pythagtriplem4  15571  pcpre1  15594  pc1  15607  pcrec  15610  pcmpt  15643  fldivp1  15648  expnprm  15653  pockthlem  15656  unbenlem  15659  prmreclem2  15668  prmrec  15673  igz  15685  4sqlem12  15707  4sqlem13  15708  4sqlem19  15714  vdwlem8  15739  vdwlem13  15744  prmo1  15788  fvprmselgcd1  15796  prmgaplem7  15808  prmlem0  15859  1259lem4  15888  2503lem2  15892  4001lem1  15895  setsstruct  15945  gsumpropd2lem  17320  mulg1  17595  mulgm1  17609  mulgp1  17621  mulgneg2  17622  cycsubgcl  17667  odinv  18024  efgs1b  18195  lt6abl  18342  pgpfac1lem2  18520  srgbinomlem4  18589  qsubdrg  19846  zsubrg  19847  gzsubrg  19848  zringmulg  19874  zringcyg  19887  mulgrhm  19894  mulgrhm2  19895  chrnzr  19926  frgpcyg  19970  zrhpsgnmhm  19978  zrhpsgnodpm  19986  m2detleiblem1  20478  m2detleiblem2  20482  zfbas  21747  imasdsf1olem  22225  cphipval  23088  cmetcaulem  23132  bcthlem5  23171  ovolctb  23304  ovolunlem1a  23310  ovolunlem1  23311  ovoliunnul  23321  ovolicc1  23330  ovolicc2lem4  23334  voliunlem1  23364  volsup  23370  uniioombllem6  23402  vitalilem5  23426  plyeq0lem  24011  vieta1lem2  24111  elqaalem2  24120  qaa  24123  iaa  24125  abelthlem6  24235  abelthlem9  24239  sin2pim  24282  cos2pim  24283  logbleb  24566  logblt  24567  1cubrlem  24613  leibpilem2  24713  emcllem5  24771  emcllem7  24773  lgamgulm2  24807  lgamcvglem  24811  gamcvg2lem  24830  lgam1  24835  wilthlem2  24840  wilthlem3  24841  ppip1le  24932  ppi1  24935  cht1  24936  chp1  24938  cht2  24943  ppieq0  24947  ppiub  24974  chpeq0  24978  chpchtsum  24989  chpub  24990  logfacbnd3  24993  logexprlim  24995  bposlem1  25054  bposlem2  25055  bposlem5  25058  bposlem6  25059  lgslem2  25068  lgsfcl2  25073  lgsval2lem  25077  lgsdir2lem1  25095  lgsdir2lem5  25099  1lgs  25110  lgsdchr  25125  lgsquad2lem2  25155  2sqlem9  25197  2sqlem10  25198  2sqblem  25201  2sqb  25202  dchrisumlem3  25225  log2sumbnd  25278  qabvle  25359  ostth3  25372  istrkg3ld  25405  tgldimor  25442  axlowdimlem3  25869  axlowdimlem4  25870  axlowdimlem6  25872  axlowdimlem7  25873  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  usgrexmpldifpr  26195  uhgrwkspthlem2  26706  pthdlem2  26720  0ewlk  27092  0pth  27103  1wlkdlem1  27115  ntrl2v2e  27136  eupth2lem3lem4  27209  clwwlkccatlem  27331  ex-fl  27434  ipval2  27690  hlim0  28220  opsqrlem2  29128  iuninc  29505  nndiffz1  29676  0dp2dp  29745  lmatfvlem  30009  mdetpmtr1  30017  mdetpmtr12  30019  lmlim  30121  qqh0  30156  qqh1  30157  esumfzf  30259  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  esumcvgsum  30278  esumsup  30279  dya2ub  30460  rrvsum  30644  dstfrvclim1  30667  ballotlem2  30678  ballotlemfc0  30682  ballotlemfcc  30683  signsvf0  30785  hgt750leme  30864  subfac1  31286  subfacp1lem1  31287  subfacp1lem2a  31288  subfacp1lem5  31292  subfacp1lem6  31293  cvmliftlem10  31402  divcnvlin  31744  faclimlem1  31755  fwddifnp1  32397  poimirlem3  33542  poimirlem4  33543  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  mblfinlem1  33576  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  fdc  33671  heibor1lem  33738  rrncmslem  33761  mapfzcons  37596  mzpexpmpt  37625  eldioph3b  37645  fz1eqin  37649  diophin  37653  diophun  37654  0dioph  37659  elnnrabdioph  37688  rabren3dioph  37696  irrapxlem1  37703  irrapxlem3  37705  rmxyadd  37803  rmxy1  37804  rmxy0  37805  rmxp1  37814  rmyp1  37815  rmxm1  37816  rmym1  37817  jm2.24nn  37843  acongeq  37867  jm2.23  37880  jm2.15nn0  37887  jm2.16nn0  37888  jm2.27c  37891  jm2.27dlem2  37894  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  expdioph  37907  mpaaeu  38037  trclfvdecomr  38337  k0004val0  38769  hashnzfzclim  38838  sumsnd  39499  fmuldfeq  40133  stoweidlem3  40538  stoweidlem20  40555  stoweidlem34  40569  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem11  40619  dirkerper  40631  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  fourierdlem47  40688  fourierswlem  40765  smfmullem4  41322  1oddALTV  41926  1nevenALTV  41927  2evenALTV  41928  nnsum3primes4  42001  nnsum3primesprm  42003  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  tgblthelfgott  42028  tgblthelfgottOLD  42034  1odd  42136  altgsumbcALT  42456  zlmodzxzsubm  42462  blen2  42704  blennngt2o2  42711  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator