Theorem nnz 9336

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℕcn 8982  ℤcz 9317

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-ltadd 7988

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-inn 8983  df-z 9318

This theorem is referenced by:  elnnz1  9340  znegcl  9348  nnleltp1  9376  nnltp1le  9377  elz2  9388  nnlem1lt  9401  nnltlem1  9402  nnm1ge0  9403  prime  9416  nneo  9420  zeo  9422  btwnz  9436  indstr  9658  eluz2b2  9668  elnn1uz2  9672  qaddcl  9700  qreccl  9707  elpqb  9715  elfz1end  10121  fznatpl1  10142  fznn  10155  elfz1b  10156  elfzo0  10249  fzo1fzo0n0  10250  elfzo0z  10251  elfzo1  10257  ubmelm1fzo  10293  intfracq  10391  zmodcl  10415  zmodfz  10417  zmodfzo  10418  zmodid2  10423  zmodidfzo  10424  modfzo0difsn  10466  mulexpzap  10650  nnesq  10730  expnlbnd  10735  expnlbnd2  10736  nn0ltexp2  10780  facdiv  10809  faclbnd  10812  bc0k  10827  bcval5  10834  seq3coll  10913  caucvgrelemcau  11124  resqrexlemlo  11157  resqrexlemcalc3  11160  resqrexlemgt0  11164  absexpzap  11224  climuni  11436  fsum3  11530  arisum  11641  trireciplem  11643  expcnvap0  11645  geo2sum  11657  geo2lim  11659  0.999...  11664  geoihalfsum  11665  cvgratz  11675  zproddc  11722  fprodseq  11726  prod1dc  11729  dvdsval3  11934  nndivdvds  11939  modmulconst  11966  dvdsle  11986  dvdsssfz1  11994  fzm1ndvds  11998  dvdsfac  12002  oexpneg  12018  nnoddm1d2  12051  divalg2  12067  divalgmod  12068  modremain  12070  ndvdsadd  12072  nndvdslegcd  12102  divgcdz  12108  divgcdnn  12112  divgcdnnr  12113  modgcd  12128  gcddiv  12156  gcdmultiple  12157  gcdmultiplez  12158  gcdzeq  12159  gcdeq  12160  rpmulgcd  12163  rplpwr  12164  rppwr  12165  sqgcd  12166  dvdssqlem  12167  dvdssq  12168  eucalginv  12194  lcmgcdlem  12215  lcmgcdnn  12220  lcmass  12223  coprmgcdb  12226  qredeq  12234  qredeu  12235  cncongr1  12241  cncongr2  12242  1idssfct  12253  isprm2lem  12254  isprm3  12256  isprm4  12257  prmind2  12258  prmdc  12268  divgcdodd  12281  isprm6  12285  sqrt2irr  12300  pw2dvds  12304  sqrt2irraplemnn  12317  divnumden  12334  divdenle  12335  nn0gcdsq  12338  phivalfi  12350  phicl2  12352  phiprmpw  12360  hashgcdlem  12376  hashgcdeq  12377  phisum  12378  nnoddn2prm  12398  pythagtriplem2  12404  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem8  12410  pythagtriplem9  12411  pythagtriplem11  12412  pythagtriplem13  12414  pythagtriplem15  12416  pythagtriplem19  12420  pythagtrip  12421  pceu  12433  pccl  12437  pcdiv  12440  pcqcl  12444  pcdvds  12453  pcndvds  12455  pcndvds2  12457  pcelnn  12459  pcz  12470  pcmpt  12481  fldivp1  12486  pcfac  12488  infpnlem1  12497  infpnlem2  12498  prmunb  12500  1arith  12505  oddennn  12549  evenennn  12550  unennn  12554  mulgnn  13196  mulgnngsum  13197  mulgaddcom  13216  mulginvcom  13217  mulgmodid  13231  ghmmulg  13326  mulgass2  13554  znfi  14143  znhash  14144  znidomb  14146  znrrg  14148  rpcxproot  15048  logbgcd1irr  15099  lgsval  15120  lgsval4a  15138  lgssq2  15157  gausslemma2dlem0c  15167  gausslemma2dlem0e  15169  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  gausslemma2dlem5  15182  lgsquadlem1  15191  trilpolemcl  15527