Theorem nn0z 9482

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕ₀cn0 9385  ℤcz 9462

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 4202  ax-pow 4259  ax-pr 4294  ax-un 4525  ax-setind 4630  ax-cnex 8106  ax-resscn 8107  ax-1cn 8108  ax-1re 8109  ax-icn 8110  ax-addcl 8111  ax-addrcl 8112  ax-mulcl 8113  ax-addcom 8115  ax-addass 8117  ax-distr 8119  ax-i2m1 8120  ax-0lt1 8121  ax-0id 8123  ax-rnegex 8124  ax-cnre 8126  ax-pre-ltirr 8127  ax-pre-ltwlin 8128  ax-pre-lttrn 8129  ax-pre-ltadd 8131

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 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-iota 5281  df-fun 5323  df-fv 5329  df-riota 5963  df-ov 6013  df-oprab 6014  df-mpo 6015  df-pnf 8199  df-mnf 8200  df-xr 8201  df-ltxr 8202  df-le 8203  df-sub 8335  df-neg 8336  df-inn 9127  df-n0 9386  df-z 9463

This theorem is referenced by:  nn0negz  9496  nn0ltp1le  9525  nn0leltp1  9526  nn0ltlem1  9527  nn0sub  9529  nn0n0n1ge2b  9542  nn0lt10b  9543  nn0lt2  9544  nn0le2is012  9545  nn0lem1lt  9546  fnn0ind  9579  nn0pzuz  9799  nn01to3  9829  nn0ge2m1nnALT  9830  fz1n  10257  ige2m1fz  10323  elfz2nn0  10325  fznn0  10326  elfz0add  10333  fzctr  10346  difelfzle  10347  fzoun  10396  fzo1fzo0n0  10400  fzofzim  10405  elincfzoext  10416  elfzodifsumelfzo  10424  zpnn0elfzo  10430  fzossfzop1  10435  ubmelm1fzo  10449  adddivflid  10529  fldivnn0  10532  divfl0  10533  flqmulnn0  10536  fldivnn0le  10540  zmodidfzoimp  10593  modqmuladdnn0  10607  modifeq2int  10625  modfzo0difsn  10634  uzennn  10675  expdivap  10829  faclbnd3  10982  bccmpl  10993  bcnp1n  10998  bcn2  11003  bcp1m1  11004  iswrd  11091  wrdval  11092  wrdexg  11100  ffz0iswrdnn0  11116  wrdnval  11120  wrdred1  11132  wrdred1hash  11133  ccatalpha  11166  swrdfv2  11216  swrdsb0eq  11218  swrdsbslen  11219  swrdspsleq  11220  swrdlsw  11222  pfx0g  11229  fnpfx  11230  pfxclg  11231  pfxnd  11242  pfxwrdsymbg  11243  pfxccatin12lem4  11279  pfxccatin12lem3  11285  pfxccat3  11287  swrdccat  11288  pfxccat3a  11291  cats1fvd  11319  nn0maxcl  11757  modfsummodlemstep  11989  bcxmas  12021  geo2sum2  12047  mertenslemi1  12067  mertensabs  12069  esum  12194  efcvgfsum  12199  ege2le3  12203  eftlcl  12220  reeftlcl  12221  eftlub  12222  effsumlt  12224  eirraplem  12309  dvds1  12385  dvdsext  12387  addmodlteqALT  12391  3dvds  12396  oddnn02np1  12412  oddge22np1  12413  nn0ehalf  12435  nn0o1gt2  12437  nno  12438  nn0o  12439  nn0oddm1d2  12441  modremain  12461  bitsmod  12488  bitsinv1  12494  gcdn0gt0  12520  nn0gcdid0  12523  bezoutlemmain  12540  nn0seqcvgd  12584  algcvgblem  12592  algcvga  12594  eucalgf  12598  prmndvdsfaclt  12699  nn0sqrtelqelz  12749  nonsq  12750  crth  12767  odzdvds  12789  coprimeprodsq  12801  coprimeprodsq2  12802  oddprm  12803  pcexp  12853  pcdvdsb  12864  pc11  12875  dvdsprmpweqle  12881  difsqpwdvds  12882  pcfac  12894  prmunb  12906  4sqexercise1  12942  4sqexercise2  12943  4sqlemsdc  12944  modxai  12960  mulgaddcom  13704  mulginvcom  13705  mulgz  13708  mulgdirlem  13711  mulgass  13717  mulgass2  14042  zncrng  14630  znzrh2  14631  zndvds  14634  znf1o  14636  znunit  14644  elply2  15430  elplyd  15436  dvply2g  15461  sgmnncl  15683  0sgmppw  15688  lgsneg1  15725  lgsdirnn0  15747  lgsdinn0  15748  2lgslem1c  15790  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgsoddprmlem2  15806  wlkv0  16141