Theorem peano2nn0 9355

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 9331	. 2 ⊢ 1 ∈ ℕ0
2		nn0addcl 9350	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
3	1, 2	mpan2 425	1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5957  1c1 7946   + caddc 7948  ℕ₀cn0 9315

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-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4170  ax-cnex 8036  ax-resscn 8037  ax-1cn 8038  ax-1re 8039  ax-icn 8040  ax-addcl 8041  ax-addrcl 8042  ax-mulcl 8043  ax-addcom 8045  ax-addass 8047  ax-i2m1 8050  ax-0id 8053

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-int 3892  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960  df-inn 9057  df-n0 9316

This theorem is referenced by:  peano2z  9428  nn0split  10278  fzonn0p1p1  10364  elfzom1p1elfzo  10365  frecfzennn  10593  leexp2r  10760  facdiv  10905  facwordi  10907  faclbnd  10908  faclbnd2  10909  faclbnd3  10910  faclbnd6  10911  bcnp1n  10926  bcp1m1  10932  bcpasc  10933  hashfz  10988  bcxmas  11875  geolim  11897  geo2sum  11900  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  efcllemp  12044  eftlub  12076  efsep  12077  effsumlt  12078  nn0ob  12294  nn0oddm1d2  12295  bitsp1  12337  nn0seqcvgd  12438  algcvg  12445  pw2dvdseulemle  12564  2sqpwodd  12573  nonsq  12604  pcprendvds  12688  pcpremul  12691  pcdvdsb  12718  4sqlem11  12799  ennnfonelemp1  12852  ennnfonelemkh  12858  ennnfonelemim  12870  elply2  15282  plyaddlem1  15294  plymullem1  15295  plycoeid3  15304  plycolemc  15305  dvply1  15312  dvply2g  15313  perfectlem1  15546  2lgslem3d1  15652