MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4nn Structured version   Visualization version   GIF version

Theorem 4nn 11937
Description: 4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
Assertion
Ref Expression
4nn 4 ∈ ℕ

Proof of Theorem 4nn
StepHypRef Expression
1 df-4 11919 . 2 4 = (3 + 1)
2 3nn 11933 . . 3 3 ∈ ℕ
3 peano2nn 11866 . . 3 (3 ∈ ℕ → (3 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (3 + 1) ∈ ℕ
51, 4eqeltri 2835 1 4 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  (class class class)co 7231  1c1 10754   + caddc 10756  cn 11854  3c3 11910  4c4 11911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336  ax-un 7541  ax-1cn 10811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-ov 7234  df-om 7663  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-nn 11855  df-2 11917  df-3 11918  df-4 11919
This theorem is referenced by:  5nn  11940  4nn0  12133  4z  12235  fldiv4p1lem1div2  13434  fldiv4lem1div2  13436  iexpcyc  13799  fsumcube  15646  ef01bndlem  15769  flodddiv4  15998  6lcm4e12  16197  2expltfac  16670  8nprm  16689  37prm  16698  43prm  16699  83prm  16700  139prm  16701  631prm  16704  prmo4  16705  1259prm  16713  2503lem2  16715  starvndx  16869  starvid  16870  srngstr  16874  homndx  16942  homid  16943  prdsvalstr  16981  oppchomfvalOLD  17242  oppcbas  17246  resccoOLD  17362  catstr  17489  lt6abl  19304  pcoass  23945  minveclem3  24350  iblitg  24690  dveflem  24900  tan4thpi  25428  atan1  25835  log2tlbnd  25852  log2ub  25856  bclbnd  26185  bpos1  26188  bposlem6  26194  bposlem7  26195  bposlem8  26196  bposlem9  26197  gausslemma2dlem4  26274  m1lgs  26293  2lgslem1a  26296  2lgslem3a  26301  2lgslem3b  26302  2lgslem3c  26303  2lgslem3d  26304  2sqreultlem  26352  2sqreunnltlem  26355  chebbnd1lem1  26374  chebbnd1lem2  26375  chebbnd1lem3  26376  pntibndlem1  26494  pntibndlem2  26496  pntibndlem3  26497  pntlema  26501  pntlemb  26502  pntlemg  26503  pntlemf  26510  upgr4cycl4dv4e  28292  fib5  32108  hgt750lem2  32368  hgt750leme  32374  iccioo01  35258  420gcd8e4  39774  420lcm8e840  39779  lcm4un  39784  lcmineqlem23  39819  lcmineqlem  39820  3lexlogpow5ineq2  39823  aks4d1p1p5  39842  rmydioph  40567  rmxdioph  40569  expdiophlem2  40575  inductionexd  41470  amgm4d  41517  257prm  44714  fmtno4sqrt  44724  fmtno4prmfac  44725  fmtno4prmfac193  44726  fmtno5nprm  44736  139prmALT  44749  mod42tp1mod8  44755  2exp340mod341  44886  341fppr2  44887  wtgoldbnnsum4prm  44955  bgoldbachlt  44966  tgblthelfgott  44968  prstcleval  46050  prstcocval  46052
  Copyright terms: Public domain W3C validator