Theorem 4nn 11708

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 11690	. 2 ⊢ 4 = (3 + 1)
2		3nn 11704	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 11637	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2886	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  1c1 10527   + caddc 10529  ℕcn 11625  3c3 11681  4c4 11682

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626  df-2 11688  df-3 11689  df-4 11690

This theorem is referenced by:  5nn  11711  4nn0  11904  4z  12004  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  iexpcyc  13565  fsumcube  15406  ef01bndlem  15529  flodddiv4  15754  6lcm4e12  15950  2expltfac  16418  8nprm  16437  37prm  16446  43prm  16447  83prm  16448  139prm  16449  631prm  16452  prmo4  16453  1259prm  16461  2503lem2  16463  starvndx  16615  starvid  16616  ressstarv  16618  srngstr  16619  homndx  16679  homid  16680  resshom  16683  prdsvalstr  16718  oppchomfval  16976  oppcbas  16980  rescco  17094  catstr  17219  lt6abl  19008  pcoass  23629  minveclem3  24033  iblitg  24372  dveflem  24582  tan4thpi  25107  atan1  25514  log2tlbnd  25531  log2ub  25535  bclbnd  25864  bpos1  25867  bposlem6  25873  bposlem7  25874  bposlem8  25875  bposlem9  25876  gausslemma2dlem4  25953  m1lgs  25972  2lgslem1a  25975  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2sqreultlem  26031  2sqreunnltlem  26034  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  pntibndlem1  26173  pntibndlem2  26175  pntibndlem3  26176  pntlema  26180  pntlemb  26181  pntlemg  26182  pntlemf  26189  upgr4cycl4dv4e  27970  fib5  31773  hgt750lem2  32033  hgt750leme  32039  iccioo01  34741  420gcd8e4  39294  420lcm8e840  39299  lcm4un  39304  lcmineqlem23  39339  lcmineqlem  39340  3lexlogpow5ineq1  39341  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  inductionexd  40858  amgm4d  40906  257prm  44078  fmtno4sqrt  44088  fmtno4prmfac  44089  fmtno4prmfac193  44090  fmtno5nprm  44100  139prmALT  44113  mod42tp1mod8  44120  2exp340mod341  44251  341fppr2  44252  wtgoldbnnsum4prm  44320  bgoldbachlt  44331  tgblthelfgott  44333