Theorem nnz 9453

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9098  ℤcz 9434

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 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-addcom 8087  ax-addass 8089  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-0id 8095  ax-rnegex 8096  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-ltwlin 8100  ax-pre-lttrn 8101  ax-pre-ltadd 8103

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 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-pnf 8171  df-mnf 8172  df-xr 8173  df-ltxr 8174  df-le 8175  df-sub 8307  df-neg 8308  df-inn 9099  df-z 9435

This theorem is referenced by:  elnnz1  9457  znegcl  9465  nnnle0  9483  nnleltp1  9494  nnltp1le  9495  elz2  9506  nnlem1lt  9519  nnltlem1  9520  nnm1ge0  9521  prime  9534  nneo  9538  zeo  9540  btwnz  9554  indstr  9776  eluz2b2  9786  elnn1uz2  9790  qaddcl  9818  qreccl  9825  elpqb  9833  elfz1end  10239  fznatpl1  10260  fznn  10273  elfz1b  10274  elfzo0  10370  fzo1fzo0n0  10371  elfzo0z  10372  elfzo1  10378  ubmelm1fzo  10419  intfracq  10529  zmodcl  10553  zmodfz  10555  zmodfzo  10556  zmodid2  10561  zmodidfzo  10562  modfzo0difsn  10604  mulexpzap  10788  nnesq  10868  expnlbnd  10873  expnlbnd2  10874  nn0ltexp2  10918  facdiv  10947  faclbnd  10950  bc0k  10965  bcval5  10972  seq3coll  11051  ccatval21sw  11126  caucvgrelemcau  11477  resqrexlemlo  11510  resqrexlemcalc3  11513  resqrexlemgt0  11517  absexpzap  11577  climuni  11790  fsum3  11884  arisum  11995  trireciplem  11997  expcnvap0  11999  geo2sum  12011  geo2lim  12013  0.999...  12018  geoihalfsum  12019  cvgratz  12029  zproddc  12076  fprodseq  12080  prod1dc  12083  dvdsval3  12288  nndivdvds  12293  modmulconst  12320  dvdsle  12341  dvdsssfz1  12349  fzm1ndvds  12353  dvdsfac  12357  oexpneg  12374  nnoddm1d2  12407  divalg2  12423  divalgmod  12424  modremain  12426  ndvdsadd  12428  nndvdslegcd  12472  divgcdz  12478  divgcdnn  12482  divgcdnnr  12483  modgcd  12498  gcddiv  12526  gcdmultiple  12527  gcdmultiplez  12528  gcdzeq  12529  gcdeq  12530  rpmulgcd  12533  rplpwr  12534  rppwr  12535  sqgcd  12536  dvdssqlem  12537  dvdssq  12538  eucalginv  12564  lcmgcdlem  12585  lcmgcdnn  12590  lcmass  12593  coprmgcdb  12596  qredeq  12604  qredeu  12605  cncongr1  12611  cncongr2  12612  1idssfct  12623  isprm2lem  12624  isprm3  12626  isprm4  12627  prmind2  12628  prmdc  12638  divgcdodd  12651  isprm6  12655  sqrt2irr  12670  pw2dvds  12674  sqrt2irraplemnn  12687  divnumden  12704  divdenle  12705  nn0gcdsq  12708  phivalfi  12720  phicl2  12722  phiprmpw  12730  hashgcdlem  12746  dvdsfi  12747  hashgcdeq  12748  phisum  12749  nnoddn2prm  12769  pythagtriplem2  12775  pythagtriplem3  12776  pythagtriplem4  12777  pythagtriplem6  12779  pythagtriplem7  12780  pythagtriplem8  12781  pythagtriplem9  12782  pythagtriplem11  12783  pythagtriplem13  12785  pythagtriplem15  12787  pythagtriplem19  12791  pythagtrip  12792  pceu  12804  pccl  12808  pcdiv  12811  pcqcl  12815  pcdvds  12824  pcndvds  12826  pcndvds2  12828  pcelnn  12830  pcz  12841  pcmpt  12852  fldivp1  12857  pcfac  12859  infpnlem1  12868  infpnlem2  12869  prmunb  12871  1arith  12876  oddennn  12949  evenennn  12950  unennn  12954  mulgnn  13649  mulgnngsum  13650  mulgaddcom  13669  mulginvcom  13670  mulgmodid  13684  ghmmulg  13779  mulgass2  14007  znfi  14604  znhash  14605  znidomb  14607  znrrg  14609  rpcxproot  15573  logbgcd1irr  15626  sgmnncl  15647  lgsval  15668  lgsval4a  15686  lgssq2  15705  gausslemma2dlem0c  15715  gausslemma2dlem0e  15717  gausslemma2dlem1a  15722  gausslemma2dlem3  15727  gausslemma2dlem5  15730  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad3  15748  2lgslem1a1  15750  2lgslem3  15765  2lgsoddprm  15777  trilpolemcl  16336