Theorem 1z 9681

Description: One is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
1z	⊢ 1 ∈ ℤ

Proof of Theorem 1z

Step	Hyp	Ref	Expression
1		1nn 9324	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 9676	1 ⊢ 1 ∈ ℤ

This proof depends on syntax axioms:   ∈ wcel 2209  1c1 8186  ℤcz 9655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-ltadd 8301

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-inn 9314  df-z 9656

This theorem is used by:  1zzd  9682  znnnlt1  9703  nn0n0n1ge2b  9736  nn0lt2  9738  nn0le2is012  9739  3halfnz  9754  prime  9756  nnuz  9974  eluz2nn  9982  eluzge3nn  9988  1eluzge0  9990  2eluzge1  9992  eluz2b1  10017  uz2m1nn  10021  elnn1uz2  10023  elnndc  10028  nn01to3  10033  nnrecq  10061  fz1n  10465  fz10  10467  fz01en  10476  fzpreddisj  10495  fznatpl1  10500  fzprval  10506  fztpval  10507  fseq1p1m1  10518  elfzp1b  10521  elfzm1b  10522  4fvwrd4  10564  ige2m2fzo  10633  fzo12sn  10652  fzofzp1  10662  fzostep1  10673  rebtwn2zlemstep  10704  qbtwnxr  10709  flqge1nn  10750  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  modqfrac  10795  modqid0  10808  q1mod  10814  mulp1mod1  10823  m1modnnsub1  10828  modqm1p1mod0  10833  modqltm1p1mod  10834  frecfzennn  10884  frecfzen2  10885  zexpcl  11012  qexpcl  11013  qexpclz  11018  m1expcl  11020  expp1zap  11046  expm1ap  11047  bcn1  11218  bcpasc  11226  bcnm1  11233  isfinite4im  11253  hashsng  11259  hashfz  11284  ssenneg  11302  fiidxsupcl  12018  climuni  12084  sum0  12180  sumsnf  12201  expcnv  12296  cvgratz  12324  prod0  12377  prodsnf  12384  sinltxirr  12553  sin01gt0  12554  p1modz1  12586  iddvds  12596  1dvds  12597  dvds1  12645  3dvds  12656  nn0o1gt2  12697  n2dvds1  12704  bitsp1o  12745  bitsfzo  12747  gcdadd  12787  gcdid  12788  gcd1  12789  1gcd  12794  bezoutlema  12801  bezoutlemb  12802  gcdmultiple  12822  lcmgcdlem  12880  lcm1  12884  3lcm2e6woprm  12889  isprm3  12921  prmgt1  12936  phicl2  13021  phibnd  13024  phi1  13026  dfphi2  13027  phimullem  13032  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemth  13039  fermltl  13041  prmdiv  13042  prmdiveq  13043  odzcllem  13050  odzdvds  13053  oddprm  13067  pythagtriplem4  13076  pcpre1  13100  pc1  13113  pcrec  13116  pcmpt  13151  fldivp1  13156  expnprm  13161  pockthlem  13164  igz  13182  4sqlem12  13210  4sqlem13m  13211  4sqlem19  13217  prmlem0  13249  1259lem4  13274  ballotfilemofi  13277  ballotfilem1  13278  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilemsval  13310  ballotfilemrval  13319  ssnnctlemct  13395  mulgm1  14004  mulgp1  14017  mulgneg2  14018  gsumsncmn  14246  gsump1  14247  zsubrg  15027  gzsubrg  15028  zringmulg  15042  mulgrhm2  15054  sin2pim  16040  cos2pim  16041  rpcxp1  16132  logbleb  16197  logblt  16198  log2tlbndlog2  16220  ppiqp1le  16267  ppi1  16270  cht1  16271  cht2  16276  ppiqeq0  16280  ppiqltx  16281  ppiqub  16293  chtublem  16295  bposlem1  16311  bposlem2  16312  bposlem6  16316  lgslem2  16325  lgsfcl2  16330  lgsval2lem  16334  lgsmod  16350  lgsdir2lem1  16352  lgsdir2lem5  16356  lgsdir  16359  lgsne0  16362  1lgs  16367  lgsdinn0  16372  gausslemma2dlem0i  16381  gausslemma2d  16393  lgseisen  16398  lgsquad2lem2  16406  m1lgs  16409  2lgs  16428  2sqlem9  16448  2sqlem10  16449  usgrexmpldifpr  16695  upgr2wlkdc  16823  umgrclwwlkge2  16848  eupth2lem3lem4fi  16919  konigsbergvtx  16928  konigsbergiedg  16929  konigsbergumgr  16933  ex-fl  16944  apdiff  17304  qdiff  17305  iswomni0  17308  nconstwlpolem0  17320