Theorem nnz 9616

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℕcn 9257  ℤcz 9597

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-addcom 8243  ax-addass 8245  ax-distr 8247  ax-i2m1 8248  ax-0lt1 8249  ax-0id 8251  ax-rnegex 8252  ax-cnre 8254  ax-pre-ltirr 8255  ax-pre-ltwlin 8256  ax-pre-lttrn 8257  ax-pre-ltadd 8259

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-opab 4177  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365  df-riota 6011  df-ov 6061  df-oprab 6062  df-mpo 6063  df-pnf 8326  df-mnf 8327  df-xr 8328  df-ltxr 8329  df-le 8330  df-sub 8463  df-neg 8464  df-inn 9258  df-z 9598

This theorem is referenced by:  elnnz1  9620  znegcl  9628  nnnle0  9646  nnleltp1  9657  nnltp1le  9658  elz2  9669  nnlem1lt  9683  nnltlem1  9684  nnm1ge0  9685  prime  9698  nneo  9702  zeo  9704  btwnz  9718  indstr  9946  eluz2b2  9956  elnn1uz2  9960  qaddcl  9988  qreccl  9995  elpqb  10003  elfz1end  10413  fznatpl1  10435  fznn  10448  elfz1b  10449  elfzo0  10545  fzo1fzo0n0  10547  elfzo0z  10548  elfzo1  10555  ubmelm1fzo  10596  intfracq  10709  zmodcl  10733  zmodfz  10735  zmodfzo  10736  zmodid2  10741  zmodidfzo  10742  modfzo0difsn  10784  mulexpzap  10968  nnesq  11049  expnlbnd  11054  expnlbnd2  11055  nn0ltexp2  11099  facdiv  11128  faclbnd  11131  bc0k  11146  bcval5  11153  bcm1n  11159  seq3coll  11242  ccatval21sw  11321  caucvgrelemcau  11694  resqrexlemlo  11727  resqrexlemcalc3  11730  resqrexlemgt0  11734  absexpzap  11794  climuni  12007  fsum3  12102  arisum  12213  trireciplem  12215  expcnvap0  12217  geo2sum  12229  geo2lim  12231  0.999...  12236  geoihalfsum  12237  cvgratz  12247  zproddc  12294  fprodseq  12298  prod1dc  12301  dvdsval3  12506  nndivdvds  12511  modmulconst  12538  dvdsle  12559  dvdsssfz1  12567  fzm1ndvds  12571  dvdsfac  12575  oexpneg  12592  nnoddm1d2  12625  divalg2  12641  divalgmod  12642  modremain  12644  ndvdsadd  12646  nndvdslegcd  12690  divgcdz  12696  divgcdnn  12700  divgcdnnr  12701  modgcd  12716  gcddiv  12744  gcdmultiple  12745  gcdmultiplez  12746  gcdzeq  12747  gcdeq  12748  rpmulgcd  12751  rplpwr  12752  rppwr  12753  sqgcd  12754  dvdssqlem  12755  dvdssq  12756  eucalginv  12782  lcmgcdlem  12803  lcmgcdnn  12808  lcmass  12811  coprmgcdb  12814  qredeq  12822  qredeu  12823  cncongr1  12829  cncongr2  12830  1idssfct  12841  isprm2lem  12842  isprm3  12844  isprm4  12845  prmind2  12846  prmdc  12856  divgcdodd  12869  isprm6  12873  sqrt2irr  12888  pw2dvds  12892  sqrt2irraplemnn  12905  divnumden  12922  divdenle  12923  nn0gcdsq  12926  phivalfi  12938  phicl2  12940  phiprmpw  12948  hashgcdlem  12964  dvdsfi  12965  hashgcdeq  12966  phisum  12967  nnoddn2prm  12987  pythagtriplem2  12993  pythagtriplem3  12994  pythagtriplem4  12995  pythagtriplem6  12997  pythagtriplem7  12998  pythagtriplem8  12999  pythagtriplem9  13000  pythagtriplem11  13001  pythagtriplem13  13003  pythagtriplem15  13005  pythagtriplem19  13009  pythagtrip  13010  pceu  13022  pccl  13026  pcdiv  13029  pcqcl  13033  pcdvds  13042  pcndvds  13044  pcndvds2  13046  pcelnn  13048  pcz  13059  pcmpt  13070  fldivp1  13075  pcfac  13077  infpnlem1  13086  infpnlem2  13087  prmunb  13089  1arith  13094  ballotfilemiex  13192  oddennn  13231  evenennn  13232  unennn  13236  mulgnn  13883  mulgnngsum  13884  mulgaddcom  13903  mulginvcom  13904  mulgmodid  13918  ghmmulg  14013  mulgass2  14305  znfi  14933  znhash  14934  znidomb  14936  znrrg  14938  rpcxproot  15909  logbgcd1irr  15962  sgmnncl  15986  lgsval  16007  lgsval4a  16025  lgssq2  16044  gausslemma2dlem0c  16054  gausslemma2dlem0e  16056  gausslemma2dlem1a  16061  gausslemma2dlem3  16066  gausslemma2dlem5  16069  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad3  16087  2lgslem1a1  16089  2lgslem3  16104  2lgsoddprm  16116  trilpolemcl  16961