Theorem 1z 9369

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

Syntax hints:   ∈ wcel 2167  1c1 7897  ℤcz 9343

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 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-0id 8004  ax-rnegex 8005  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-ltadd 8012

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 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-iota 5220  df-fun 5261  df-fv 5267  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-inn 9008  df-z 9344

This theorem is referenced by:  1zzd  9370  znnnlt1  9391  nn0n0n1ge2b  9422  nn0lt2  9424  nn0le2is012  9425  3halfnz  9440  prime  9442  nnuz  9654  eluz2nn  9657  eluzge3nn  9663  1eluzge0  9665  2eluzge1  9667  eluz2b1  9692  uz2m1nn  9696  elnn1uz2  9698  elnndc  9703  nn01to3  9708  nnrecq  9736  fz1n  10136  fz10  10138  fz01en  10145  fzpreddisj  10163  fznatpl1  10168  fzprval  10174  fztpval  10175  fseq1p1m1  10186  elfzp1b  10189  elfzm1b  10190  4fvwrd4  10232  ige2m2fzo  10291  fzo12sn  10310  fzofzp1  10320  fzostep1  10330  rebtwn2zlemstep  10359  qbtwnxr  10364  flqge1nn  10401  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  modqfrac  10446  modqid0  10459  q1mod  10465  mulp1mod1  10474  m1modnnsub1  10479  modqm1p1mod0  10484  modqltm1p1mod  10485  frecfzennn  10535  frecfzen2  10536  zexpcl  10663  qexpcl  10664  qexpclz  10669  m1expcl  10671  expp1zap  10697  expm1ap  10698  bcn1  10867  bcpasc  10875  bcnm1  10881  isfinite4im  10901  hashsng  10907  hashfz  10930  climuni  11475  sum0  11570  sumsnf  11591  expcnv  11686  cvgratz  11714  prod0  11767  prodsnf  11774  sinltxirr  11943  sin01gt0  11944  p1modz1  11976  iddvds  11986  1dvds  11987  dvds1  12035  3dvds  12046  nn0o1gt2  12087  n2dvds1  12094  bitsp1o  12135  bitsfzo  12137  gcdadd  12177  gcdid  12178  gcd1  12179  1gcd  12184  bezoutlema  12191  bezoutlemb  12192  gcdmultiple  12212  lcmgcdlem  12270  lcm1  12274  3lcm2e6woprm  12279  isprm3  12311  prmgt1  12325  phicl2  12407  phibnd  12410  phi1  12412  dfphi2  12413  phimullem  12418  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemth  12425  fermltl  12427  prmdiv  12428  prmdiveq  12429  odzcllem  12436  odzdvds  12439  oddprm  12453  pythagtriplem4  12462  pcpre1  12486  pc1  12499  pcrec  12502  pcmpt  12537  fldivp1  12542  expnprm  12547  pockthlem  12550  igz  12568  4sqlem12  12596  4sqlem13m  12597  4sqlem19  12603  ssnnctlemct  12688  mulgm1  13348  mulgp1  13361  mulgneg2  13362  zsubrg  14213  gzsubrg  14214  zringmulg  14230  mulgrhm2  14242  sin2pim  15133  cos2pim  15134  rpcxp1  15219  logbleb  15281  logblt  15282  lgslem2  15326  lgsfcl2  15331  lgsval2lem  15335  lgsmod  15351  lgsdir2lem1  15353  lgsdir2lem5  15357  lgsdir  15360  lgsne0  15363  1lgs  15368  lgsdinn0  15373  gausslemma2dlem0i  15382  gausslemma2d  15394  lgseisen  15399  lgsquad2lem2  15407  m1lgs  15410  2lgs  15429  2sqlem9  15449  2sqlem10  15450  ex-fl  15455  apdiff  15779  iswomni0  15782  nconstwlpolem0  15794