Theorem nn0z 9405

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℕ₀cn0 9308  ℤ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-n0 9309  df-z 9386

This theorem is referenced by:  nn0negz  9419  nn0ltp1le  9448  nn0leltp1  9449  nn0ltlem1  9450  nn0sub  9452  nn0n0n1ge2b  9465  nn0lt10b  9466  nn0lt2  9467  nn0le2is012  9468  nn0lem1lt  9469  fnn0ind  9502  nn0pzuz  9721  nn01to3  9751  nn0ge2m1nnALT  9752  fz1n  10179  ige2m1fz  10245  elfz2nn0  10247  fznn0  10248  elfz0add  10255  fzctr  10268  difelfzle  10269  fzo1fzo0n0  10320  fzofzim  10325  elincfzoext  10335  elfzodifsumelfzo  10343  zpnn0elfzo  10349  fzossfzop1  10354  ubmelm1fzo  10368  adddivflid  10448  fldivnn0  10451  divfl0  10452  flqmulnn0  10455  fldivnn0le  10459  zmodidfzoimp  10512  modqmuladdnn0  10526  modifeq2int  10544  modfzo0difsn  10553  uzennn  10594  expdivap  10748  faclbnd3  10901  bccmpl  10912  bcnp1n  10917  bcn2  10922  bcp1m1  10923  iswrd  11009  wrdval  11010  wrdexg  11018  wrdnval  11037  wrdred1  11049  wrdred1hash  11050  swrdfv2  11130  swrdsb0eq  11132  swrdsbslen  11133  swrdspsleq  11134  swrdlsw  11136  pfx0g  11143  pfxclg  11144  pfxnd  11154  pfxwrdsymbg  11155  nn0maxcl  11586  modfsummodlemstep  11818  bcxmas  11850  geo2sum2  11876  mertenslemi1  11896  mertensabs  11898  esum  12023  efcvgfsum  12028  ege2le3  12032  eftlcl  12049  reeftlcl  12050  eftlub  12051  effsumlt  12053  eirraplem  12138  dvds1  12214  dvdsext  12216  addmodlteqALT  12220  3dvds  12225  oddnn02np1  12241  oddge22np1  12242  nn0ehalf  12264  nn0o1gt2  12266  nno  12267  nn0o  12268  nn0oddm1d2  12270  modremain  12290  bitsmod  12317  bitsinv1  12323  gcdn0gt0  12349  nn0gcdid0  12352  bezoutlemmain  12369  nn0seqcvgd  12413  algcvgblem  12421  algcvga  12423  eucalgf  12427  prmndvdsfaclt  12528  nn0sqrtelqelz  12578  nonsq  12579  crth  12596  odzdvds  12618  coprimeprodsq  12630  coprimeprodsq2  12631  oddprm  12632  pcexp  12682  pcdvdsb  12693  pc11  12704  dvdsprmpweqle  12710  difsqpwdvds  12711  pcfac  12723  prmunb  12735  4sqexercise1  12771  4sqexercise2  12772  4sqlemsdc  12773  modxai  12789  mulgaddcom  13532  mulginvcom  13533  mulgz  13536  mulgdirlem  13539  mulgass  13545  mulgass2  13870  zncrng  14457  znzrh2  14458  zndvds  14461  znf1o  14463  znunit  14471  elply2  15257  elplyd  15263  dvply2g  15288  sgmnncl  15510  0sgmppw  15515  lgsneg1  15552  lgsdirnn0  15574  lgsdinn0  15575  2lgslem1c  15617  2lgslem3a1  15624  2lgslem3b1  15625  2lgslem3c1  15626  2lgsoddprmlem2  15633