Theorem 5nn 12206

Description: 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
5nn	⊢ 5 ∈ ℕ

Proof of Theorem 5nn

Step	Hyp	Ref	Expression
1		df-5 12186	. 2 ⊢ 5 = (4 + 1)
2		4nn 12203	. . 3 ⊢ 4 ∈ ℕ
3		peano2nn 12132	. . 3 ⊢ (4 ∈ ℕ → (4 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (4 + 1) ∈ ℕ
5	1, 4	eqeltri 2827	1 ⊢ 5 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7341  1c1 11002   + caddc 11004  ℕcn 12120  4c4 12177  5c5 12178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-1cn 11059

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12121  df-2 12183  df-3 12184  df-4 12185  df-5 12186

This theorem is referenced by:  6nn  12209  5nn0  12396  5eluz3  12776  5ndvds3  16319  5ndvds6  16320  prm23ge5  16722  dec5dvds  16971  dec5nprm  16973  dec2nprm  16974  5prm  17015  10nprm  17020  23prm  17025  prmlem2  17026  43prm  17028  83prm  17029  317prm  17032  prmo5  17035  scandx  17213  scaid  17214  lmodstr  17224  ipsstr  17235  ccondx  17312  ccoid  17313  slotsbhcdif  17314  slotsdifplendx2  17315  slotsdifocndx  17316  prdsvalstr  17351  catstr  17862  lt6abl  19802  psrvalstr  21848  log2ublem1  26878  log2ublem2  26879  log2ub  26881  birthday  26886  ppiublem1  27135  ppiublem2  27136  ppiub  27137  bclbnd  27213  bposlem3  27219  bposlem4  27220  bposlem5  27221  bposlem6  27222  bposlem8  27224  bposlem9  27225  lgsdir2lem3  27260  ex-eprel  30405  ex-xp  30408  fib6  34411  hgt750lem2  34657  hgt750leme  34663  12gcd5e1  42036  12lcm5e60  42041  lcm5un  42050  lcmineqlem  42085  3lexlogpow5ineq1  42087  3lexlogpow2ineq1  42091  3lexlogpow2ineq2  42092  3lexlogpow5ineq5  42093  aks4d1p1p6  42106  aks4d1p1  42109  5ne0  42293  rmydioph  43047  expdiophlem2  43055  algstr  43206  inductionexd  44188  plusmod5ne  47376  minusmod5ne  47380  minusmodnep2tmod  47384  8mod5e3  47391  257prm  47592  fmtno4prmfac193  47604  31prm  47628  41prothprm  47650  gbowge7  47794  gbege6  47796  stgoldbwt  47807  sbgoldbwt  47808  sbgoldbm  47815  sbgoldbo  47818  nnsum3primesle9  47825  gpg5order  48091  gpg5nbgrvtx13starlem1  48102  gpg5nbgrvtx13starlem2  48103  gpg5nbgrvtx13starlem3  48104  gpg5nbgr3star  48112  gpg5grlim  48124  pgnioedg1  48139  pgnioedg2  48140  pgnioedg3  48141  pgnioedg4  48142  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem4  48150  gpg5edgnedg  48161  grlimedgnedg  48162