Theorem 1z 12521

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 12156	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 12515	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 2113  1c1 11027  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-nn 12146  df-z 12489

This theorem is referenced by:  1zzd  12522  peano2z  12532  peano2zm  12534  3halfnz  12571  peano5uzti  12582  nnuz  12790  1eluzge0  12793  2eluzge1  12795  eluz2nn  12801  eluz2b1  12832  uz2m1nn  12836  nninf  12842  nnrecq  12885  qbtwnxr  13115  fz1n  13458  fz10  13461  fz01en  13468  fznatpl1  13494  fz12pr  13497  fztpval  13502  fseq1p1m1  13514  elfzp1b  13517  elfzm1b  13518  4fvwrd4  13564  fzo1lb  13629  ige2m2fzo  13644  fz0add1fz1  13651  fzo12sn  13664  fzo13pr  13665  fzo1to4tp  13670  fzofzp1  13680  fzom1ne1  13701  fzostep1  13702  flge1nn  13741  fldiv4p1lem1div2  13755  modid0  13817  nnnfi  13889  fzennn  13891  fzen2  13892  f13idfv  13923  ser1const  13981  exp1  13990  zexpcl  13999  qexpcl  14000  qexpclz  14004  m1expcl  14009  expp1z  14034  expm1  14035  facnn  14198  fac0  14199  fac1  14200  bcn1  14236  bcpasc  14244  bcnm1  14250  hashsng  14292  hashfz  14350  fz1isolem  14384  seqcoll  14387  hashge2el2difr  14404  ccat2s1p2  14554  s2f1o  14839  f1oun2prg  14840  swrd2lsw  14875  2swrd2eqwrdeq  14876  relexp1g  14949  climuni  15475  isercoll2  15592  iseraltlem1  15605  sum0  15644  sumsnf  15666  climcndslem1  15772  climcndslem2  15773  divcnvshft  15778  supcvg  15779  prod0  15866  prodsn  15885  prodsnf  15887  zrisefaccl  15943  zfallfaccl  15944  sin01gt0  16115  rpnnen2lem10  16148  nthruc  16177  iddvds  16196  1dvds  16197  dvdsle  16237  dvds1  16246  3dvds  16258  n2dvds1  16295  divalglem5  16324  divalg  16330  bitsfzolem  16361  gcdcllem1  16426  gcdcllem3  16428  gcdaddmlem  16451  gcdadd  16453  gcdid  16454  gcd1  16455  1gcd  16460  bezoutlem1  16466  nn0rppwr  16488  nn0expgcd  16491  lcmgcdlem  16533  lcm1  16537  3lcm2e6woprm  16542  lcmfunsnlem  16568  isprm3  16610  ge2nprmge4  16628  phicl2  16695  phi1  16700  dfphi2  16701  eulerthlem2  16709  prmdiv  16712  prmdiveq  16713  odzcllem  16720  oddprm  16738  pythagtriplem4  16747  pcpre1  16770  pc1  16783  pcrec  16786  pcmpt  16820  fldivp1  16825  expnprm  16830  pockthlem  16833  unbenlem  16836  prmreclem2  16845  prmrec  16850  igz  16862  4sqlem12  16884  4sqlem13  16885  4sqlem19  16891  vdwlem8  16916  vdwlem13  16921  prmo1  16965  fvprmselgcd1  16973  prmlem0  17033  1259lem4  17061  2503lem2  17065  4001lem1  17068  setsstruct  17103  chnub  18545  gsumpropd2lem  18604  efmnd1hash  18817  mulgfval  18999  mulg1  19011  mulgm1  19024  mulgp1  19037  mulgneg2  19038  cycsubgcl  19135  odinv  19490  efgs1b  19665  lt6abl  19824  pgpfac1lem2  20006  srgbinomlem4  20164  qsubdrg  21374  zsubrg  21375  gzsubrg  21376  zringmulg  21411  zringcyg  21424  mulgrhm  21432  mulgrhm2  21433  pzriprnglem7  21442  pzriprnglem9  21444  pzriprnglem12  21447  pzriprnglem13  21448  pzriprnglem14  21449  pzriprng1ALT  21451  fermltlchr  21484  chrnzr  21485  frgpcyg  21528  zrhpsgnmhm  21539  zrhpsgnodpm  21547  m2detleiblem1  22568  m2detleiblem2  22572  zfbas  23840  imasdsf1olem  24317  cphipval  25199  cmetcaulem  25244  bcthlem5  25284  ehl1eudis  25376  ovolctb  25447  ovolunlem1a  25453  ovolunlem1  25454  ovoliunnul  25464  ovolicc1  25473  ovolicc2lem4  25477  voliunlem1  25507  volsup  25513  uniioombllem6  25545  vitalilem5  25569  plyeq0lem  26171  vieta1lem2  26275  elqaalem2  26284  qaa  26287  iaa  26289  abelthlem6  26402  abelthlem9  26406  sin2pim  26450  cos2pim  26451  logbleb  26749  logblt  26750  1cubrlem  26807  leibpilem2  26907  emcllem5  26966  emcllem7  26968  lgamgulm2  27002  lgamcvglem  27006  gamcvg2lem  27025  lgam1  27030  wilthlem2  27035  wilthlem3  27036  ppip1le  27127  ppi1  27130  cht1  27131  chp1  27133  cht2  27138  ppieq0  27142  ppiub  27171  chpeq0  27175  chpchtsum  27186  chpub  27187  logfacbnd3  27190  logexprlim  27192  bposlem1  27251  bposlem2  27252  bposlem5  27255  bposlem6  27256  lgslem2  27265  lgsfcl2  27270  lgsval2lem  27274  lgsdir2lem1  27292  lgsdir2lem5  27296  1lgs  27307  lgsdchr  27322  lgsquad2lem2  27352  2sqlem9  27394  2sqlem10  27395  2sqblem  27398  2sqb  27399  dchrisumlem3  27458  log2sumbnd  27511  qabvle  27592  ostth3  27605  istrkg3ld  28533  tgldimor  28574  axlowdimlem3  29017  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  usgrexmpldifpr  29331  dfpth2  29802  uhgrwkspthlem2  29827  pthdlem2  29841  0ewlk  30189  0pth  30200  1wlkdlem1  30212  ntrl2v2e  30233  eupth2lem3lem4  30306  ex-fl  30522  ipval2  30782  hlim0  31310  opsqrlem2  32216  iuninc  32635  nndiffz1  32866  0dp2dp  32990  cshw1s2  33042  cycpmco2lem4  33211  1fldgenq  33404  znfermltl  33447  zringfrac  33635  constrextdg2  33906  cos9thpiminplylem5  33943  lmatfvlem  33972  mdetpmtr1  33980  mdetpmtr12  33982  lmlim  34104  qqh0  34141  qqh1  34142  esumfzf  34226  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  esumcvgsum  34245  esumsup  34246  dya2ub  34427  rrvsum  34611  dstfrvclim1  34635  ballotlem2  34646  ballotlemfc0  34650  ballotlemfcc  34651  signsvf0  34737  hgt750leme  34815  subfac1  35372  subfacp1lem1  35373  subfacp1lem2a  35374  subfacp1lem5  35378  subfacp1lem6  35379  cvmliftlem10  35488  divcnvlin  35927  faclimlem1  35937  fwddifnp1  36359  irrdiff  37527  poimirlem3  37820  poimirlem4  37821  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem24  37841  poimirlem27  37844  poimirlem28  37845  poimirlem31  37848  poimirlem32  37849  mblfinlem1  37854  mblfinlem2  37855  ovoliunnfl  37859  voliunnfl  37861  fdc  37942  heibor1lem  38006  rrncmslem  38029  lcmfunnnd  42262  lcm1un  42263  lcm2un  42264  lcmineqlem11  42289  lcmineqlem19  42297  aks4d1p1p2  42320  mapfzcons  42954  mzpexpmpt  42983  eldioph3b  43003  fz1eqin  43007  diophin  43010  diophun  43011  0dioph  43016  elnnrabdioph  43045  rabren3dioph  43053  irrapxlem1  43060  irrapxlem3  43062  rmxyadd  43159  rmxy1  43160  rmxy0  43161  rmxp1  43170  rmyp1  43171  rmxm1  43172  rmym1  43173  jm2.24nn  43197  acongeq  43221  jm2.23  43234  jm2.15nn0  43241  jm2.16nn0  43242  jm2.27c  43245  jm2.27dlem2  43248  rmydioph  43252  rmxdioph  43254  expdiophlem2  43260  expdioph  43261  mpaaeu  43388  trclfvdecomr  43965  k0004val0  44391  hashnzfzclim  44559  sumsnd  45267  fmuldfeq  45825  stoweidlem3  46243  stoweidlem20  46260  stoweidlem34  46274  wallispilem4  46308  wallispi2lem1  46311  wallispi2lem2  46312  stirlinglem11  46324  dirkerper  46336  dirkertrigeqlem1  46338  dirkertrigeqlem3  46340  fourierdlem47  46393  fourierswlem  46470  smfmullem4  47034  ormklocald  47114  natlocalincr  47116  nthrucw  47126  ceilhalf1  47576  1oddALTV  47932  1nevenALTV  47933  2evenALTV  47934  nnsum3primes4  48030  nnsum3primesprm  48032  nnsum3primesgbe  48034  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  tgblthelfgott  48057  stgr1  48203  gpgusgralem  48298  1odd  48413  altgsumbcALT  48595  zlmodzxzsubm  48601  blen2  48827  blennngt2o2  48834  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862