Theorem 4nn 12269

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 12251	. 2 ⊢ 4 = (3 + 1)
2		3nn 12265	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 12198	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  1c1 11069   + caddc 11071  ℕcn 12186  3c3 12242  4c4 12243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-2 12249  df-3 12250  df-4 12251

This theorem is referenced by:  5nn  12272  4ne0  12294  4nn0  12461  4z  12567  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  iexpcyc  14172  fsumcube  16026  ef01bndlem  16152  flodddiv4  16385  6lcm4e12  16586  2expltfac  17063  8nprm  17082  37prm  17091  43prm  17092  83prm  17093  139prm  17094  631prm  17097  prmo4  17098  1259prm  17106  2503lem2  17108  starvndx  17265  starvid  17266  srngstr  17272  homndx  17374  homid  17375  slotsdifplendx2  17379  slotsdifocndx  17380  prdsvalstr  17415  catstr  17922  lt6abl  19825  pcoass  24924  minveclem3  25329  iblitg  25669  dveflem  25883  tan4thpiOLD  26424  atan1  26838  log2tlbnd  26855  log2ub  26859  bclbnd  27191  bpos1  27194  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  gausslemma2dlem4  27280  m1lgs  27299  2lgslem1a  27302  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2sqreultlem  27358  2sqreunnltlem  27361  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  pntibndlem1  27500  pntibndlem2  27502  pntibndlem3  27503  pntlema  27507  pntlemb  27508  pntlemg  27509  pntlemf  27516  upgr4cycl4dv4e  30114  fib5  34396  hgt750lem2  34643  hgt750leme  34649  iccioo01  37315  420gcd8e4  41994  420lcm8e840  41999  lcm4un  42004  lcmineqlem23  42039  lcmineqlem  42040  3lexlogpow5ineq2  42043  aks4d1p1p5  42063  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  inductionexd  44144  amgm4d  44189  257prm  47562  fmtno4sqrt  47572  fmtno4prmfac  47573  fmtno4prmfac193  47574  fmtno5nprm  47584  139prmALT  47597  mod42tp1mod8  47603  2exp340mod341  47734  341fppr2  47735  wtgoldbnnsum4prm  47803  bgoldbachlt  47814  tgblthelfgott  47816