Theorem 1z 9495

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 9144	. 2 |- 1 e. NN
2	1	nnzi 9490	1 |- 1 e. ZZ

Syntax hints:   e. wcel 2200   1c1 8023   ZZcz 9469

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-ltwlin 8135  ax-pre-lttrn 8136  ax-pre-ltadd 8138

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210  df-sub 8342  df-neg 8343  df-inn 9134  df-z 9470

This theorem is referenced by:  1zzd  9496  znnnlt1  9517  nn0n0n1ge2b  9549  nn0lt2  9551  nn0le2is012  9552  3halfnz  9567  prime  9569  nnuz  9782  eluz2nn  9790  eluzge3nn  9796  1eluzge0  9798  2eluzge1  9800  eluz2b1  9825  uz2m1nn  9829  elnn1uz2  9831  elnndc  9836  nn01to3  9841  nnrecq  9869  fz1n  10269  fz10  10271  fz01en  10278  fzpreddisj  10296  fznatpl1  10301  fzprval  10307  fztpval  10308  fseq1p1m1  10319  elfzp1b  10322  elfzm1b  10323  4fvwrd4  10365  ige2m2fzo  10433  fzo12sn  10452  fzofzp1  10462  fzostep1  10473  rebtwn2zlemstep  10502  qbtwnxr  10507  flqge1nn  10544  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  modqfrac  10589  modqid0  10602  q1mod  10608  mulp1mod1  10617  m1modnnsub1  10622  modqm1p1mod0  10627  modqltm1p1mod  10628  frecfzennn  10678  frecfzen2  10679  zexpcl  10806  qexpcl  10807  qexpclz  10812  m1expcl  10814  expp1zap  10840  expm1ap  10841  bcn1  11010  bcpasc  11018  bcnm1  11024  isfinite4im  11044  hashsng  11050  hashfz  11075  climuni  11844  sum0  11939  sumsnf  11960  expcnv  12055  cvgratz  12083  prod0  12136  prodsnf  12143  sinltxirr  12312  sin01gt0  12313  p1modz1  12345  iddvds  12355  1dvds  12356  dvds1  12404  3dvds  12415  nn0o1gt2  12456  n2dvds1  12463  bitsp1o  12504  bitsfzo  12506  gcdadd  12546  gcdid  12547  gcd1  12548  1gcd  12553  bezoutlema  12560  bezoutlemb  12561  gcdmultiple  12581  lcmgcdlem  12639  lcm1  12643  3lcm2e6woprm  12648  isprm3  12680  prmgt1  12694  phicl2  12776  phibnd  12779  phi1  12781  dfphi2  12782  phimullem  12787  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemth  12794  fermltl  12796  prmdiv  12797  prmdiveq  12798  odzcllem  12805  odzdvds  12808  oddprm  12822  pythagtriplem4  12831  pcpre1  12855  pc1  12868  pcrec  12871  pcmpt  12906  fldivp1  12911  expnprm  12916  pockthlem  12919  igz  12937  4sqlem12  12965  4sqlem13m  12966  4sqlem19  12972  ssnnctlemct  13057  mulgm1  13719  mulgp1  13732  mulgneg2  13733  zsubrg  14585  gzsubrg  14586  zringmulg  14602  mulgrhm2  14614  sin2pim  15527  cos2pim  15528  rpcxp1  15613  logbleb  15675  logblt  15676  lgslem2  15720  lgsfcl2  15725  lgsval2lem  15729  lgsmod  15745  lgsdir2lem1  15747  lgsdir2lem5  15751  lgsdir  15754  lgsne0  15757  1lgs  15762  lgsdinn0  15767  gausslemma2dlem0i  15776  gausslemma2d  15788  lgseisen  15793  lgsquad2lem2  15801  m1lgs  15804  2lgs  15823  2sqlem9  15843  2sqlem10  15844  usgrexmpldifpr  16088  upgr2wlkdc  16172  umgrclwwlkge2  16197  ex-fl  16257  apdiff  16588  iswomni0  16591  nconstwlpolem0  16603