Theorem nnz 12575

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022.)

Assertion

Ref	Expression
nnz	⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnre 12215	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1331	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12556	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  ℝcr 11105  0cc0 11106  -cneg 11441  ℕcn 12208  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-neg 11443  df-nn 12209  df-z 12555

This theorem is referenced by:  nnssz  12576  elnnz1  12584  znegcl  12593  nnleltp1  12613  nnltp1le  12614  nnlem1lt  12624  nnltlem1  12625  nnm1ge0  12626  prime  12639  nneo  12642  zeo  12644  btwnz  12661  eluz2b2  12901  qaddcl  12945  qreccl  12949  elpqb  12956  elfz1end  13527  fznatpl1  13551  fznn  13565  elfz1b  13566  elfzo0  13669  elfzo0z  13670  elfzo1  13678  fzo1fzo0n0  13679  elfzom1p1elfzo  13708  ubmelm1fzo  13724  quoremz  13816  intfracq  13820  fznnfl  13823  zmodcl  13852  zmodfz  13854  zmodfzo  13855  zmodid2  13860  zmodidfzo  13861  modfzo0difsn  13904  expnnval  14026  mulexpz  14064  nnesq  14186  expnlbnd  14192  expnlbnd2  14193  digit2  14195  faclbnd  14246  bc0k  14267  bcval5  14274  fz1isolem  14418  seqcoll  14421  ccatval21sw  14531  lswccatn0lsw  14537  cshwidxmod  14749  cshwidxn  14755  absexpz  15248  climuni  15492  isercoll  15610  climcnds  15793  arisum  15802  trireciplem  15804  expcnv  15806  pwdif  15810  geo2sum  15815  geo2lim  15817  0.999...  15823  geoihalfsum  15824  rpnnen2lem6  16158  rpnnen2lem9  16161  rpnnen2lem10  16162  dvdsval3  16197  nndivdvds  16202  modmulconst  16227  dvdsle  16249  dvdsssfz1  16257  fzm1ndvds  16261  dvdsfac  16265  mulmoddvds  16269  oexpneg  16284  nnoddm1d2  16325  pwp1fsum  16330  divalg2  16344  divalgmod  16345  modremain  16347  ndvdsadd  16349  nndvdslegcd  16442  divgcdz  16448  divgcdnn  16452  divgcdnnr  16453  modgcd  16470  gcdmultiple  16474  gcddiv  16489  gcdzeq  16490  gcdeq  16491  rpmulgcd  16494  rplpwr  16495  rprpwr  16496  sqgcd  16498  dvdssqlem  16499  dvdssq  16500  eucalginv  16517  lcmgcdlem  16539  lcmgcdnn  16544  lcmass  16547  lcmftp  16569  lcmfunsnlem2lem1  16571  coprmgcdb  16582  qredeq  16590  qredeu  16591  coprmprod  16594  coprmproddvdslem  16595  coprmproddvds  16596  cncongr1  16600  cncongr2  16601  1idssfct  16613  isprm2lem  16614  isprm3  16616  prmind2  16618  ge2nprmge4  16634  divgcdodd  16643  isprm6  16647  ncoprmlnprm  16660  divnumden  16680  divdenle  16681  nn0gcdsq  16684  phicl2  16697  phiprmpw  16705  eulerthlem2  16711  hashgcdlem  16717  hashgcdeq  16718  phisum  16719  nnoddn2prm  16740  pythagtriplem3  16747  pythagtriplem4  16748  pythagtriplem6  16750  pythagtriplem7  16751  pythagtriplem8  16752  pythagtriplem9  16753  pythagtriplem11  16754  pythagtriplem13  16756  pythagtriplem15  16758  pythagtriplem19  16762  pythagtrip  16763  iserodd  16764  pclem  16767  pccl  16778  pcdiv  16781  pcqcl  16785  pcdvds  16793  pcndvds  16795  pcndvds2  16797  pcelnn  16799  pcz  16810  pcmpt  16821  fldivp1  16826  pcfac  16828  infpnlem1  16839  prmunb  16843  prmreclem1  16845  1arith  16856  ram0  16951  prmdvdsprmo  16971  prmgaplem4  16983  prmgaplem6  16985  prmgaplem7  16986  cshwshashlem2  17026  setsstruct2  17103  mulgnn  18952  mulgaddcom  18972  mulginvcom  18973  mulgmodid  18987  ghmmulg  19098  dfod2  19426  gexdvds  19446  gexnnod  19450  gexex  19715  mulgass2  20114  qsssubdrg  20996  prmirredlem  21033  znidomb  21108  znrrg  21112  chfacfisf  22347  chfacfisfcpmat  22348  chfacfscmul0  22351  chfacfpmmul0  22355  cayhamlem1  22359  cpmadugsumlemF  22369  lmmo  22875  1stckgenlem  23048  imasdsf1olem  23870  clmmulg  24608  cmetcaulem  24796  ovolunlem1a  25004  ovolicc2lem4  25028  mbfi1fseqlem6  25229  dvexp3  25486  dgreq0  25770  elqaalem2  25824  aaliou3lem1  25846  aaliou3lem2  25847  aaliou3lem3  25848  aaliou3lem9  25854  pserdvlem2  25931  logtayl2  26161  root1eq1  26252  root1cj  26253  logbgcd1irr  26288  atantayl2  26432  birthdaylem2  26446  birthdaylem3  26447  emcllem5  26493  basellem2  26575  basellem3  26576  basellem5  26578  issqf  26629  sgmnncl  26640  prmorcht  26671  mumullem1  26672  mumullem2  26673  sqff1o  26675  dvdsflsumcom  26681  muinv  26686  vmalelog  26697  chtublem  26703  vmasum  26708  logfac2  26709  logfaclbnd  26714  bclbnd  26772  bposlem5  26780  lgsval4a  26811  lgssq2  26830  lgsdchr  26847  gausslemma2dlem0c  26850  gausslemma2dlem0e  26852  gausslemma2dlem1a  26857  gausslemma2dlem5  26863  lgsquadlem1  26872  lgsquadlem2  26873  lgsquad3  26879  2lgslem1a1  26881  2lgslem3  26896  2lgsoddprm  26908  2sqnn  26931  2sqreunnltlem  26942  rplogsumlem1  26976  rplogsumlem2  26977  dchrisumlem2  26982  dchrmusumlema  26985  dchrmusum2  26986  dchrvmasumiflem1  26993  dchrvmaeq0  26996  dchrisum0flblem2  27001  dchrisum0re  27005  dchrisum0lema  27006  dchrisum0lem1b  27007  dchrisum0lem2a  27009  logdivbnd  27048  pntrsumbnd2  27059  ostth2lem1  27110  ostth2lem3  27127  ostth3  27130  axlowdimlem13  28201  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem7  29059  wlkiswwlksupgr2  29120  clwwisshclwwslem  29256  clwwlkinwwlk  29282  clwwlkel  29288  clwwlkf  29289  wwlksubclwwlk  29300  clwwlkvbij  29355  eucrctshift  29485  eucrct2eupth  29487  numclwlk2lem2f  29619  bcm1n  31993  pnfinf  32316  1fldgenq  32400  isarchiofld  32423  rearchi  32449  submat1n  32773  lmatfvlem  32783  esumcvg  33072  oddpwdc  33341  fibp1  33388  chtvalz  33629  nnltp1ne  34088  erdszelem7  34176  climuzcnv  34644  elfzm12  34648  bcprod  34696  nn0prpwlem  35195  knoppndvlem1  35376  knoppndvlem2  35377  knoppndvlem7  35382  knoppndvlem18  35393  poimirlem13  36489  poimirlem14  36490  mblfinlem2  36514  fzmul  36597  incsequz  36604  geomcau  36615  heibor1lem  36665  bfplem2  36679  lcmfunnnd  40865  metakunt16  40988  metakunt26  40998  nn0rppwr  41219  nn0expgcd  41221  dvdsexpnn  41226  dvdsexpnn0  41227  zrtdvds  41232  fzsplit1nn0  41477  irrapxlem1  41545  pellexlem5  41556  rmynn  41680  jm2.24nn  41683  jm2.17c  41686  congrep  41697  congabseq  41698  acongrep  41704  acongeq  41707  jm2.18  41712  jm2.23  41720  jm2.20nn  41721  jm2.26lem3  41725  jm2.26  41726  jm2.15nn0  41727  jm2.16nn0  41728  jm2.27dlem2  41734  rmydioph  41738  jm3.1  41744  expdiophlem1  41745  expdioph  41747  idomodle  41923  proot1ex  41928  nznngen  43060  sumnnodd  44332  stoweidlem7  44709  stoweidlem17  44719  wallispilem4  44770  stirlinglem2  44777  stirlinglem3  44778  stirlinglem4  44779  stirlinglem12  44787  stirlinglem13  44788  stirlinglem14  44789  stirlinglem15  44790  stirlingr  44792  dirkertrigeqlem1  44800  fouriersw  44933  ovnsubaddlem1  45272  subsubelfzo0  46020  2ffzoeq  46022  iccpartres  46072  iccpartipre  46075  iccpartltu  46079  iccelpart  46087  odz2prm2pw  46217  fmtnoprmfac2lem1  46220  2pwp1prm  46243  lighneallem2  46260  lighneallem4  46264  lighneal  46265  proththd  46268  nneoALTV  46326  divgcdoddALTV  46336  fpprmod  46381  fppr2odd  46385  dfwppr  46392  fpprwppr  46393  fpprwpprb  46394  gbowge7  46417  gbege6  46419  altgsumbc  46981  altgsumbcALT  46982  pw2m1lepw2m1  47154  nnpw2even  47168  nnlog2ge0lt1  47205  logbpw2m1  47206  blenpw2m1  47218  nnpw2blenfzo  47220  nnpw2pmod  47222  nnpw2p  47225  blengt1fldiv2p1  47232  dignn0fr  47240  dignn0flhalflem1  47254  dignn0flhalflem2  47255  nn0sumshdiglemA  47258  nn0sumshdiglemB  47259