Theorem 4nn 11034

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 10928	. 2 ⊢ 4 = (3 + 1)
2		3nn 11033	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 10879	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2683	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 1976  (class class class)co 6527  1c1 9793   + caddc 9795  ℕcn 10867  3c3 10918  4c4 10919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-1cn 9850

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10868  df-2 10926  df-3 10927  df-4 10928

This theorem is referenced by:  5nn  11035  4nn0  11158  4z  11244  fldiv4p1lem1div2  12453  fldiv4lem1div2  12455  iexpcyc  12786  fsumcube  14576  ef01bndlem  14699  flodddiv4  14921  6lcm4e12  15113  2expltfac  15583  8nprm  15602  37prm  15612  43prm  15613  83prm  15614  139prm  15615  631prm  15618  prmo4  15619  1259prm  15627  2503lem2  15629  starvndx  15773  starvid  15774  ressstarv  15776  srngfn  15777  homndx  15843  homid  15844  resshom  15847  prdsvalstr  15882  oppchomfval  16143  oppcbas  16147  rescco  16261  catstr  16386  lt6abl  18065  pcoass  22563  minveclem3  22925  iblitg  23258  dveflem  23463  tan4thpi  23987  atan1  24372  log2tlbnd  24389  log2ub  24393  bclbnd  24722  bpos1  24725  bposlem6  24731  bposlem7  24732  bposlem8  24733  bposlem9  24734  gausslemma2dlem4  24811  m1lgs  24830  2lgslem1a  24833  2lgslem3a  24838  2lgslem3b  24839  2lgslem3c  24840  2lgslem3d  24841  chebbnd1lem1  24875  chebbnd1lem2  24876  chebbnd1lem3  24877  pntibndlem1  24995  pntibndlem2  24997  pntibndlem3  24998  pntlema  25002  pntlemb  25003  pntlemg  25004  pntlemf  25011  4cycl4dv  25961  fib5  29600  rmydioph  36395  rmxdioph  36397  expdiophlem2  36403  inductionexd  37269  amgm4d  37321  257prm  39809  fmtno4sqrt  39819  fmtno4prmfac  39820  fmtno4prmfac193  39821  fmtno5nprm  39831  139prmALT  39847  mod42tp1mod8  39855  wtgoldbnnsum4prm  40016  bgoldbachlt  40025  tgblthelfgott  40027  bgoldbachltOLD  40032  tgblthelfgottOLD  40034  upgr4cycl4dv4e  41347