Theorem 1z 9225

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 8876	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 9220	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 2141  1c1 7762  ℤcz 9199

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-addcom 7861  ax-addass 7863  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-0id 7869  ax-rnegex 7870  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-ltadd 7877

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-iota 5158  df-fun 5198  df-fv 5204  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-inn 8866  df-z 9200

This theorem is referenced by:  1zzd  9226  znnnlt1  9247  nn0n0n1ge2b  9278  nn0lt2  9280  nn0le2is012  9281  3halfnz  9296  prime  9298  nnuz  9509  eluz2nn  9512  eluzge3nn  9518  1eluzge0  9520  2eluzge1  9522  eluz2b1  9547  uz2m1nn  9551  elnn1uz2  9553  elnndc  9558  nn01to3  9563  nnrecq  9591  fz1n  9987  fz10  9989  fz01en  9996  fzpreddisj  10014  fznatpl1  10019  fzprval  10025  fztpval  10026  fseq1p1m1  10037  elfzp1b  10040  elfzm1b  10041  4fvwrd4  10083  ige2m2fzo  10141  fzo12sn  10160  fzofzp1  10170  fzostep1  10180  rebtwn2zlemstep  10196  qbtwnxr  10201  flqge1nn  10237  fldiv4p1lem1div2  10248  modqfrac  10280  modqid0  10293  q1mod  10299  mulp1mod1  10308  m1modnnsub1  10313  modqm1p1mod0  10318  modqltm1p1mod  10319  frecfzennn  10369  frecfzen2  10370  zexpcl  10478  qexpcl  10479  qexpclz  10484  m1expcl  10486  expp1zap  10512  expm1ap  10513  bcn1  10679  bcpasc  10687  bcnm1  10693  isfinite4im  10714  hashsng  10720  hashfz  10743  climuni  11243  sum0  11338  sumsnf  11359  expcnv  11454  cvgratz  11482  prod0  11535  prodsnf  11542  sin01gt0  11711  p1modz1  11743  iddvds  11753  1dvds  11754  dvds1  11800  nn0o1gt2  11851  n2dvds1  11858  gcdadd  11927  gcdid  11928  gcd1  11929  1gcd  11934  bezoutlema  11941  bezoutlemb  11942  gcdmultiple  11962  lcmgcdlem  12018  lcm1  12022  3lcm2e6woprm  12027  isprm3  12059  prmgt1  12073  phicl2  12155  phibnd  12158  phi1  12160  dfphi2  12161  phimullem  12166  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemth  12173  fermltl  12175  prmdiv  12176  prmdiveq  12177  odzcllem  12183  odzdvds  12186  oddprm  12200  pythagtriplem4  12209  pcpre1  12233  pc1  12246  pcrec  12249  pcmpt  12282  fldivp1  12287  expnprm  12292  pockthlem  12295  igz  12313  ssnnctlemct  12388  sin2pim  13487  cos2pim  13488  rpcxp1  13573  logbleb  13632  logblt  13633  lgslem2  13655  lgsfcl2  13660  lgsval2lem  13664  lgsmod  13680  lgsdir2lem1  13682  lgsdir2lem5  13686  lgsdir  13689  lgsne0  13692  1lgs  13697  lgsdinn0  13702  2sqlem9  13713  2sqlem10  13714  ex-fl  13719  apdiff  14040  iswomni0  14043  nconstwlpolem0  14054