Theorem nn0z 8868

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 8866	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3035	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1445  ℕ₀cn0 8771  ℤcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0lt1 7548  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltirr 7554  ax-pre-ltwlin 7555  ax-pre-lttrn 7556  ax-pre-ltadd 7558

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-opab 3922  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-sub 7752  df-neg 7753  df-inn 8521  df-n0 8772  df-z 8849

This theorem is referenced by:  nn0negz  8882  nn0ltp1le  8910  nn0leltp1  8911  nn0ltlem1  8912  nn0sub  8914  nn0n0n1ge2b  8924  nn0lt10b  8925  nn0lt2  8926  nn0le2is012  8927  nn0lem1lt  8928  fnn0ind  8961  nn0pzuz  9174  nn01to3  9201  nn0ge2m1nnALT  9202  fz1n  9607  ige2m1fz  9673  elfz2nn0  9675  fznn0  9676  elfz0add  9683  fzctr  9693  difelfzle  9694  fzo1fzo0n0  9743  fzofzim  9748  elfzodifsumelfzo  9761  zpnn0elfzo  9767  fzossfzop1  9772  ubmelm1fzo  9786  adddivflid  9848  fldivnn0  9851  divfl0  9852  flqmulnn0  9855  fldivnn0le  9859  zmodidfzoimp  9910  modqmuladdnn0  9924  modifeq2int  9942  modfzo0difsn  9951  expdivap  10137  faclbnd3  10282  bccmpl  10293  bcnp1n  10298  bcn2  10303  bcp1m1  10304  modfsummodlemstep  11015  bcxmas  11047  geo2sum2  11073  mertenslemi1  11093  mertensabs  11095  esum  11116  efcvgfsum  11121  ege2le3  11125  eftlcl  11142  reeftlcl  11143  eftlub  11144  effsumlt  11146  eirraplem  11228  dvds1  11296  dvdsext  11298  addmodlteqALT  11302  oddnn02np1  11322  oddge22np1  11323  nn0ehalf  11345  nn0o1gt2  11347  nno  11348  nn0o  11349  nn0oddm1d2  11351  modremain  11371  gcdn0gt0  11411  nn0gcdid0  11414  bezoutlemmain  11429  nn0seqcvgd  11465  algcvgblem  11473  algcvga  11475  eucalgf  11479  prmndvdsfaclt  11577  nn0sqrtelqelz  11626  nonsq  11627  crth  11642