Theorem nnz 9491

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

Assertion

Ref	Expression
nnz	⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnssz 9489	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3221	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9136  ℤcz 9472

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 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-1re 8119  ax-icn 8120  ax-addcl 8121  ax-addrcl 8122  ax-mulcl 8123  ax-addcom 8125  ax-addass 8127  ax-distr 8129  ax-i2m1 8130  ax-0lt1 8131  ax-0id 8133  ax-rnegex 8134  ax-cnre 8136  ax-pre-ltirr 8137  ax-pre-ltwlin 8138  ax-pre-lttrn 8139  ax-pre-ltadd 8141

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 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8209  df-mnf 8210  df-xr 8211  df-ltxr 8212  df-le 8213  df-sub 8345  df-neg 8346  df-inn 9137  df-z 9473

This theorem is referenced by:  elnnz1  9495  znegcl  9503  nnnle0  9521  nnleltp1  9532  nnltp1le  9533  elz2  9544  nnlem1lt  9557  nnltlem1  9558  nnm1ge0  9559  prime  9572  nneo  9576  zeo  9578  btwnz  9592  indstr  9820  eluz2b2  9830  elnn1uz2  9834  qaddcl  9862  qreccl  9869  elpqb  9877  elfz1end  10283  fznatpl1  10304  fznn  10317  elfz1b  10318  elfzo0  10414  fzo1fzo0n0  10415  elfzo0z  10416  elfzo1  10423  ubmelm1fzo  10464  intfracq  10575  zmodcl  10599  zmodfz  10601  zmodfzo  10602  zmodid2  10607  zmodidfzo  10608  modfzo0difsn  10650  mulexpzap  10834  nnesq  10914  expnlbnd  10919  expnlbnd2  10920  nn0ltexp2  10964  facdiv  10993  faclbnd  10996  bc0k  11011  bcval5  11018  seq3coll  11099  ccatval21sw  11175  caucvgrelemcau  11534  resqrexlemlo  11567  resqrexlemcalc3  11570  resqrexlemgt0  11574  absexpzap  11634  climuni  11847  fsum3  11941  arisum  12052  trireciplem  12054  expcnvap0  12056  geo2sum  12068  geo2lim  12070  0.999...  12075  geoihalfsum  12076  cvgratz  12086  zproddc  12133  fprodseq  12137  prod1dc  12140  dvdsval3  12345  nndivdvds  12350  modmulconst  12377  dvdsle  12398  dvdsssfz1  12406  fzm1ndvds  12410  dvdsfac  12414  oexpneg  12431  nnoddm1d2  12464  divalg2  12480  divalgmod  12481  modremain  12483  ndvdsadd  12485  nndvdslegcd  12529  divgcdz  12535  divgcdnn  12539  divgcdnnr  12540  modgcd  12555  gcddiv  12583  gcdmultiple  12584  gcdmultiplez  12585  gcdzeq  12586  gcdeq  12587  rpmulgcd  12590  rplpwr  12591  rppwr  12592  sqgcd  12593  dvdssqlem  12594  dvdssq  12595  eucalginv  12621  lcmgcdlem  12642  lcmgcdnn  12647  lcmass  12650  coprmgcdb  12653  qredeq  12661  qredeu  12662  cncongr1  12668  cncongr2  12669  1idssfct  12680  isprm2lem  12681  isprm3  12683  isprm4  12684  prmind2  12685  prmdc  12695  divgcdodd  12708  isprm6  12712  sqrt2irr  12727  pw2dvds  12731  sqrt2irraplemnn  12744  divnumden  12761  divdenle  12762  nn0gcdsq  12765  phivalfi  12777  phicl2  12779  phiprmpw  12787  hashgcdlem  12803  dvdsfi  12804  hashgcdeq  12805  phisum  12806  nnoddn2prm  12826  pythagtriplem2  12832  pythagtriplem3  12833  pythagtriplem4  12834  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem8  12838  pythagtriplem9  12839  pythagtriplem11  12840  pythagtriplem13  12842  pythagtriplem15  12844  pythagtriplem19  12848  pythagtrip  12849  pceu  12861  pccl  12865  pcdiv  12868  pcqcl  12872  pcdvds  12881  pcndvds  12883  pcndvds2  12885  pcelnn  12887  pcz  12898  pcmpt  12909  fldivp1  12914  pcfac  12916  infpnlem1  12925  infpnlem2  12926  prmunb  12928  1arith  12933  oddennn  13006  evenennn  13007  unennn  13011  mulgnn  13706  mulgnngsum  13707  mulgaddcom  13726  mulginvcom  13727  mulgmodid  13741  ghmmulg  13836  mulgass2  14064  znfi  14662  znhash  14663  znidomb  14665  znrrg  14667  rpcxproot  15631  logbgcd1irr  15684  sgmnncl  15705  lgsval  15726  lgsval4a  15744  lgssq2  15763  gausslemma2dlem0c  15773  gausslemma2dlem0e  15775  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  gausslemma2dlem5  15788  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad3  15806  2lgslem1a1  15808  2lgslem3  15823  2lgsoddprm  15835  trilpolemcl  16591