Theorem nnz 9473

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9118  ℤcz 9454

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 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-addcom 8107  ax-addass 8109  ax-distr 8111  ax-i2m1 8112  ax-0lt1 8113  ax-0id 8115  ax-rnegex 8116  ax-cnre 8118  ax-pre-ltirr 8119  ax-pre-ltwlin 8120  ax-pre-lttrn 8121  ax-pre-ltadd 8123

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 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8191  df-mnf 8192  df-xr 8193  df-ltxr 8194  df-le 8195  df-sub 8327  df-neg 8328  df-inn 9119  df-z 9455

This theorem is referenced by:  elnnz1  9477  znegcl  9485  nnnle0  9503  nnleltp1  9514  nnltp1le  9515  elz2  9526  nnlem1lt  9539  nnltlem1  9540  nnm1ge0  9541  prime  9554  nneo  9558  zeo  9560  btwnz  9574  indstr  9796  eluz2b2  9806  elnn1uz2  9810  qaddcl  9838  qreccl  9845  elpqb  9853  elfz1end  10259  fznatpl1  10280  fznn  10293  elfz1b  10294  elfzo0  10390  fzo1fzo0n0  10391  elfzo0z  10392  elfzo1  10399  ubmelm1fzo  10440  intfracq  10550  zmodcl  10574  zmodfz  10576  zmodfzo  10577  zmodid2  10582  zmodidfzo  10583  modfzo0difsn  10625  mulexpzap  10809  nnesq  10889  expnlbnd  10894  expnlbnd2  10895  nn0ltexp2  10939  facdiv  10968  faclbnd  10971  bc0k  10986  bcval5  10993  seq3coll  11072  ccatval21sw  11148  caucvgrelemcau  11499  resqrexlemlo  11532  resqrexlemcalc3  11535  resqrexlemgt0  11539  absexpzap  11599  climuni  11812  fsum3  11906  arisum  12017  trireciplem  12019  expcnvap0  12021  geo2sum  12033  geo2lim  12035  0.999...  12040  geoihalfsum  12041  cvgratz  12051  zproddc  12098  fprodseq  12102  prod1dc  12105  dvdsval3  12310  nndivdvds  12315  modmulconst  12342  dvdsle  12363  dvdsssfz1  12371  fzm1ndvds  12375  dvdsfac  12379  oexpneg  12396  nnoddm1d2  12429  divalg2  12445  divalgmod  12446  modremain  12448  ndvdsadd  12450  nndvdslegcd  12494  divgcdz  12500  divgcdnn  12504  divgcdnnr  12505  modgcd  12520  gcddiv  12548  gcdmultiple  12549  gcdmultiplez  12550  gcdzeq  12551  gcdeq  12552  rpmulgcd  12555  rplpwr  12556  rppwr  12557  sqgcd  12558  dvdssqlem  12559  dvdssq  12560  eucalginv  12586  lcmgcdlem  12607  lcmgcdnn  12612  lcmass  12615  coprmgcdb  12618  qredeq  12626  qredeu  12627  cncongr1  12633  cncongr2  12634  1idssfct  12645  isprm2lem  12646  isprm3  12648  isprm4  12649  prmind2  12650  prmdc  12660  divgcdodd  12673  isprm6  12677  sqrt2irr  12692  pw2dvds  12696  sqrt2irraplemnn  12709  divnumden  12726  divdenle  12727  nn0gcdsq  12730  phivalfi  12742  phicl2  12744  phiprmpw  12752  hashgcdlem  12768  dvdsfi  12769  hashgcdeq  12770  phisum  12771  nnoddn2prm  12791  pythagtriplem2  12797  pythagtriplem3  12798  pythagtriplem4  12799  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem8  12803  pythagtriplem9  12804  pythagtriplem11  12805  pythagtriplem13  12807  pythagtriplem15  12809  pythagtriplem19  12813  pythagtrip  12814  pceu  12826  pccl  12830  pcdiv  12833  pcqcl  12837  pcdvds  12846  pcndvds  12848  pcndvds2  12850  pcelnn  12852  pcz  12863  pcmpt  12874  fldivp1  12879  pcfac  12881  infpnlem1  12890  infpnlem2  12891  prmunb  12893  1arith  12898  oddennn  12971  evenennn  12972  unennn  12976  mulgnn  13671  mulgnngsum  13672  mulgaddcom  13691  mulginvcom  13692  mulgmodid  13706  ghmmulg  13801  mulgass2  14029  znfi  14627  znhash  14628  znidomb  14630  znrrg  14632  rpcxproot  15596  logbgcd1irr  15649  sgmnncl  15670  lgsval  15691  lgsval4a  15709  lgssq2  15728  gausslemma2dlem0c  15738  gausslemma2dlem0e  15740  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  gausslemma2dlem5  15753  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad3  15771  2lgslem1a1  15773  2lgslem3  15788  2lgsoddprm  15800  trilpolemcl  16435