Theorem nnzi 11822

Description: A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Hypothesis

Ref	Expression
nnzi.1	⊢ 𝑁 ∈ ℕ

Assertion

Ref	Expression
nnzi	⊢ 𝑁 ∈ ℤ

Proof of Theorem nnzi

Step	Hyp	Ref	Expression
1		nnssz 11817	. 2 ⊢ ℕ ⊆ ℤ
2		nnzi.1	. 2 ⊢ 𝑁 ∈ ℕ
3	1, 2	sselii 3857	1 ⊢ 𝑁 ∈ ℤ

Syntax hints:   ∈ wcel 2050  ℕcn 11441  ℤcz 11796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-i2m1 10405  ax-1ne0 10406  ax-rrecex 10409  ax-cnre 10410

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-ov 6981  df-om 7399  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-neg 10675  df-nn 11442  df-z 11797

This theorem is referenced by:  1z  11828  2z  11830  3z  11831  4z  11832  faclbnd4lem1  13471  3dvds  15543  3dvdsdec  15544  divalglem6  15612  divalglem7  15613  divalglem8  15614  divalglem9  15615  ndvdsi  15626  6gcd4e2  15745  3lcm2e6  15931  prm23ge5  16011  pockthi  16102  modxai  16263  mod2xnegi  16266  gcdmodi  16269  strleun  16450  strle1  16451  lt6abl  18772  2logb9irr  25077  ppiublem1  25483  ppiublem2  25484  ppiub  25485  bpos1lem  25563  bposlem6  25570  bposlem8  25572  bposlem9  25573  lgsdir2lem5  25610  2lgsoddprmlem2  25690  ex-mod  28009  ex-dvds  28016  ex-gcd  28017  ex-lcm  28018  ballotlem1  31390  ballotlem2  31392  ballotlemfmpn  31398  ballotlemsdom  31415  ballotlemsel1i  31416  ballotlemsima  31419  ballotlemfrceq  31432  ballotlemfrcn0  31433  chtvalz  31548  hgt750lem  31570  inductionexd  39868  hoidmvlelem3  42311  fmtnoprmfac2lem1  43097  31prm  43129  mod42tp1mod8  43136  6even  43245  8even  43247  341fppr2  43268  8exp8mod9  43270  9fppr8  43271  nfermltl8rev  43276  nfermltlrev  43278  gbowge7  43297  gbege6  43299  stgoldbwt  43310  sbgoldbwt  43311  sbgoldbm  43318  mogoldbb  43319  sbgoldbo  43321  nnsum3primesle9  43328  nnsum4primeseven  43334  nnsum4primesevenALTV  43335  wtgoldbnnsum4prm  43336  bgoldbnnsum3prm  43338  bgoldbtbndlem1  43339  tgblthelfgott  43349  tgoldbach  43351  zlmodzxzequa  43919  zlmodzxznm  43920  zlmodzxzequap  43922  zlmodzxzldeplem3  43925  zlmodzxzldep  43927  ldepsnlinclem2  43929  ldepsnlinc  43931