Theorem 1z 9460

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

Syntax hints:   ∈ wcel 2200  1c1 7988  ℤcz 9434

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 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-addcom 8087  ax-addass 8089  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-0id 8095  ax-rnegex 8096  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-ltwlin 8100  ax-pre-lttrn 8101  ax-pre-ltadd 8103

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 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-pnf 8171  df-mnf 8172  df-xr 8173  df-ltxr 8174  df-le 8175  df-sub 8307  df-neg 8308  df-inn 9099  df-z 9435

This theorem is referenced by:  1zzd  9461  znnnlt1  9482  nn0n0n1ge2b  9514  nn0lt2  9516  nn0le2is012  9517  3halfnz  9532  prime  9534  nnuz  9746  eluz2nn  9749  eluzge3nn  9755  1eluzge0  9757  2eluzge1  9759  eluz2b1  9784  uz2m1nn  9788  elnn1uz2  9790  elnndc  9795  nn01to3  9800  nnrecq  9828  fz1n  10228  fz10  10230  fz01en  10237  fzpreddisj  10255  fznatpl1  10260  fzprval  10266  fztpval  10267  fseq1p1m1  10278  elfzp1b  10281  elfzm1b  10282  4fvwrd4  10324  ige2m2fzo  10391  fzo12sn  10410  fzofzp1  10420  fzostep1  10430  rebtwn2zlemstep  10459  qbtwnxr  10464  flqge1nn  10501  fldiv4p1lem1div2  10512  fldiv4lem1div2  10514  modqfrac  10546  modqid0  10559  q1mod  10565  mulp1mod1  10574  m1modnnsub1  10579  modqm1p1mod0  10584  modqltm1p1mod  10585  frecfzennn  10635  frecfzen2  10636  zexpcl  10763  qexpcl  10764  qexpclz  10769  m1expcl  10771  expp1zap  10797  expm1ap  10798  bcn1  10967  bcpasc  10975  bcnm1  10981  isfinite4im  11001  hashsng  11007  hashfz  11030  climuni  11790  sum0  11885  sumsnf  11906  expcnv  12001  cvgratz  12029  prod0  12082  prodsnf  12089  sinltxirr  12258  sin01gt0  12259  p1modz1  12291  iddvds  12301  1dvds  12302  dvds1  12350  3dvds  12361  nn0o1gt2  12402  n2dvds1  12409  bitsp1o  12450  bitsfzo  12452  gcdadd  12492  gcdid  12493  gcd1  12494  1gcd  12499  bezoutlema  12506  bezoutlemb  12507  gcdmultiple  12527  lcmgcdlem  12585  lcm1  12589  3lcm2e6woprm  12594  isprm3  12626  prmgt1  12640  phicl2  12722  phibnd  12725  phi1  12727  dfphi2  12728  phimullem  12733  eulerthlemrprm  12737  eulerthlema  12738  eulerthlemth  12740  fermltl  12742  prmdiv  12743  prmdiveq  12744  odzcllem  12751  odzdvds  12754  oddprm  12768  pythagtriplem4  12777  pcpre1  12801  pc1  12814  pcrec  12817  pcmpt  12852  fldivp1  12857  expnprm  12862  pockthlem  12865  igz  12883  4sqlem12  12911  4sqlem13m  12912  4sqlem19  12918  ssnnctlemct  13003  mulgm1  13665  mulgp1  13678  mulgneg2  13679  zsubrg  14530  gzsubrg  14531  zringmulg  14547  mulgrhm2  14559  sin2pim  15472  cos2pim  15473  rpcxp1  15558  logbleb  15620  logblt  15621  lgslem2  15665  lgsfcl2  15670  lgsval2lem  15674  lgsmod  15690  lgsdir2lem1  15692  lgsdir2lem5  15696  lgsdir  15699  lgsne0  15702  1lgs  15707  lgsdinn0  15712  gausslemma2dlem0i  15721  gausslemma2d  15733  lgseisen  15738  lgsquad2lem2  15746  m1lgs  15749  2lgs  15768  2sqlem9  15788  2sqlem10  15789  ex-fl  16019  apdiff  16347  iswomni0  16350  nconstwlpolem0  16362