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

Theorem 9nn 11382
Description: 9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
Assertion
Ref Expression
9nn 9 ∈ ℕ

Proof of Theorem 9nn
StepHypRef Expression
1 df-9 11276 . 2 9 = (8 + 1)
2 8nn 11381 . . 3 8 ∈ ℕ
3 peano2nn 11222 . . 3 (8 ∈ ℕ → (8 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (8 + 1) ∈ ℕ
51, 4eqeltri 2833 1 9 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 2137  (class class class)co 6811  1c1 10127   + caddc 10129  cn 11210  8c8 11266  9c9 11267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-1cn 10184
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-reu 3055  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-ov 6814  df-om 7229  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276
This theorem is referenced by:  10nnOLD  11383  9nn0  11506  9p1e10  11686  10nn  11704  3dvdsdec  15254  3dvdsdecOLD  15255  19prm  16025  prmlem2  16027  37prm  16028  43prm  16029  83prm  16030  139prm  16031  163prm  16032  317prm  16033  631prm  16034  1259lem1  16038  1259lem2  16039  1259lem3  16040  1259lem4  16041  1259lem5  16042  2503lem3  16046  tsetndx  16240  tsetid  16241  topgrpstr  16242  resstset  16246  otpsstr  16251  otpsstrOLD  16255  odrngstr  16266  imasvalstr  16312  ipostr  17352  oppgtset  17980  mgptset  18695  sratset  19384  psrvalstr  19563  cnfldstr  19948  eltpsg  20947  indistpsALT  21017  mcubic  24771  log2cnv  24868  log2tlbnd  24869  log2ublem2  24871  log2ub  24873  bposlem7  25212  ex-cnv  27603  ex-dm  27605  ex-gcd  27623  ex-lcm  27624  ex-prmo  27625  hgt750lem2  31037  rmydioph  38081  deccarry  41829  257prm  41981  fmtno4nprmfac193  41994  139prmALT  42019  127prm  42023  wtgoldbnnsum4prm  42198  bgoldbnnsum3prm  42200  bgoldbtbndlem1  42201  tgblthelfgott  42211  tgblthelfgottOLD  42217
  Copyright terms: Public domain W3C validator