Theorem 1z 9679

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

Assertion

Ref	Expression
1z	|- 1 e. ZZ

Proof of Theorem 1z

Step	Hyp	Ref	Expression
1		1nn 9324	. 2 |- 1 e. NN
2	1	nnzi 9674	1 |- 1 e. ZZ

This proof depends on syntax axioms:   e. wcel 2209   1c1 8186   ZZcz 9653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-ltadd 8301

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-inn 9314  df-z 9654

This theorem is used by:  1zzd  9680  znnnlt1  9701  nn0n0n1ge2b  9734  nn0lt2  9736  nn0le2is012  9737  3halfnz  9753  prime  9755  nnuz  9973  eluz2nn  9981  eluzge3nn  9987  1eluzge0  9989  2eluzge1  9991  eluz2b1  10016  uz2m1nn  10020  elnn1uz2  10022  elnndc  10027  nn01to3  10032  nnrecq  10060  fz1n  10464  fz10  10466  fz01en  10475  fzpreddisj  10494  fznatpl1  10499  fzprval  10505  fztpval  10506  fseq1p1m1  10517  elfzp1b  10520  elfzm1b  10521  4fvwrd4  10563  ige2m2fzo  10632  fzo12sn  10651  fzofzp1  10661  fzostep1  10672  rebtwn2zlemstep  10703  qbtwnxr  10708  flqge1nn  10749  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  modqfrac  10794  modqid0  10807  q1mod  10813  mulp1mod1  10822  m1modnnsub1  10827  modqm1p1mod0  10832  modqltm1p1mod  10833  frecfzennn  10883  frecfzen2  10884  zexpcl  11011  qexpcl  11012  qexpclz  11017  m1expcl  11019  expp1zap  11045  expm1ap  11046  bcn1  11217  bcpasc  11225  bcnm1  11232  isfinite4im  11252  hashsng  11258  hashfz  11283  ssenneg  11301  fiidxsupcl  12017  climuni  12083  sum0  12179  sumsnf  12200  expcnv  12295  cvgratz  12323  prod0  12376  prodsnf  12383  sinltxirr  12552  sin01gt0  12553  p1modz1  12585  iddvds  12595  1dvds  12596  dvds1  12644  3dvds  12655  nn0o1gt2  12696  n2dvds1  12703  bitsp1o  12744  bitsfzo  12746  gcdadd  12786  gcdid  12787  gcd1  12788  1gcd  12793  bezoutlema  12800  bezoutlemb  12801  gcdmultiple  12821  lcmgcdlem  12879  lcm1  12883  3lcm2e6woprm  12888  isprm3  12920  prmgt1  12935  phicl2  13020  phibnd  13023  phi1  13025  dfphi2  13026  phimullem  13031  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemth  13038  fermltl  13040  prmdiv  13041  prmdiveq  13042  odzcllem  13049  odzdvds  13052  oddprm  13066  pythagtriplem4  13075  pcpre1  13099  pc1  13112  pcrec  13115  pcmpt  13150  fldivp1  13155  expnprm  13160  pockthlem  13163  igz  13181  4sqlem12  13209  4sqlem13m  13210  4sqlem19  13216  prmlem0  13248  1259lem4  13273  ballotfilemofi  13276  ballotfilem1  13277  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfmpn  13291  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilemsval  13309  ballotfilemrval  13318  ssnnctlemct  13394  mulgm1  14003  mulgp1  14016  mulgneg2  14017  gsumsncmn  14245  gsump1  14246  zsubrg  15026  gzsubrg  15027  zringmulg  15041  mulgrhm2  15053  sin2pim  16057  cos2pim  16058  rpcxp1  16149  logbleb  16214  logblt  16215  log2tlbndlog2  16237  ppiqp1le  16284  ppi1  16287  cht1  16288  cht2  16293  ppiqeq0  16297  ppiqltx  16298  ppiqub  16310  chtublem  16312  bposlem1  16328  bposlem2  16329  bposlem6  16333  lgslem2  16342  lgsfcl2  16347  lgsval2lem  16351  lgsmod  16367  lgsdir2lem1  16369  lgsdir2lem5  16373  lgsdir  16376  lgsne0  16379  1lgs  16384  lgsdinn0  16389  gausslemma2dlem0i  16398  gausslemma2d  16410  lgseisen  16415  lgsquad2lem2  16423  m1lgs  16426  2lgs  16445  2sqlem9  16465  2sqlem10  16466  usgrexmpldifpr  16712  upgr2wlkdc  16840  umgrclwwlkge2  16865  eupth2lem3lem4fi  16936  konigsbergvtx  16945  konigsbergiedg  16946  konigsbergumgr  16950  ex-fl  16961  apdiff  17321  qdiff  17322  iswomni0  17325  nconstwlpolem0  17337