Theorem 5nn 12258

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 12238	. 2 ⊢ 5 = (4 + 1)
2		4nn 12255	. . 3 ⊢ 4 ∈ ℕ
3		peano2nn 12177	. . 3 ⊢ (4 ∈ ℕ → (4 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (4 + 1) ∈ ℕ
5	1, 4	eqeltri 2833	1 ⊢ 5 ∈ ℕ

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  1c1 11030   + caddc 11032  ℕcn 12165  4c4 12229  5c5 12230

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 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238

This theorem is referenced by:  6nn  12261  5nn0  12448  5eluz3  12824  5ndvds3  16373  5ndvds6  16374  prm23ge5  16777  dec5dvds  17026  dec5nprm  17028  dec2nprm  17029  5prm  17070  10nprm  17075  23prm  17080  prmlem2  17081  43prm  17083  83prm  17084  317prm  17087  prmo5  17090  scandx  17268  scaid  17269  lmodstr  17279  ipsstr  17290  ccondx  17367  ccoid  17368  slotsbhcdif  17369  slotsdifplendx2  17370  slotsdifocndx  17371  prdsvalstr  17406  catstr  17918  lt6abl  19861  psrvalstr  21906  log2ublem1  26923  log2ublem2  26924  log2ub  26926  birthday  26931  ppiublem1  27179  ppiublem2  27180  ppiub  27181  bclbnd  27257  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem8  27268  bposlem9  27269  lgsdir2lem3  27304  ex-eprel  30518  ex-xp  30521  fib6  34566  hgt750lem2  34812  hgt750leme  34818  12gcd5e1  42456  12lcm5e60  42461  lcm5un  42470  lcmineqlem  42505  3lexlogpow5ineq1  42507  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1p1p6  42526  aks4d1p1  42529  5ne0  42712  rmydioph  43460  expdiophlem2  43468  algstr  43619  inductionexd  44600  plusmod5ne  47811  minusmod5ne  47815  minusmodnep2tmod  47819  8mod5e3  47826  257prm  48036  fmtno4prmfac193  48048  31prm  48072  41prothprm  48094  gbowge7  48251  gbege6  48253  stgoldbwt  48264  sbgoldbwt  48265  sbgoldbm  48272  sbgoldbo  48275  nnsum3primesle9  48282  gpg5order  48548  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg5nbgr3star  48569  gpg5grlim  48581  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem4  48607  gpg5edgnedg  48618  grlimedgnedg  48619