Theorem 1z 9603

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 9248	. 2 |- 1 e. NN
2	1	nnzi 9598	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2203   1c1 8128   ZZcz 9577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-z 9578

This theorem is referenced by:  1zzd  9604  znnnlt1  9625  nn0n0n1ge2b  9657  nn0lt2  9659  nn0le2is012  9660  3halfnz  9675  prime  9677  nnuz  9890  eluz2nn  9898  eluzge3nn  9904  1eluzge0  9906  2eluzge1  9908  eluz2b1  9933  uz2m1nn  9937  elnn1uz2  9939  elnndc  9944  nn01to3  9949  nnrecq  9977  fz1n  10378  fz10  10380  fz01en  10387  fzpreddisj  10405  fznatpl1  10410  fzprval  10416  fztpval  10417  fseq1p1m1  10428  elfzp1b  10431  elfzm1b  10432  4fvwrd4  10474  ige2m2fzo  10543  fzo12sn  10562  fzofzp1  10572  fzostep1  10583  rebtwn2zlemstep  10612  qbtwnxr  10617  flqge1nn  10654  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  modqfrac  10699  modqid0  10712  q1mod  10718  mulp1mod1  10727  m1modnnsub1  10732  modqm1p1mod0  10737  modqltm1p1mod  10738  frecfzennn  10788  frecfzen2  10789  zexpcl  10916  qexpcl  10917  qexpclz  10922  m1expcl  10924  expp1zap  10950  expm1ap  10951  bcn1  11120  bcpasc  11128  bcnm1  11135  isfinite4im  11155  hashsng  11161  hashfz  11186  ssenneg  11204  climuni  11978  sum0  12074  sumsnf  12095  expcnv  12190  cvgratz  12218  prod0  12271  prodsnf  12278  sinltxirr  12447  sin01gt0  12448  p1modz1  12480  iddvds  12490  1dvds  12491  dvds1  12539  3dvds  12550  nn0o1gt2  12591  n2dvds1  12598  bitsp1o  12639  bitsfzo  12641  gcdadd  12681  gcdid  12682  gcd1  12683  1gcd  12688  bezoutlema  12695  bezoutlemb  12696  gcdmultiple  12716  lcmgcdlem  12774  lcm1  12778  3lcm2e6woprm  12783  isprm3  12815  prmgt1  12829  phicl2  12911  phibnd  12914  phi1  12916  dfphi2  12917  phimullem  12922  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemth  12929  fermltl  12931  prmdiv  12932  prmdiveq  12933  odzcllem  12940  odzdvds  12943  oddprm  12957  pythagtriplem4  12966  pcpre1  12990  pc1  13003  pcrec  13006  pcmpt  13041  fldivp1  13046  expnprm  13051  pockthlem  13054  igz  13072  4sqlem12  13100  4sqlem13m  13101  4sqlem19  13107  ballotfilemofi  13138  ballotfilem1  13139  ballotfilem2  13142  ssnnctlemct  13197  mulgm1  13859  mulgp1  13872  mulgneg2  13873  zsubrg  14729  gzsubrg  14730  zringmulg  14746  mulgrhm2  14758  sin2pim  15678  cos2pim  15679  rpcxp1  15764  logbleb  15826  logblt  15827  lgslem2  15874  lgsfcl2  15879  lgsval2lem  15883  lgsmod  15899  lgsdir2lem1  15901  lgsdir2lem5  15905  lgsdir  15908  lgsne0  15911  1lgs  15916  lgsdinn0  15921  gausslemma2dlem0i  15930  gausslemma2d  15942  lgseisen  15947  lgsquad2lem2  15955  m1lgs  15958  2lgs  15977  2sqlem9  15997  2sqlem10  15998  usgrexmpldifpr  16244  upgr2wlkdc  16372  umgrclwwlkge2  16397  eupth2lem3lem4fi  16468  konigsbergvtx  16477  konigsbergiedg  16478  konigsbergumgr  16482  ex-fl  16493  apdiff  16832  qdiff  16833  iswomni0  16836  nconstwlpolem0  16849  gfsumsn  16867  gfsump1  16868