Theorem 1z 9620

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 9265	. 2 |- 1 e. NN
2	1	nnzi 9615	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2205   1c1 8144   ZZcz 9594

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 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-addcom 8243  ax-addass 8245  ax-distr 8247  ax-i2m1 8248  ax-0lt1 8249  ax-0id 8251  ax-rnegex 8252  ax-cnre 8254  ax-pre-ltirr 8255  ax-pre-ltwlin 8256  ax-pre-lttrn 8257  ax-pre-ltadd 8259

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 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-opab 4177  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365  df-riota 6011  df-ov 6061  df-oprab 6062  df-mpo 6063  df-pnf 8326  df-mnf 8327  df-xr 8328  df-ltxr 8329  df-le 8330  df-sub 8462  df-neg 8463  df-inn 9255  df-z 9595

This theorem is referenced by:  1zzd  9621  znnnlt1  9642  nn0n0n1ge2b  9675  nn0lt2  9677  nn0le2is012  9678  3halfnz  9693  prime  9695  nnuz  9908  eluz2nn  9916  eluzge3nn  9922  1eluzge0  9924  2eluzge1  9926  eluz2b1  9951  uz2m1nn  9955  elnn1uz2  9957  elnndc  9962  nn01to3  9967  nnrecq  9995  fz1n  10398  fz10  10400  fz01en  10408  fzpreddisj  10427  fznatpl1  10432  fzprval  10438  fztpval  10439  fseq1p1m1  10450  elfzp1b  10453  elfzm1b  10454  4fvwrd4  10496  ige2m2fzo  10565  fzo12sn  10584  fzofzp1  10594  fzostep1  10605  rebtwn2zlemstep  10636  qbtwnxr  10641  flqge1nn  10678  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  modqfrac  10723  modqid0  10736  q1mod  10742  mulp1mod1  10751  m1modnnsub1  10756  modqm1p1mod0  10761  modqltm1p1mod  10762  frecfzennn  10812  frecfzen2  10813  zexpcl  10940  qexpcl  10941  qexpclz  10946  m1expcl  10948  expp1zap  10974  expm1ap  10975  bcn1  11145  bcpasc  11153  bcnm1  11160  isfinite4im  11180  hashsng  11186  hashfz  11211  ssenneg  11229  climuni  12003  sum0  12099  sumsnf  12120  expcnv  12215  cvgratz  12243  prod0  12296  prodsnf  12303  sinltxirr  12472  sin01gt0  12473  p1modz1  12505  iddvds  12515  1dvds  12516  dvds1  12564  3dvds  12575  nn0o1gt2  12616  n2dvds1  12623  bitsp1o  12664  bitsfzo  12666  gcdadd  12706  gcdid  12707  gcd1  12708  1gcd  12713  bezoutlema  12720  bezoutlemb  12721  gcdmultiple  12741  lcmgcdlem  12799  lcm1  12803  3lcm2e6woprm  12808  isprm3  12840  prmgt1  12854  phicl2  12936  phibnd  12939  phi1  12941  dfphi2  12942  phimullem  12947  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemth  12954  fermltl  12956  prmdiv  12957  prmdiveq  12958  odzcllem  12965  odzdvds  12968  oddprm  12982  pythagtriplem4  12991  pcpre1  13015  pc1  13028  pcrec  13031  pcmpt  13066  fldivp1  13071  expnprm  13076  pockthlem  13079  igz  13097  4sqlem12  13125  4sqlem13m  13126  4sqlem19  13132  ballotfilemofi  13163  ballotfilem1  13164  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilemsval  13196  ballotfilemrval  13205  ssnnctlemct  13281  mulgm1  13895  mulgp1  13908  mulgneg2  13909  gfsumsn  14107  gfsump1  14108  zsubrg  14855  gzsubrg  14856  zringmulg  14872  mulgrhm2  14884  sin2pim  15804  cos2pim  15805  rpcxp1  15890  logbleb  15952  logblt  15953  lgslem2  16000  lgsfcl2  16005  lgsval2lem  16009  lgsmod  16025  lgsdir2lem1  16027  lgsdir2lem5  16031  lgsdir  16034  lgsne0  16037  1lgs  16042  lgsdinn0  16047  gausslemma2dlem0i  16056  gausslemma2d  16068  lgseisen  16073  lgsquad2lem2  16081  m1lgs  16084  2lgs  16103  2sqlem9  16123  2sqlem10  16124  usgrexmpldifpr  16370  upgr2wlkdc  16498  umgrclwwlkge2  16523  eupth2lem3lem4fi  16594  konigsbergvtx  16603  konigsbergiedg  16604  konigsbergumgr  16608  ex-fl  16619  apdiff  16958  qdiff  16959  iswomni0  16962  nconstwlpolem0  16975