Theorem 1z 9505

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

Syntax hints:   ∈ wcel 2202  1c1 8033  ℤcz 9479

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-z 9480

This theorem is referenced by:  1zzd  9506  znnnlt1  9527  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  3halfnz  9577  prime  9579  nnuz  9792  eluz2nn  9800  eluzge3nn  9806  1eluzge0  9808  2eluzge1  9810  eluz2b1  9835  uz2m1nn  9839  elnn1uz2  9841  elnndc  9846  nn01to3  9851  nnrecq  9879  fz1n  10279  fz10  10281  fz01en  10288  fzpreddisj  10306  fznatpl1  10311  fzprval  10317  fztpval  10318  fseq1p1m1  10329  elfzp1b  10332  elfzm1b  10333  4fvwrd4  10375  ige2m2fzo  10444  fzo12sn  10463  fzofzp1  10473  fzostep1  10484  rebtwn2zlemstep  10513  qbtwnxr  10518  flqge1nn  10555  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  modqfrac  10600  modqid0  10613  q1mod  10619  mulp1mod1  10628  m1modnnsub1  10633  modqm1p1mod0  10638  modqltm1p1mod  10639  frecfzennn  10689  frecfzen2  10690  zexpcl  10817  qexpcl  10818  qexpclz  10823  m1expcl  10825  expp1zap  10851  expm1ap  10852  bcn1  11021  bcpasc  11029  bcnm1  11035  isfinite4im  11055  hashsng  11061  hashfz  11086  climuni  11871  sum0  11967  sumsnf  11988  expcnv  12083  cvgratz  12111  prod0  12164  prodsnf  12171  sinltxirr  12340  sin01gt0  12341  p1modz1  12373  iddvds  12383  1dvds  12384  dvds1  12432  3dvds  12443  nn0o1gt2  12484  n2dvds1  12491  bitsp1o  12532  bitsfzo  12534  gcdadd  12574  gcdid  12575  gcd1  12576  1gcd  12581  bezoutlema  12588  bezoutlemb  12589  gcdmultiple  12609  lcmgcdlem  12667  lcm1  12671  3lcm2e6woprm  12676  isprm3  12708  prmgt1  12722  phicl2  12804  phibnd  12807  phi1  12809  dfphi2  12810  phimullem  12815  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemth  12822  fermltl  12824  prmdiv  12825  prmdiveq  12826  odzcllem  12833  odzdvds  12836  oddprm  12850  pythagtriplem4  12859  pcpre1  12883  pc1  12896  pcrec  12899  pcmpt  12934  fldivp1  12939  expnprm  12944  pockthlem  12947  igz  12965  4sqlem12  12993  4sqlem13m  12994  4sqlem19  13000  ssnnctlemct  13085  mulgm1  13747  mulgp1  13760  mulgneg2  13761  zsubrg  14614  gzsubrg  14615  zringmulg  14631  mulgrhm2  14643  sin2pim  15556  cos2pim  15557  rpcxp1  15642  logbleb  15704  logblt  15705  lgslem2  15749  lgsfcl2  15754  lgsval2lem  15758  lgsmod  15774  lgsdir2lem1  15776  lgsdir2lem5  15780  lgsdir  15783  lgsne0  15786  1lgs  15791  lgsdinn0  15796  gausslemma2dlem0i  15805  gausslemma2d  15817  lgseisen  15822  lgsquad2lem2  15830  m1lgs  15833  2lgs  15852  2sqlem9  15872  2sqlem10  15873  usgrexmpldifpr  16119  upgr2wlkdc  16247  umgrclwwlkge2  16272  eupth2lem3lem4fi  16343  konigsbergvtx  16352  konigsbergiedg  16353  konigsbergumgr  16357  ex-fl  16368  apdiff  16703  qdiff  16704  iswomni0  16707  nconstwlpolem0  16719  gfsumsn  16737  gfsump1  16738