Theorem 1z 9433

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 9082	. 2 |- 1 e. NN
2	1	nnzi 9428	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2178   1c1 7961   ZZcz 9407

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-distr 8064  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-cnre 8071  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-iota 5251  df-fun 5292  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-sub 8280  df-neg 8281  df-inn 9072  df-z 9408

This theorem is referenced by:  1zzd  9434  znnnlt1  9455  nn0n0n1ge2b  9487  nn0lt2  9489  nn0le2is012  9490  3halfnz  9505  prime  9507  nnuz  9719  eluz2nn  9722  eluzge3nn  9728  1eluzge0  9730  2eluzge1  9732  eluz2b1  9757  uz2m1nn  9761  elnn1uz2  9763  elnndc  9768  nn01to3  9773  nnrecq  9801  fz1n  10201  fz10  10203  fz01en  10210  fzpreddisj  10228  fznatpl1  10233  fzprval  10239  fztpval  10240  fseq1p1m1  10251  elfzp1b  10254  elfzm1b  10255  4fvwrd4  10297  ige2m2fzo  10364  fzo12sn  10383  fzofzp1  10393  fzostep1  10403  rebtwn2zlemstep  10432  qbtwnxr  10437  flqge1nn  10474  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  modqfrac  10519  modqid0  10532  q1mod  10538  mulp1mod1  10547  m1modnnsub1  10552  modqm1p1mod0  10557  modqltm1p1mod  10558  frecfzennn  10608  frecfzen2  10609  zexpcl  10736  qexpcl  10737  qexpclz  10742  m1expcl  10744  expp1zap  10770  expm1ap  10771  bcn1  10940  bcpasc  10948  bcnm1  10954  isfinite4im  10974  hashsng  10980  hashfz  11003  climuni  11719  sum0  11814  sumsnf  11835  expcnv  11930  cvgratz  11958  prod0  12011  prodsnf  12018  sinltxirr  12187  sin01gt0  12188  p1modz1  12220  iddvds  12230  1dvds  12231  dvds1  12279  3dvds  12290  nn0o1gt2  12331  n2dvds1  12338  bitsp1o  12379  bitsfzo  12381  gcdadd  12421  gcdid  12422  gcd1  12423  1gcd  12428  bezoutlema  12435  bezoutlemb  12436  gcdmultiple  12456  lcmgcdlem  12514  lcm1  12518  3lcm2e6woprm  12523  isprm3  12555  prmgt1  12569  phicl2  12651  phibnd  12654  phi1  12656  dfphi2  12657  phimullem  12662  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemth  12669  fermltl  12671  prmdiv  12672  prmdiveq  12673  odzcllem  12680  odzdvds  12683  oddprm  12697  pythagtriplem4  12706  pcpre1  12730  pc1  12743  pcrec  12746  pcmpt  12781  fldivp1  12786  expnprm  12791  pockthlem  12794  igz  12812  4sqlem12  12840  4sqlem13m  12841  4sqlem19  12847  ssnnctlemct  12932  mulgm1  13593  mulgp1  13606  mulgneg2  13607  zsubrg  14458  gzsubrg  14459  zringmulg  14475  mulgrhm2  14487  sin2pim  15400  cos2pim  15401  rpcxp1  15486  logbleb  15548  logblt  15549  lgslem2  15593  lgsfcl2  15598  lgsval2lem  15602  lgsmod  15618  lgsdir2lem1  15620  lgsdir2lem5  15624  lgsdir  15627  lgsne0  15630  1lgs  15635  lgsdinn0  15640  gausslemma2dlem0i  15649  gausslemma2d  15661  lgseisen  15666  lgsquad2lem2  15674  m1lgs  15677  2lgs  15696  2sqlem9  15716  2sqlem10  15717  ex-fl  15861  apdiff  16189  iswomni0  16192  nconstwlpolem0  16204