Theorem 1z 11866

Description: One is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
1z	⊢ 1 ∈ ℤ

Proof of Theorem 1z

Step	Hyp	Ref	Expression
1		1nn 11503	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 11860	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 2083  1c1 10391  ℤcz 11835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-i2m1 10458  ax-1ne0 10459  ax-rrecex 10462  ax-cnre 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-neg 10726  df-nn 11493  df-z 11836

This theorem is referenced by:  1zzd  11867  peano2z  11877  peano2zm  11879  3halfnz  11915  peano5uzti  11926  nnuz  12134  eluz2nn  12137  eluzge3nn  12143  1eluzge0  12145  2eluzge1  12147  eluz2b1  12172  uz2m1nn  12176  nninf  12182  nnrecq  12225  qbtwnxr  12447  fz1n  12779  fz10  12782  fz01en  12789  fznatpl1  12815  fz12pr  12818  fztpval  12823  fseq1p1m1  12835  elfzp1b  12838  elfzm1b  12839  4fvwrd4  12881  ige2m2fzo  12954  fz0add1fz1  12961  fzo12sn  12974  fzo13pr  12975  fzo1to4tp  12979  fzofzp1  12988  fzostep1  13007  flge1nn  13045  fldiv4p1lem1div2  13059  modid0  13119  nnnfi  13188  fzennn  13190  fzen2  13191  f13idfv  13222  ser1const  13280  exp1  13289  zexpcl  13298  qexpcl  13299  qexpclz  13304  m1expcl  13306  expp1z  13332  expm1  13333  facnn  13489  fac0  13490  fac1  13491  bcn1  13527  bcpasc  13535  bcnm1  13541  hashsng  13583  hashfz  13640  fz1isolem  13671  seqcoll  13674  hashge2el2difr  13689  ccat2s1p2  13832  s2f1o  14118  f1oun2prg  14119  swrd2lsw  14154  2swrd2eqwrdeq  14155  relexp1g  14223  climuni  14747  isercoll2  14863  iseraltlem1  14876  sum0  14915  sumsnf  14936  climcndslem1  15041  climcndslem2  15042  divcnvshft  15047  supcvg  15048  prod0  15134  prodsn  15153  prodsnf  15155  zrisefaccl  15211  zfallfaccl  15212  sin01gt0  15380  rpnnen2lem10  15413  nthruc  15442  iddvds  15460  1dvds  15461  dvdsle  15497  dvds1  15506  3dvds  15517  n2dvds1  15554  divalglem5  15585  divalg  15591  bitsfzolem  15620  gcdcllem1  15685  gcdcllem3  15687  gcdaddmlem  15709  gcdadd  15711  gcdid  15712  gcd1  15713  1gcd  15718  bezoutlem1  15720  gcdmultiple  15733  lcmgcdlem  15783  lcm1  15787  3lcm2e6woprm  15792  lcmfunsnlem  15818  isprm3  15860  ge2nprmge4  15878  phicl2  15938  phi1  15943  dfphi2  15944  eulerthlem2  15952  prmdiv  15955  prmdiveq  15956  odzcllem  15962  oddprm  15980  pythagtriplem4  15989  pcpre1  16012  pc1  16025  pcrec  16028  pcmpt  16061  fldivp1  16066  expnprm  16071  pockthlem  16074  unbenlem  16077  prmreclem2  16086  prmrec  16091  igz  16103  4sqlem12  16125  4sqlem13  16126  4sqlem19  16132  vdwlem8  16157  vdwlem13  16162  prmo1  16206  fvprmselgcd1  16214  prmgaplem7  16226  prmlem0  16272  1259lem4  16300  2503lem2  16304  4001lem1  16307  setsstruct  16356  gsumpropd2lem  17716  mulgfval  17987  mulg1  17994  mulgm1  18007  mulgp1  18018  mulgneg2  18019  cycsubgcl  18063  odinv  18422  efgs1b  18593  lt6abl  18740  pgpfac1lem2  18918  srgbinomlem4  18987  qsubdrg  20283  zsubrg  20284  gzsubrg  20285  zringmulg  20311  zringcyg  20324  mulgrhm  20331  mulgrhm2  20332  chrnzr  20363  frgpcyg  20406  zrhpsgnmhm  20414  zrhpsgnodpm  20422  m2detleiblem1  20921  m2detleiblem2  20925  zfbas  22192  imasdsf1olem  22670  cphipval  23533  cmetcaulem  23578  bcthlem5  23618  ehl1eudis  23710  ovolctb  23778  ovolunlem1a  23784  ovolunlem1  23785  ovoliunnul  23795  ovolicc1  23804  ovolicc2lem4  23808  voliunlem1  23838  volsup  23844  uniioombllem6  23876  vitalilem5  23900  plyeq0lem  24487  vieta1lem2  24587  elqaalem2  24596  qaa  24599  iaa  24601  abelthlem6  24711  abelthlem9  24715  sin2pim  24758  cos2pim  24759  logbleb  25046  logblt  25047  1cubrlem  25104  leibpilem2  25205  emcllem5  25263  emcllem7  25265  lgamgulm2  25299  lgamcvglem  25303  gamcvg2lem  25322  lgam1  25327  wilthlem2  25332  wilthlem3  25333  ppip1le  25424  ppi1  25427  cht1  25428  chp1  25430  cht2  25435  ppieq0  25439  ppiub  25466  chpeq0  25470  chpchtsum  25481  chpub  25482  logfacbnd3  25485  logexprlim  25487  bposlem1  25546  bposlem2  25547  bposlem5  25550  bposlem6  25551  lgslem2  25560  lgsfcl2  25565  lgsval2lem  25569  lgsdir2lem1  25587  lgsdir2lem5  25591  1lgs  25602  lgsdchr  25617  lgsquad2lem2  25647  2sqlem9  25689  2sqlem10  25690  2sqblem  25693  2sqb  25694  dchrisumlem3  25753  log2sumbnd  25806  qabvle  25887  ostth3  25900  istrkg3ld  25933  tgldimor  25974  axlowdimlem3  26417  axlowdimlem6  26420  axlowdimlem7  26421  axlowdimlem16  26430  axlowdimlem17  26431  axlowdim  26434  usgrexmpldifpr  26727  uhgrwkspthlem2  27221  pthdlem2  27235  clwwlkccatlem  27453  0ewlk  27579  0pth  27590  1wlkdlem1  27602  ntrl2v2e  27623  eupth2lem3lem4  27696  ex-fl  27914  ipval2  28171  hlim0  28699  opsqrlem2  29605  iuninc  29998  nndiffz1  30193  0dp2dp  30265  cshw1s2  30304  lmatfvlem  30691  mdetpmtr1  30699  mdetpmtr12  30701  lmlim  30803  qqh0  30838  qqh1  30839  esumfzf  30941  esumfsup  30942  esumpcvgval  30950  esumcvg  30958  esumcvgsum  30960  esumsup  30961  dya2ub  31141  rrvsum  31325  dstfrvclim1  31348  ballotlem2  31359  ballotlemfc0  31363  ballotlemfcc  31364  signsvf0  31463  hgt750leme  31542  subfac1  32035  subfacp1lem1  32036  subfacp1lem2a  32037  subfacp1lem5  32041  subfacp1lem6  32042  cvmliftlem10  32151  divcnvlin  32574  faclimlem1  32585  fwddifnp1  33237  poimirlem3  34447  poimirlem4  34448  poimirlem16  34460  poimirlem17  34461  poimirlem19  34463  poimirlem20  34464  poimirlem24  34468  poimirlem27  34471  poimirlem28  34472  poimirlem31  34475  poimirlem32  34476  mblfinlem1  34481  mblfinlem2  34482  ovoliunnfl  34486  voliunnfl  34488  fdc  34573  heibor1lem  34640  rrncmslem  34663  nn0rppwr  38725  nn0expgcd  38727  mapfzcons  38819  mzpexpmpt  38848  eldioph3b  38868  fz1eqin  38872  diophin  38875  diophun  38876  0dioph  38881  elnnrabdioph  38910  rabren3dioph  38918  irrapxlem1  38925  irrapxlem3  38927  rmxyadd  39024  rmxy1  39025  rmxy0  39026  rmxp1  39035  rmyp1  39036  rmxm1  39037  rmym1  39038  jm2.24nn  39062  acongeq  39086  jm2.23  39099  jm2.15nn0  39106  jm2.16nn0  39107  jm2.27c  39110  jm2.27dlem2  39113  rmydioph  39117  rmxdioph  39119  expdiophlem2  39125  expdioph  39126  mpaaeu  39256  trclfvdecomr  39579  k0004val0  40010  hashnzfzclim  40213  sumsnd  40843  fmuldfeq  41427  stoweidlem3  41852  stoweidlem20  41869  stoweidlem34  41883  wallispilem4  41917  wallispi2lem1  41920  wallispi2lem2  41921  stirlinglem11  41933  dirkerper  41945  dirkertrigeqlem1  41947  dirkertrigeqlem3  41949  fourierdlem47  42002  fourierswlem  42079  smfmullem4  42633  1oddALTV  43359  1nevenALTV  43360  2evenALTV  43361  nnsum3primes4  43457  nnsum3primesprm  43459  nnsum3primesgbe  43461  nnsum4primesodd  43465  nnsum4primesoddALTV  43466  nnsum4primeseven  43469  nnsum4primesevenALTV  43470  tgblthelfgott  43484  1odd  43582  altgsumbcALT  43901  zlmodzxzsubm  43907  blen2  44148  blennngt2o2  44155  nn0sumshdiglemA  44182  nn0sumshdiglemB  44183