Theorem 1z 9480

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

Syntax hints:   ∈ wcel 2200  1c1 8008  ℤcz 9454

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 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-addcom 8107  ax-addass 8109  ax-distr 8111  ax-i2m1 8112  ax-0lt1 8113  ax-0id 8115  ax-rnegex 8116  ax-cnre 8118  ax-pre-ltirr 8119  ax-pre-ltwlin 8120  ax-pre-lttrn 8121  ax-pre-ltadd 8123

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 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8191  df-mnf 8192  df-xr 8193  df-ltxr 8194  df-le 8195  df-sub 8327  df-neg 8328  df-inn 9119  df-z 9455

This theorem is referenced by:  1zzd  9481  znnnlt1  9502  nn0n0n1ge2b  9534  nn0lt2  9536  nn0le2is012  9537  3halfnz  9552  prime  9554  nnuz  9766  eluz2nn  9769  eluzge3nn  9775  1eluzge0  9777  2eluzge1  9779  eluz2b1  9804  uz2m1nn  9808  elnn1uz2  9810  elnndc  9815  nn01to3  9820  nnrecq  9848  fz1n  10248  fz10  10250  fz01en  10257  fzpreddisj  10275  fznatpl1  10280  fzprval  10286  fztpval  10287  fseq1p1m1  10298  elfzp1b  10301  elfzm1b  10302  4fvwrd4  10344  ige2m2fzo  10412  fzo12sn  10431  fzofzp1  10441  fzostep1  10451  rebtwn2zlemstep  10480  qbtwnxr  10485  flqge1nn  10522  fldiv4p1lem1div2  10533  fldiv4lem1div2  10535  modqfrac  10567  modqid0  10580  q1mod  10586  mulp1mod1  10595  m1modnnsub1  10600  modqm1p1mod0  10605  modqltm1p1mod  10606  frecfzennn  10656  frecfzen2  10657  zexpcl  10784  qexpcl  10785  qexpclz  10790  m1expcl  10792  expp1zap  10818  expm1ap  10819  bcn1  10988  bcpasc  10996  bcnm1  11002  isfinite4im  11022  hashsng  11028  hashfz  11051  climuni  11812  sum0  11907  sumsnf  11928  expcnv  12023  cvgratz  12051  prod0  12104  prodsnf  12111  sinltxirr  12280  sin01gt0  12281  p1modz1  12313  iddvds  12323  1dvds  12324  dvds1  12372  3dvds  12383  nn0o1gt2  12424  n2dvds1  12431  bitsp1o  12472  bitsfzo  12474  gcdadd  12514  gcdid  12515  gcd1  12516  1gcd  12521  bezoutlema  12528  bezoutlemb  12529  gcdmultiple  12549  lcmgcdlem  12607  lcm1  12611  3lcm2e6woprm  12616  isprm3  12648  prmgt1  12662  phicl2  12744  phibnd  12747  phi1  12749  dfphi2  12750  phimullem  12755  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemth  12762  fermltl  12764  prmdiv  12765  prmdiveq  12766  odzcllem  12773  odzdvds  12776  oddprm  12790  pythagtriplem4  12799  pcpre1  12823  pc1  12836  pcrec  12839  pcmpt  12874  fldivp1  12879  expnprm  12884  pockthlem  12887  igz  12905  4sqlem12  12933  4sqlem13m  12934  4sqlem19  12940  ssnnctlemct  13025  mulgm1  13687  mulgp1  13700  mulgneg2  13701  zsubrg  14553  gzsubrg  14554  zringmulg  14570  mulgrhm2  14582  sin2pim  15495  cos2pim  15496  rpcxp1  15581  logbleb  15643  logblt  15644  lgslem2  15688  lgsfcl2  15693  lgsval2lem  15697  lgsmod  15713  lgsdir2lem1  15715  lgsdir2lem5  15719  lgsdir  15722  lgsne0  15725  1lgs  15730  lgsdinn0  15735  gausslemma2dlem0i  15744  gausslemma2d  15756  lgseisen  15761  lgsquad2lem2  15769  m1lgs  15772  2lgs  15791  2sqlem9  15811  2sqlem10  15812  upgr2wlkdc  16096  ex-fl  16113  apdiff  16446  iswomni0  16449  nconstwlpolem0  16461