Theorem 1z 9194

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 8845	. 2 |- 1 e. NN
2	1	nnzi 9189	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2128   1c1 7734   ZZcz 9168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4083  ax-pow 4136  ax-pr 4170  ax-un 4394  ax-setind 4497  ax-cnex 7824  ax-resscn 7825  ax-1cn 7826  ax-1re 7827  ax-icn 7828  ax-addcl 7829  ax-addrcl 7830  ax-mulcl 7831  ax-addcom 7833  ax-addass 7835  ax-distr 7837  ax-i2m1 7838  ax-0lt1 7839  ax-0id 7841  ax-rnegex 7842  ax-cnre 7844  ax-pre-ltirr 7845  ax-pre-ltwlin 7846  ax-pre-lttrn 7847  ax-pre-ltadd 7849

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-int 3809  df-br 3967  df-opab 4027  df-id 4254  df-xp 4593  df-rel 4594  df-cnv 4595  df-co 4596  df-dm 4597  df-iota 5136  df-fun 5173  df-fv 5179  df-riota 5781  df-ov 5828  df-oprab 5829  df-mpo 5830  df-pnf 7915  df-mnf 7916  df-xr 7917  df-ltxr 7918  df-le 7919  df-sub 8049  df-neg 8050  df-inn 8835  df-z 9169

This theorem is referenced by:  1zzd  9195  znnnlt1  9216  nn0n0n1ge2b  9244  nn0lt2  9246  nn0le2is012  9247  3halfnz  9262  prime  9264  nnuz  9475  eluz2nn  9478  eluzge3nn  9484  1eluzge0  9486  2eluzge1  9488  eluz2b1  9513  uz2m1nn  9517  elnn1uz2  9519  nn01to3  9527  nnrecq  9555  fz1n  9947  fz10  9949  fz01en  9956  fzpreddisj  9974  fznatpl1  9979  fzprval  9985  fztpval  9986  fseq1p1m1  9997  elfzp1b  10000  elfzm1b  10001  4fvwrd4  10043  ige2m2fzo  10101  fzo12sn  10120  fzofzp1  10130  fzostep1  10140  rebtwn2zlemstep  10156  qbtwnxr  10161  flqge1nn  10197  fldiv4p1lem1div2  10208  modqfrac  10240  modqid0  10253  q1mod  10259  mulp1mod1  10268  m1modnnsub1  10273  modqm1p1mod0  10278  modqltm1p1mod  10279  frecfzennn  10329  frecfzen2  10330  zexpcl  10438  qexpcl  10439  qexpclz  10444  m1expcl  10446  expp1zap  10472  expm1ap  10473  bcn1  10636  bcpasc  10644  bcnm1  10650  isfinite4im  10671  hashsng  10676  hashfz  10699  climuni  11194  sum0  11289  sumsnf  11310  expcnv  11405  cvgratz  11433  prod0  11486  prodsnf  11493  sin01gt0  11662  p1modz1  11694  iddvds  11704  1dvds  11705  dvds1  11749  nn0o1gt2  11800  n2dvds1  11807  gcdadd  11873  gcdid  11874  gcd1  11875  1gcd  11880  bezoutlema  11887  bezoutlemb  11888  gcdmultiple  11908  lcmgcdlem  11958  lcm1  11962  3lcm2e6woprm  11967  isprm3  11999  prmgt1  12013  phicl2  12093  phibnd  12096  phi1  12098  dfphi2  12099  phimullem  12104  eulerthlemrprm  12108  eulerthlema  12109  eulerthlemth  12111  fermltl  12113  prmdiv  12114  prmdiveq  12115  odzcllem  12121  odzdvds  12124  oddprm  12138  pythagtriplem4  12147  ssnnctlemct  12217  sin2pim  13176  cos2pim  13177  rpcxp1  13262  logbleb  13320  logblt  13321  ex-fl  13343  apdiff  13661  iswomni0  13664  nconstwlpolem0  13675