Theorem 4nn 12255

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  1c1 11030   + caddc 11032  ℕcn 12165  3c3 12228  4c4 12229

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

This theorem is referenced by:  5nn  12258  4ne0  12280  4nn0  12447  4z  12552  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  iexpcyc  14160  fsumcube  16016  ef01bndlem  16142  flodddiv4  16375  6lcm4e12  16576  2expltfac  17054  8nprm  17073  37prm  17082  43prm  17083  83prm  17084  139prm  17085  631prm  17088  prmo4  17089  1259prm  17097  2503lem2  17099  starvndx  17256  starvid  17257  srngstr  17263  homndx  17365  homid  17366  slotsdifplendx2  17370  slotsdifocndx  17371  prdsvalstr  17406  catstr  17918  lt6abl  19861  pcoass  25001  minveclem3  25406  iblitg  25745  dveflem  25956  tan4thpiOLD  26492  atan1  26905  log2tlbnd  26922  log2ub  26926  bclbnd  27257  bpos1  27260  bposlem6  27266  bposlem7  27267  bposlem8  27268  bposlem9  27269  gausslemma2dlem4  27346  m1lgs  27365  2lgslem1a  27368  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2sqreultlem  27424  2sqreunnltlem  27427  chebbnd1lem1  27446  chebbnd1lem2  27447  chebbnd1lem3  27448  pntibndlem1  27566  pntibndlem2  27568  pntibndlem3  27569  pntlema  27573  pntlemb  27574  pntlemg  27575  pntlemf  27582  upgr4cycl4dv4e  30270  fib5  34565  hgt750lem2  34812  hgt750leme  34818  iccioo01  37657  420gcd8e4  42459  420lcm8e840  42464  lcm4un  42469  lcmineqlem23  42504  lcmineqlem  42505  3lexlogpow5ineq2  42508  aks4d1p1p5  42528  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  inductionexd  44600  amgm4d  44645  257prm  48036  fmtno4sqrt  48046  fmtno4prmfac  48047  fmtno4prmfac193  48048  fmtno5nprm  48058  139prmALT  48071  mod42tp1mod8  48077  ppivalnn4  48102  2exp340mod341  48221  341fppr2  48222  wtgoldbnnsum4prm  48290  bgoldbachlt  48301  tgblthelfgott  48303