Theorem 4nn 12302

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 12284	. 2 ⊢ 4 = (3 + 1)
2		3nn 12298	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 12231	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2828	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2105  (class class class)co 7412  1c1 11117   + caddc 11119  ℕcn 12219  3c3 12275  4c4 12276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729  ax-1cn 11174

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-om 7860  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-nn 12220  df-2 12282  df-3 12283  df-4 12284

This theorem is referenced by:  5nn  12305  4nn0  12498  4z  12603  fldiv4p1lem1div2  13807  fldiv4lem1div2  13809  iexpcyc  14178  fsumcube  16011  ef01bndlem  16134  flodddiv4  16363  6lcm4e12  16560  2expltfac  17033  8nprm  17052  37prm  17061  43prm  17062  83prm  17063  139prm  17064  631prm  17067  prmo4  17068  1259prm  17076  2503lem2  17078  starvndx  17254  starvid  17255  srngstr  17261  homndx  17363  homid  17364  slotsdifplendx2  17369  slotsdifocndx  17370  prdsvalstr  17405  oppchomfvalOLD  17666  oppcbasOLD  17671  resccoOLD  17788  catstr  17919  lt6abl  19811  pcoass  24871  minveclem3  25277  iblitg  25618  dveflem  25831  tan4thpi  26364  atan1  26774  log2tlbnd  26791  log2ub  26795  bclbnd  27127  bpos1  27130  bposlem6  27136  bposlem7  27137  bposlem8  27138  bposlem9  27139  gausslemma2dlem4  27216  m1lgs  27235  2lgslem1a  27238  2lgslem3a  27243  2lgslem3b  27244  2lgslem3c  27245  2lgslem3d  27246  2sqreultlem  27294  2sqreunnltlem  27297  chebbnd1lem1  27316  chebbnd1lem2  27317  chebbnd1lem3  27318  pntibndlem1  27436  pntibndlem2  27438  pntibndlem3  27439  pntlema  27443  pntlemb  27444  pntlemg  27445  pntlemf  27452  upgr4cycl4dv4e  29872  fib5  33869  hgt750lem2  34129  hgt750leme  34135  iccioo01  36674  420gcd8e4  41340  420lcm8e840  41345  lcm4un  41350  lcmineqlem23  41385  lcmineqlem  41386  3lexlogpow5ineq2  41389  aks4d1p1p5  41409  rmydioph  42218  rmxdioph  42220  expdiophlem2  42226  inductionexd  43371  amgm4d  43417  257prm  46690  fmtno4sqrt  46700  fmtno4prmfac  46701  fmtno4prmfac193  46702  fmtno5nprm  46712  139prmALT  46725  mod42tp1mod8  46731  2exp340mod341  46862  341fppr2  46863  wtgoldbnnsum4prm  46931  bgoldbachlt  46942  tgblthelfgott  46944  prstclevalOLD  47853  prstcocvalOLD  47856