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

Theorem 4nn 12170
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 12152 . 2 4 = (3 + 1)
2 3nn 12166 . . 3 3 ∈ ℕ
3 peano2nn 12099 . . 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 2107  (class class class)co 7350  1c1 10986   + caddc 10988  cn 12087  3c3 12143  4c4 12144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383  ax-un 7663  ax-1cn 11043
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7353  df-om 7794  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-nn 12088  df-2 12150  df-3 12151  df-4 12152
This theorem is referenced by:  5nn  12173  4nn0  12366  4z  12468  fldiv4p1lem1div2  13669  fldiv4lem1div2  13671  iexpcyc  14037  fsumcube  15878  ef01bndlem  16001  flodddiv4  16230  6lcm4e12  16427  2expltfac  16900  8nprm  16919  37prm  16928  43prm  16929  83prm  16930  139prm  16931  631prm  16934  prmo4  16935  1259prm  16943  2503lem2  16945  starvndx  17118  starvid  17119  srngstr  17125  homndx  17227  homid  17228  slotsdifplendx2  17233  slotsdifocndx  17234  prdsvalstr  17269  oppchomfvalOLD  17530  oppcbasOLD  17535  resccoOLD  17652  catstr  17780  lt6abl  19601  pcoass  24309  minveclem3  24715  iblitg  25055  dveflem  25265  tan4thpi  25793  atan1  26200  log2tlbnd  26217  log2ub  26221  bclbnd  26550  bpos1  26553  bposlem6  26559  bposlem7  26560  bposlem8  26561  bposlem9  26562  gausslemma2dlem4  26639  m1lgs  26658  2lgslem1a  26661  2lgslem3a  26666  2lgslem3b  26667  2lgslem3c  26668  2lgslem3d  26669  2sqreultlem  26717  2sqreunnltlem  26720  chebbnd1lem1  26739  chebbnd1lem2  26740  chebbnd1lem3  26741  pntibndlem1  26859  pntibndlem2  26861  pntibndlem3  26862  pntlema  26866  pntlemb  26867  pntlemg  26868  pntlemf  26875  upgr4cycl4dv4e  28915  fib5  32766  hgt750lem2  33026  hgt750leme  33032  iccioo01  35684  420gcd8e4  40349  420lcm8e840  40354  lcm4un  40359  lcmineqlem23  40394  lcmineqlem  40395  3lexlogpow5ineq2  40398  aks4d1p1p5  40418  rmydioph  41172  rmxdioph  41174  expdiophlem2  41180  inductionexd  42160  amgm4d  42206  257prm  45453  fmtno4sqrt  45463  fmtno4prmfac  45464  fmtno4prmfac193  45465  fmtno5nprm  45475  139prmALT  45488  mod42tp1mod8  45494  2exp340mod341  45625  341fppr2  45626  wtgoldbnnsum4prm  45694  bgoldbachlt  45705  tgblthelfgott  45707  prstclevalOLD  46789  prstcocvalOLD  46792
  Copyright terms: Public domain W3C validator