Theorem nn0z 9187

Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0z	⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Proof of Theorem nn0z

Step	Hyp	Ref	Expression
1		nn0ssz 9185	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3124	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2128  ℕ₀cn0 9090  ℤcz 9167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-cnex 7823  ax-resscn 7824  ax-1cn 7825  ax-1re 7826  ax-icn 7827  ax-addcl 7828  ax-addrcl 7829  ax-mulcl 7830  ax-addcom 7832  ax-addass 7834  ax-distr 7836  ax-i2m1 7837  ax-0lt1 7838  ax-0id 7840  ax-rnegex 7841  ax-cnre 7843  ax-pre-ltirr 7844  ax-pre-ltwlin 7845  ax-pre-lttrn 7846  ax-pre-ltadd 7848

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-id 4253  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-iota 5135  df-fun 5172  df-fv 5178  df-riota 5780  df-ov 5827  df-oprab 5828  df-mpo 5829  df-pnf 7914  df-mnf 7915  df-xr 7916  df-ltxr 7917  df-le 7918  df-sub 8048  df-neg 8049  df-inn 8834  df-n0 9091  df-z 9168

This theorem is referenced by:  nn0negz  9201  nn0ltp1le  9229  nn0leltp1  9230  nn0ltlem1  9231  nn0sub  9233  nn0n0n1ge2b  9243  nn0lt10b  9244  nn0lt2  9245  nn0le2is012  9246  nn0lem1lt  9247  fnn0ind  9280  nn0pzuz  9498  nn01to3  9526  nn0ge2m1nnALT  9527  fz1n  9946  ige2m1fz  10012  elfz2nn0  10014  fznn0  10015  elfz0add  10022  fzctr  10032  difelfzle  10033  fzo1fzo0n0  10082  fzofzim  10087  elfzodifsumelfzo  10100  zpnn0elfzo  10106  fzossfzop1  10111  ubmelm1fzo  10125  adddivflid  10191  fldivnn0  10194  divfl0  10195  flqmulnn0  10198  fldivnn0le  10202  zmodidfzoimp  10253  modqmuladdnn0  10267  modifeq2int  10285  modfzo0difsn  10294  uzennn  10335  expdivap  10470  faclbnd3  10617  bccmpl  10628  bcnp1n  10633  bcn2  10638  bcp1m1  10639  modfsummodlemstep  11354  bcxmas  11386  geo2sum2  11412  mertenslemi1  11432  mertensabs  11434  esum  11559  efcvgfsum  11564  ege2le3  11568  eftlcl  11585  reeftlcl  11586  eftlub  11587  effsumlt  11589  eirraplem  11673  dvds1  11744  dvdsext  11746  addmodlteqALT  11750  oddnn02np1  11770  oddge22np1  11771  nn0ehalf  11793  nn0o1gt2  11795  nno  11796  nn0o  11797  nn0oddm1d2  11799  modremain  11819  gcdn0gt0  11861  nn0gcdid0  11864  bezoutlemmain  11881  nn0seqcvgd  11917  algcvgblem  11925  algcvga  11927  eucalgf  11931  prmndvdsfaclt  12030  nn0sqrtelqelz  12080  nonsq  12081  crth  12098  odzdvds  12119