Theorem 4nn 12349

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 12331	. 2 ⊢ 4 = (3 + 1)
2		3nn 12345	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 12278	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2837	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  1c1 11156   + caddc 11158  ℕcn 12266  3c3 12322  4c4 12323

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-2 12329  df-3 12330  df-4 12331

This theorem is referenced by:  5nn  12352  4nn0  12545  4z  12651  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  iexpcyc  14246  fsumcube  16096  ef01bndlem  16220  flodddiv4  16452  6lcm4e12  16653  2expltfac  17130  8nprm  17149  37prm  17158  43prm  17159  83prm  17160  139prm  17161  631prm  17164  prmo4  17165  1259prm  17173  2503lem2  17175  starvndx  17346  starvid  17347  srngstr  17353  homndx  17455  homid  17456  slotsdifplendx2  17461  slotsdifocndx  17462  prdsvalstr  17497  catstr  18005  lt6abl  19913  pcoass  25057  minveclem3  25463  iblitg  25803  dveflem  26017  tan4thpiOLD  26557  atan1  26971  log2tlbnd  26988  log2ub  26992  bclbnd  27324  bpos1  27327  bposlem6  27333  bposlem7  27334  bposlem8  27335  bposlem9  27336  gausslemma2dlem4  27413  m1lgs  27432  2lgslem1a  27435  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2sqreultlem  27491  2sqreunnltlem  27494  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  pntibndlem1  27633  pntibndlem2  27635  pntibndlem3  27636  pntlema  27640  pntlemb  27641  pntlemg  27642  pntlemf  27649  upgr4cycl4dv4e  30204  fib5  34407  hgt750lem2  34667  hgt750leme  34673  iccioo01  37328  420gcd8e4  42007  420lcm8e840  42012  lcm4un  42017  lcmineqlem23  42052  lcmineqlem  42053  3lexlogpow5ineq2  42056  aks4d1p1p5  42076  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  inductionexd  44168  amgm4d  44213  257prm  47548  fmtno4sqrt  47558  fmtno4prmfac  47559  fmtno4prmfac193  47560  fmtno5nprm  47570  139prmALT  47583  mod42tp1mod8  47589  2exp340mod341  47720  341fppr2  47721  wtgoldbnnsum4prm  47789  bgoldbachlt  47800  tgblthelfgott  47802  prstclevalOLD  49158  prstcocvalOLD  49161