Theorem peano2nn0 12684

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
peano2nn0	⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Proof of Theorem peano2nn0

Step	Hyp	Ref	Expression
1		1nn0 12660	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 12679	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 704	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7449  1c1 11238   + caddc 11240  ℕ₀cn0 12644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-ov 7452  df-om 7910  df-2nd 8034  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-er 8753  df-en 9010  df-dom 9011  df-sdom 9012  df-pnf 11382  df-mnf 11383  df-ltxr 11385  df-nn 12374  df-n0 12645

This theorem is used by:  nn0split  13815  fzonn0p1p1  13917  leexp2r  14355  expnbnd  14415  facdiv  14470  facwordi  14472  faclbnd  14473  faclbnd2  14474  faclbnd3  14475  faclbnd6  14482  bcnp1n  14497  bcp1m1  14503  bcpasc  14504  hashfz  14611  hashf1  14641  hashdifsnp1  14690  fi1uzind  14691  brfi1indALT  14694  pfxccatpfx2  14926  pfxccat3a  14927  swrds2  15132  iseraltlem2  15891  bcxmas  16045  climcndslem1  16059  climcnds  16061  pwdif  16078  geolim  16080  geo2sum  16083  mertenslem1  16094  mertenslem2  16095  mertens  16096  risefacp1  16236  fallfacp1  16237  binomfallfaclem1  16246  binomfallfaclem2  16247  fsumkthpow  16263  efcllem  16284  eftlub  16318  efsep  16319  effsumlt  16320  ruclem9  16447  nn0ob  16595  nn0oddm1d2  16596  pwp1fsum  16602  bitsp1  16642  sadcp1  16666  smuval2  16693  smu01lem  16696  smup1  16700  nn0seqcvgd  16786  algcvg  16792  nonsq  16976  iserodd  17054  pcprendvds  17059  pcpremul  17062  pcdvdsb  17088  4sqlem11  17174  vdwapun  17193  vdwlem1  17200  vdwlem9  17208  ramub1  17247  ramcl  17248  prmop1  17257  sylow1lem3  19856  efgsfo  19995  efgred  20004  telgsums  20249  telgsum  20250  srgbinomlem3  20496  srgbinomlem4  20497  assamulgscmlem2  22252  psdmplcl  22527  psdadd  22528  psdvsca  22529  psdmul  22531  chfacffsupp  23218  chfacfscmulfsupp  23221  chfacfscmulgsum  23222  chfacfpmmulfsupp  23225  chfacfpmmulgsum  23226  cpnord  26299  ply1divex  26499  fta1glem1  26530  fta1glem2  26531  fta1g  26532  plyco0  26554  plyaddlem1  26576  plymullem1  26577  plyco  26604  dvply1  26649  dvply2g  26650  aaliou3lem8  26718  aaliou3lem9  26723  dvtaylp  26743  dvradcnv  26794  pserdvlem2  26801  advlogexp  27029  atantayl3  27313  leibpi  27316  log2cnv  27318  ftalem4  27449  ftalem5  27450  perfectlem1  27602  bcp1ctr  27652  2lgslem3d1  27776  dchrisum0flblem1  27881  ostth2lem2  28007  ostth2lem3  28008  crctcshwlkn0lem7  30451  wwlksnred  30527  wwlksnext  30528  wwlksnextbi  30529  wwlksnredwwlkn  30530  wwlksnredwwlkn0  30531  wwlksnextproplem1  30544  wwlksnextproplem2  30545  wwlksnextproplem3  30546  rusgrnumwwlks  30612  clwwlkf  30684  clwwlknonex2lem2  30745  eupth2lems  30885  eucrct2eupth  30892  numclwlk2lem2f  31024  nndiffz1  33464  nn0diffz0  33472  2exple2exp  33511  gsummoncoe1fz  34226  esplyindfv  34312  vietalem  34315  nn0constr  34497  subfacval2  36153  erdsze2lem1  36169  bccolsum  36712  fwddifnp1  37138  knoppndvlem6  37591  poimirlem17  38816  heiborlem3  39006  heiborlem4  39007  heiborlem6  39009  facp2  43452  sqn5i  43602  sumcubes  43630  2rexfrabdioph  44063  elnn0rabdioph  44070  dvdsrabdioph  44077  jm2.17a  44227  jm2.17b  44228  expdiophlem1  44288  expdiophlem2  44289  hbt  44391  cotrclrcl  44997  k0004ss3  45408  bccp1k  45580  binomcxplemnn0  45588  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnmul  47220  stoweidlem17  47294  wallispilem1  47342  stirlinglem5  47355  etransclem23  47534  etransclem46  47557  etransclem48  47559  fmtnoge3  48882  fmtnorec1  48889  sqrtpwpw2p  48890  fmtnosqrt  48891  fmtnorec2lem  48894  fmtnorec3  48900  fmtnoprmfac1  48917  fmtnoprmfac2lem1  48918  fmtnofac1  48922  flsqrt  48945  perfectALTVlem1  49086  isubgr3stgrlem2  49332  nn0eo  49965  fllog2  50005  dignnld  50040  0dig2nn0o  50050  dignn0ehalf  50054  dignn0flhalf  50055  nn0sumshdiglemA  50056  itcovalsuc  50104  ackvalsuc1mpt  50115  ackval1  50118  ackval2  50119  ackval3  50120  ackendofnn0  50121  ackval0val  50123  ackvalsucsucval  50125  aacllem  51361