Theorem 1z 9273

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 8924	. 2 |- 1 e. NN
2	1	nnzi 9268	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2148   1c1 7807   ZZcz 9247

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-cnex 7897  ax-resscn 7898  ax-1cn 7899  ax-1re 7900  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-addcom 7906  ax-addass 7908  ax-distr 7910  ax-i2m1 7911  ax-0lt1 7912  ax-0id 7914  ax-rnegex 7915  ax-cnre 7917  ax-pre-ltirr 7918  ax-pre-ltwlin 7919  ax-pre-lttrn 7920  ax-pre-ltadd 7922

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-br 4002  df-opab 4063  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-pnf 7988  df-mnf 7989  df-xr 7990  df-ltxr 7991  df-le 7992  df-sub 8124  df-neg 8125  df-inn 8914  df-z 9248

This theorem is referenced by:  1zzd  9274  znnnlt1  9295  nn0n0n1ge2b  9326  nn0lt2  9328  nn0le2is012  9329  3halfnz  9344  prime  9346  nnuz  9557  eluz2nn  9560  eluzge3nn  9566  1eluzge0  9568  2eluzge1  9570  eluz2b1  9595  uz2m1nn  9599  elnn1uz2  9601  elnndc  9606  nn01to3  9611  nnrecq  9639  fz1n  10037  fz10  10039  fz01en  10046  fzpreddisj  10064  fznatpl1  10069  fzprval  10075  fztpval  10076  fseq1p1m1  10087  elfzp1b  10090  elfzm1b  10091  4fvwrd4  10133  ige2m2fzo  10191  fzo12sn  10210  fzofzp1  10220  fzostep1  10230  rebtwn2zlemstep  10246  qbtwnxr  10251  flqge1nn  10287  fldiv4p1lem1div2  10298  modqfrac  10330  modqid0  10343  q1mod  10349  mulp1mod1  10358  m1modnnsub1  10363  modqm1p1mod0  10368  modqltm1p1mod  10369  frecfzennn  10419  frecfzen2  10420  zexpcl  10528  qexpcl  10529  qexpclz  10534  m1expcl  10536  expp1zap  10562  expm1ap  10563  bcn1  10729  bcpasc  10737  bcnm1  10743  isfinite4im  10763  hashsng  10769  hashfz  10792  climuni  11292  sum0  11387  sumsnf  11408  expcnv  11503  cvgratz  11531  prod0  11584  prodsnf  11591  sin01gt0  11760  p1modz1  11792  iddvds  11802  1dvds  11803  dvds1  11849  nn0o1gt2  11900  n2dvds1  11907  gcdadd  11976  gcdid  11977  gcd1  11978  1gcd  11983  bezoutlema  11990  bezoutlemb  11991  gcdmultiple  12011  lcmgcdlem  12067  lcm1  12071  3lcm2e6woprm  12076  isprm3  12108  prmgt1  12122  phicl2  12204  phibnd  12207  phi1  12209  dfphi2  12210  phimullem  12215  eulerthlemrprm  12219  eulerthlema  12220  eulerthlemth  12222  fermltl  12224  prmdiv  12225  prmdiveq  12226  odzcllem  12232  odzdvds  12235  oddprm  12249  pythagtriplem4  12258  pcpre1  12282  pc1  12295  pcrec  12298  pcmpt  12331  fldivp1  12336  expnprm  12341  pockthlem  12344  igz  12362  ssnnctlemct  12437  mulgm1  12931  mulgp1  12943  mulgneg2  12944  sin2pim  14016  cos2pim  14017  rpcxp1  14102  logbleb  14161  logblt  14162  lgslem2  14184  lgsfcl2  14189  lgsval2lem  14193  lgsmod  14209  lgsdir2lem1  14211  lgsdir2lem5  14215  lgsdir  14218  lgsne0  14221  1lgs  14226  lgsdinn0  14231  2sqlem9  14242  2sqlem10  14243  ex-fl  14248  apdiff  14567  iswomni0  14570  nconstwlpolem0  14581