Theorem 1z 9411

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

Syntax hints:   ∈ wcel 2177  1c1 7939  ℤcz 9385

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258  ax-un 4485  ax-setind 4590  ax-cnex 8029  ax-resscn 8030  ax-1cn 8031  ax-1re 8032  ax-icn 8033  ax-addcl 8034  ax-addrcl 8035  ax-mulcl 8036  ax-addcom 8038  ax-addass 8040  ax-distr 8042  ax-i2m1 8043  ax-0lt1 8044  ax-0id 8046  ax-rnegex 8047  ax-cnre 8049  ax-pre-ltirr 8050  ax-pre-ltwlin 8051  ax-pre-lttrn 8052  ax-pre-ltadd 8054

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3001  df-dif 3170  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-int 3889  df-br 4049  df-opab 4111  df-id 4345  df-xp 4686  df-rel 4687  df-cnv 4688  df-co 4689  df-dm 4690  df-iota 5238  df-fun 5279  df-fv 5285  df-riota 5909  df-ov 5957  df-oprab 5958  df-mpo 5959  df-pnf 8122  df-mnf 8123  df-xr 8124  df-ltxr 8125  df-le 8126  df-sub 8258  df-neg 8259  df-inn 9050  df-z 9386

This theorem is referenced by:  1zzd  9412  znnnlt1  9433  nn0n0n1ge2b  9465  nn0lt2  9467  nn0le2is012  9468  3halfnz  9483  prime  9485  nnuz  9697  eluz2nn  9700  eluzge3nn  9706  1eluzge0  9708  2eluzge1  9710  eluz2b1  9735  uz2m1nn  9739  elnn1uz2  9741  elnndc  9746  nn01to3  9751  nnrecq  9779  fz1n  10179  fz10  10181  fz01en  10188  fzpreddisj  10206  fznatpl1  10211  fzprval  10217  fztpval  10218  fseq1p1m1  10229  elfzp1b  10232  elfzm1b  10233  4fvwrd4  10275  ige2m2fzo  10340  fzo12sn  10359  fzofzp1  10369  fzostep1  10379  rebtwn2zlemstep  10408  qbtwnxr  10413  flqge1nn  10450  fldiv4p1lem1div2  10461  fldiv4lem1div2  10463  modqfrac  10495  modqid0  10508  q1mod  10514  mulp1mod1  10523  m1modnnsub1  10528  modqm1p1mod0  10533  modqltm1p1mod  10534  frecfzennn  10584  frecfzen2  10585  zexpcl  10712  qexpcl  10713  qexpclz  10718  m1expcl  10720  expp1zap  10746  expm1ap  10747  bcn1  10916  bcpasc  10924  bcnm1  10930  isfinite4im  10950  hashsng  10956  hashfz  10979  climuni  11654  sum0  11749  sumsnf  11770  expcnv  11865  cvgratz  11893  prod0  11946  prodsnf  11953  sinltxirr  12122  sin01gt0  12123  p1modz1  12155  iddvds  12165  1dvds  12166  dvds1  12214  3dvds  12225  nn0o1gt2  12266  n2dvds1  12273  bitsp1o  12314  bitsfzo  12316  gcdadd  12356  gcdid  12357  gcd1  12358  1gcd  12363  bezoutlema  12370  bezoutlemb  12371  gcdmultiple  12391  lcmgcdlem  12449  lcm1  12453  3lcm2e6woprm  12458  isprm3  12490  prmgt1  12504  phicl2  12586  phibnd  12589  phi1  12591  dfphi2  12592  phimullem  12597  eulerthlemrprm  12601  eulerthlema  12602  eulerthlemth  12604  fermltl  12606  prmdiv  12607  prmdiveq  12608  odzcllem  12615  odzdvds  12618  oddprm  12632  pythagtriplem4  12641  pcpre1  12665  pc1  12678  pcrec  12681  pcmpt  12716  fldivp1  12721  expnprm  12726  pockthlem  12729  igz  12747  4sqlem12  12775  4sqlem13m  12776  4sqlem19  12782  ssnnctlemct  12867  mulgm1  13528  mulgp1  13541  mulgneg2  13542  zsubrg  14393  gzsubrg  14394  zringmulg  14410  mulgrhm2  14422  sin2pim  15335  cos2pim  15336  rpcxp1  15421  logbleb  15483  logblt  15484  lgslem2  15528  lgsfcl2  15533  lgsval2lem  15537  lgsmod  15553  lgsdir2lem1  15555  lgsdir2lem5  15559  lgsdir  15562  lgsne0  15565  1lgs  15570  lgsdinn0  15575  gausslemma2dlem0i  15584  gausslemma2d  15596  lgseisen  15601  lgsquad2lem2  15609  m1lgs  15612  2lgs  15631  2sqlem9  15651  2sqlem10  15652  ex-fl  15775  apdiff  16102  iswomni0  16105  nconstwlpolem0  16117