Theorem 4nn 9403

Description: 4 is a positive integer. (Contributed by NM, 8-Jan-2006.)

Assertion

Ref	Expression
4nn	⊢ 4 ∈ ℕ

Proof of Theorem 4nn

Step	Hyp	Ref	Expression
1		df-4 9300	. 2 ⊢ 4 = (3 + 1)
2		3nn 9402	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 9251	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2307	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2205  (class class class)co 6052  1c1 8130   + caddc 8132  ℕcn 9239  3c3 9291  4c4 9292

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4230  ax-cnex 8220  ax-resscn 8221  ax-1re 8223  ax-addrcl 8226

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-inn 9240  df-2 9298  df-3 9299  df-4 9300

This theorem is referenced by:  5nn  9404  4nn0  9517  4z  9609  fldiv4p1lem1div2  10669  fldiv4lem1div2uz2  10670  fldiv4lem1div2  10671  iexpcyc  11010  resqrexlemnmsq  11706  ef01bndlem  12446  flodddiv4  12626  flodddiv4t2lthalf  12629  6lcm4e12  12788  2expltfac  13141  starvndx  13369  starvid  13370  starvslid  13371  srngstrd  13376  homndx  13463  homid  13464  homslid  13465  prdsvalstrd  13501  dveflem  15608  tan4thpi  15723  gausslemma2dlem0d  15942  gausslemma2dlem3  15953  gausslemma2dlem4  15954  gausslemma2dlem5a  15955  gausslemma2dlem5  15956  gausslemma2dlem6  15957  m1lgs  15975  2lgslem1a2  15977  2lgslem1a  15978  2lgslem1  15981  2lgslem2  15982  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986