Theorem nnz 12545

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 12181	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1333	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12526	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11378  ℕcn 12174  ℤcz 12524

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-z 12525

This theorem is referenced by:  nnssz  12546  elnnz1  12553  znegcl  12562  nnleltp1  12584  nnltp1le  12585  nnlem1lt  12595  nnltlem1  12596  nnm1ge0  12597  prime  12610  nneo  12613  zeo  12615  btwnz  12632  eluz2b2  12871  qaddcl  12915  qreccl  12919  elpqb  12926  elfz1end  13508  fznatpl1  13532  fznn  13546  elfz1b  13547  elfzo0  13655  elfzo0z  13656  elfzo1  13667  fzo1fzo0n0  13670  elfzom1p1elfzo  13700  ubmelm1fzo  13718  quoremz  13814  intfracq  13818  fznnfl  13821  zmodcl  13850  zmodfz  13852  zmodfzo  13853  zmodid2  13858  zmodidfzo  13859  modfzo0difsn  13905  expnnval  14026  mulexpz  14064  nnesq  14189  expnlbnd  14195  expnlbnd2  14196  digit2  14198  faclbnd  14252  bc0k  14273  bcval5  14280  fz1isolem  14423  seqcoll  14426  ccatval21sw  14548  lswccatn0lsw  14554  cshwidxmod  14765  cshwidxn  14771  absexpz  15267  climuni  15514  isercoll  15630  climcnds  15816  arisum  15825  trireciplem  15827  expcnv  15829  pwdif  15833  geo2sum  15838  geo2lim  15840  0.999...  15846  geoihalfsum  15847  rpnnen2lem6  16186  rpnnen2lem9  16189  rpnnen2lem10  16190  dvdsval3  16225  nndivdvds  16230  modmulconst  16257  dvdsle  16279  dvdsssfz1  16287  fzm1ndvds  16291  dvdsfac  16295  mulmoddvds  16299  oexpneg  16314  nnoddm1d2  16355  pwp1fsum  16360  divalg2  16374  divalgmod  16375  modremain  16377  ndvdsadd  16379  nndvdslegcd  16474  divgcdz  16480  divgcdnn  16484  divgcdnnr  16485  modgcd  16501  gcdmultiple  16505  gcddiv  16520  gcdzeq  16521  gcdeq  16522  rpmulgcd  16526  rplpwr  16527  rprpwr  16528  nn0rppwr  16530  sqgcd  16531  nn0expgcd  16533  dvdssqlem  16535  dvdssq  16536  eucalginv  16553  lcmgcdlem  16575  lcmgcdnn  16580  lcmass  16583  lcmftp  16605  lcmfunsnlem2lem1  16607  coprmgcdb  16618  qredeq  16626  qredeu  16627  coprmprod  16630  coprmproddvdslem  16631  coprmproddvds  16632  cncongr1  16636  cncongr2  16637  1idssfct  16649  isprm2lem  16650  isprm3  16652  prmind2  16654  ge2nprmge4  16671  divgcdodd  16680  isprm6  16684  ncoprmlnprm  16698  divnumden  16718  divdenle  16719  nn0gcdsq  16722  phicl2  16738  phiprmpw  16746  eulerthlem2  16752  hashgcdlem  16758  hashgcdeq  16760  phisum  16761  nnoddn2prm  16782  pythagtriplem3  16789  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem8  16794  pythagtriplem9  16795  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem15  16800  pythagtriplem19  16804  pythagtrip  16805  iserodd  16806  pclem  16809  pccl  16820  pcdiv  16823  pcqcl  16827  pcdvds  16835  pcndvds  16837  pcndvds2  16839  pcelnn  16841  pcz  16852  pcmpt  16863  fldivp1  16868  pcfac  16870  infpnlem1  16881  prmunb  16885  prmreclem1  16887  1arith  16898  ram0  16993  prmdvdsprmo  17013  prmgaplem4  17025  prmgaplem6  17027  prmgaplem7  17028  cshwshashlem2  17067  setsstruct2  17144  mulgnn  19051  mulgaddcom  19074  mulginvcom  19075  mulgmodid  19089  ghmmulg  19203  dfod2  19539  gexdvds  19559  gexnnod  19563  gexex  19828  mulgass2  20290  qsssubdrg  21406  prmirredlem  21452  znidomb  21541  znrrg  21545  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmul0  22823  chfacfpmmul0  22827  cayhamlem1  22831  cpmadugsumlemF  22841  lmmo  23345  1stckgenlem  23518  imasdsf1olem  24338  clmmulg  25068  cmetcaulem  25255  ovolunlem1a  25463  ovolicc2lem4  25487  mbfi1fseqlem6  25687  dvexp3  25945  dgreq0  26230  elqaalem2  26286  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem9  26316  pserdvlem2  26393  logtayl2  26626  root1eq1  26719  root1cj  26720  zrtdvds  26723  logbgcd1irr  26758  atantayl2  26902  birthdaylem2  26916  birthdaylem3  26917  emcllem5  26963  basellem2  27045  basellem3  27046  basellem5  27048  issqf  27099  sgmnncl  27110  prmorcht  27141  mumullem1  27142  mumullem2  27143  sqff1o  27145  dvdsflsumcom  27151  muinv  27156  vmalelog  27168  chtublem  27174  vmasum  27179  logfac2  27180  logfaclbnd  27185  bclbnd  27243  bposlem5  27251  lgsval4a  27282  lgssq2  27301  lgsdchr  27318  gausslemma2dlem0c  27321  gausslemma2dlem0e  27323  gausslemma2dlem1a  27328  gausslemma2dlem5  27334  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad3  27350  2lgslem1a1  27352  2lgslem3  27367  2lgsoddprm  27379  2sqnn  27402  2sqreunnltlem  27413  rplogsumlem1  27447  rplogsumlem2  27448  dchrisumlem2  27453  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumiflem1  27464  dchrvmaeq0  27467  dchrisum0flblem2  27472  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem2a  27480  logdivbnd  27519  pntrsumbnd2  27530  ostth2lem1  27581  ostth2lem3  27598  ostth3  27601  axlowdimlem13  29023  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem7  29884  wlkiswwlksupgr2  29945  clwwisshclwwslem  30084  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  wwlksubclwwlk  30128  clwwlkvbij  30183  eucrctshift  30313  eucrct2eupth  30315  numclwlk2lem2f  30447  bcm1n  32868  pnfinf  33244  isarchiofld  33260  1fldgenq  33383  rearchi  33406  submat1n  33949  lmatfvlem  33959  esumcvg  34230  oddpwdc  34498  fibp1  34545  chtvalz  34773  nnltp1ne  35293  erdszelem7  35379  climuzcnv  35853  elfzm12  35857  bcprod  35920  nn0prpwlem  36504  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem18  36789  poimirlem13  37954  poimirlem14  37955  mblfinlem2  37979  fzmul  38062  incsequz  38069  geomcau  38080  heibor1lem  38130  bfplem2  38144  lcmfunnnd  42451  posbezout  42539  unitscyglem4  42637  dvdsexpnn  42765  dvdsexpnn0  42766  fimgmcyc  42979  fzsplit1nn0  43186  irrapxlem1  43250  pellexlem5  43261  rmynn  43384  jm2.24nn  43387  jm2.17c  43390  congrep  43401  congabseq  43402  acongrep  43408  acongeq  43411  jm2.18  43416  jm2.23  43424  jm2.20nn  43425  jm2.26lem3  43429  jm2.26  43430  jm2.15nn0  43431  jm2.16nn0  43432  jm2.27dlem2  43438  rmydioph  43442  jm3.1  43448  expdiophlem1  43449  expdioph  43451  idomodle  43619  proot1ex  43624  nznngen  44743  sumnnodd  46060  stoweidlem7  46435  stoweidlem17  46445  wallispilem4  46496  stirlinglem2  46503  stirlinglem3  46504  stirlinglem4  46505  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  dirkertrigeqlem1  46526  fouriersw  46659  ovnsubaddlem1  46998  nthrucw  47316  subsubelfzo0  47775  2ffzoeq  47776  nnmul2  47778  ceilhalfelfzo1  47782  2tceilhalfelfzo1  47784  difltmodne  47796  addmodne  47798  submodlt  47804  facnn0dvdsfac  47833  muldvdsfacgt  47834  iccpartres  47878  iccpartipre  47881  iccpartltu  47885  iccelpart  47893  odz2prm2pw  48026  fmtnoprmfac2lem1  48029  2pwp1prm  48052  lighneallem2  48069  lighneallem4  48073  lighneal  48074  proththd  48077  nneoALTV  48148  divgcdoddALTV  48158  fpprmod  48203  fppr2odd  48207  dfwppr  48214  fpprwppr  48215  fpprwpprb  48216  gbowge7  48239  gbege6  48241  gpg3kgrtriexlem2  48560  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem5  48563  gpg3kgrtriexlem6  48564  altgsumbc  48828  altgsumbcALT  48829  pw2m1lepw2m1  48996  nnpw2even  49005  nnlog2ge0lt1  49042  logbpw2m1  49043  blenpw2m1  49055  nnpw2blenfzo  49057  nnpw2pmod  49059  nnpw2p  49062  blengt1fldiv2p1  49069  dignn0fr  49077  dignn0flhalflem1  49091  dignn0flhalflem2  49092  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096