MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2nnd Structured version   Visualization version   GIF version

Theorem peano2nnd 11643
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
peano2nnd (𝜑 → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nnd
StepHypRef Expression
1 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
2 peano2nn 11638 . 2 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
31, 2syl 17 1 (𝜑 → (𝐴 + 1) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  1c1 10526   + caddc 10528  cn 11626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-nn 11627
This theorem is referenced by:  bcpasc  13669  relexpsucnnr  14372  o1fsum  15156  bpolydiflem  15396  eftlub  15450  eirrlem  15545  infpnlem1  16234  infpnlem2  16235  prmreclem4  16243  prmreclem5  16244  prmreclem6  16245  vdwlem6  16310  cayhamlem1  21402  ovolunlem1a  24024  ovolicc2lem3  24047  uniioombllem3  24113  uniioombllem4  24114  vieta1lem1  24826  vieta1lem2  24827  aaliou3lem2  24859  lgamgulmlem3  25535  lgamgulmlem4  25536  lgamgulmlem5  25537  lgamgulmlem6  25538  lgamgulm2  25540  lgamcvg2  25559  gamcvg  25560  gamcvg2lem  25563  regamcl  25565  relgamcl  25566  basellem1  25585  basellem2  25586  basellem3  25587  basellem4  25588  basellem5  25589  basellem6  25590  basellem7  25591  basellem8  25592  basellem9  25593  perfectlem1  25732  perfectlem2  25733  bclbnd  25783  lgsdilem2  25836  rplogsumlem2  25988  dchrisumlem2  25993  pntrsumbnd2  26070  pntrlog2bndlem2  26081  pntpbnd1a  26088  pntpbnd1  26089  pntpbnd2  26090  axlowdimlem16  26670  fzto1st  30672  psgnfzto1st  30674  isarchi3  30743  ofldchr  30814  smatrcl  30960  esumfzf  31227  esumpcvgval  31236  esumcvg  31244  dstfrvunirn  31631  dstfrvclim1  31634  subfacp1lem1  32323  subfacp1lem5  32328  subfaclim  32332  poimirlem7  34780  poimirlem15  34788  poimirlem17  34790  poimirlem19  34792  poimirlem28  34801  4rexfrabdioph  39273  6rexfrabdioph  39274  pellfundge  39357  pellfundgt1  39358  limsup10exlem  41929  wallispilem5  42231  wallispi2lem1  42233  wallispi2  42235  fourierdlem47  42315  nnfoctbdjlem  42614  hoidmvlelem2  42755  vonioolem2  42840  vonicclem2  42843  fmtnof1  43574  lighneallem4b  43651  proththdlem  43655  perfectALTVlem1  43763  perfectALTVlem2  43764  blennngt2o2  44580
  Copyright terms: Public domain W3C validator