Theorem 1z 9352

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

Syntax hints:   ∈ wcel 2167  1c1 7880  ℤcz 9326

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-ltadd 7995

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-iota 5219  df-fun 5260  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-z 9327

This theorem is referenced by:  1zzd  9353  znnnlt1  9374  nn0n0n1ge2b  9405  nn0lt2  9407  nn0le2is012  9408  3halfnz  9423  prime  9425  nnuz  9637  eluz2nn  9640  eluzge3nn  9646  1eluzge0  9648  2eluzge1  9650  eluz2b1  9675  uz2m1nn  9679  elnn1uz2  9681  elnndc  9686  nn01to3  9691  nnrecq  9719  fz1n  10119  fz10  10121  fz01en  10128  fzpreddisj  10146  fznatpl1  10151  fzprval  10157  fztpval  10158  fseq1p1m1  10169  elfzp1b  10172  elfzm1b  10173  4fvwrd4  10215  ige2m2fzo  10274  fzo12sn  10293  fzofzp1  10303  fzostep1  10313  rebtwn2zlemstep  10342  qbtwnxr  10347  flqge1nn  10384  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  modqfrac  10429  modqid0  10442  q1mod  10448  mulp1mod1  10457  m1modnnsub1  10462  modqm1p1mod0  10467  modqltm1p1mod  10468  frecfzennn  10518  frecfzen2  10519  zexpcl  10646  qexpcl  10647  qexpclz  10652  m1expcl  10654  expp1zap  10680  expm1ap  10681  bcn1  10850  bcpasc  10858  bcnm1  10864  isfinite4im  10884  hashsng  10890  hashfz  10913  climuni  11458  sum0  11553  sumsnf  11574  expcnv  11669  cvgratz  11697  prod0  11750  prodsnf  11757  sinltxirr  11926  sin01gt0  11927  p1modz1  11959  iddvds  11969  1dvds  11970  dvds1  12018  3dvds  12029  nn0o1gt2  12070  n2dvds1  12077  bitsp1o  12117  bitsfzo  12119  gcdadd  12152  gcdid  12153  gcd1  12154  1gcd  12159  bezoutlema  12166  bezoutlemb  12167  gcdmultiple  12187  lcmgcdlem  12245  lcm1  12249  3lcm2e6woprm  12254  isprm3  12286  prmgt1  12300  phicl2  12382  phibnd  12385  phi1  12387  dfphi2  12388  phimullem  12393  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemth  12400  fermltl  12402  prmdiv  12403  prmdiveq  12404  odzcllem  12411  odzdvds  12414  oddprm  12428  pythagtriplem4  12437  pcpre1  12461  pc1  12474  pcrec  12477  pcmpt  12512  fldivp1  12517  expnprm  12522  pockthlem  12525  igz  12543  4sqlem12  12571  4sqlem13m  12572  4sqlem19  12578  ssnnctlemct  12663  mulgm1  13272  mulgp1  13285  mulgneg2  13286  zsubrg  14137  gzsubrg  14138  zringmulg  14154  mulgrhm2  14166  sin2pim  15049  cos2pim  15050  rpcxp1  15135  logbleb  15197  logblt  15198  lgslem2  15242  lgsfcl2  15247  lgsval2lem  15251  lgsmod  15267  lgsdir2lem1  15269  lgsdir2lem5  15273  lgsdir  15276  lgsne0  15279  1lgs  15284  lgsdinn0  15289  gausslemma2dlem0i  15298  gausslemma2d  15310  lgseisen  15315  lgsquad2lem2  15323  m1lgs  15326  2lgs  15345  2sqlem9  15365  2sqlem10  15366  ex-fl  15371  apdiff  15692  iswomni0  15695  nconstwlpolem0  15707