Theorem 4nn 12295

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 12276	. 2 ⊢ 4 = (3 + 1)
2		3nn 12291	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 12216	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2857	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2141  (class class class)co 7391  1c1 11068   + caddc 11070  ℕcn 12204  3c3 12267  4c4 12268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205  df-2 12274  df-3 12275  df-4 12276

This theorem is referenced by:  5nn  12298  4pos  12322  4ne0  12323  4nn0  12494  4z  12599  fldiv4p1lem1div2  13839  fldiv4lem1div2  13841  iexpcyc  14214  fsumcube  16081  ef01bndlem  16207  flodddiv4  16440  6lcm4e12  16641  2expltfac  17119  8nprm  17138  37prm  17148  43prm  17149  83prm  17150  139prm  17151  631prm  17154  prmo4  17155  1259prm  17163  2503lem2  17165  starvndx  17322  starvid  17323  srngstr  17329  homndx  17431  homid  17432  slotsdifplendx2  17436  slotsdifocndx  17437  prdsvalstr  17472  catstr  17984  lt6abl  19926  pcoass  25074  minveclem3  25479  iblitg  25818  dveflem  26029  tan4thpiOLD  26568  atan1  26981  log2tlbnd  26998  log2ub  27002  bclbnd  27332  bpos1  27335  bposlem6  27341  bposlem7  27342  bposlem8  27343  bposlem9  27344  gausslemma2dlem4  27421  m1lgs  27440  2lgslem1a  27443  2lgslem3a  27448  2lgslem3b  27449  2lgslem3c  27450  2lgslem3d  27451  2sqreultlem  27499  2sqreunnltlem  27502  chebbnd1lem1  27521  chebbnd1lem2  27522  chebbnd1lem3  27523  pntibndlem1  27641  pntibndlem2  27643  pntibndlem3  27644  pntlema  27648  pntlemb  27649  pntlemg  27650  pntlemf  27657  upgr4cycl4dv4e  30344  fib5  34663  hgt750lem2  34907  hgt750leme  34913  iccioo01  37782  420gcd8e4  42584  420lcm8e840  42589  lcm4un  42594  lcmineqlem23  42629  lcmineqlem  42630  3lexlogpow5ineq2  42633  aks4d1p1p5  42653  rmydioph  43552  rmxdioph  43554  expdiophlem2  43560  inductionexd  44692  amgm4d  44737  257prm  48131  fmtno4sqrt  48141  fmtno4prmfac  48142  fmtno4prmfac193  48143  fmtno5nprm  48153  139prmALT  48166  mod42tp1mod8  48172  ppivalnn4  48197  2exp340mod341  48316  341fppr2  48317  wtgoldbnnsum4prm  48385  bgoldbachlt  48396  tgblthelfgott  48398