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

Theorem 9nn 11136
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 11030 . 2 9 = (8 + 1)
2 8nn 11135 . . 3 8 ∈ ℕ
3 peano2nn 10976 . . 3 (8 ∈ ℕ → (8 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (8 + 1) ∈ ℕ
51, 4eqeltri 2694 1 9 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  (class class class)co 6604  1c1 9881   + caddc 9883  cn 10964  8c8 11020  9c9 11021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-1cn 9938
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030
This theorem is referenced by:  10nnOLD  11137  9nn0  11260  9p1e10  11440  10nn  11458  3dvdsdec  14978  3dvdsdecOLD  14979  19prm  15749  prmlem2  15751  37prm  15752  43prm  15753  83prm  15754  139prm  15755  163prm  15756  317prm  15757  631prm  15758  1259lem1  15762  1259lem2  15763  1259lem3  15764  1259lem4  15765  1259lem5  15766  2503lem3  15770  tsetndx  15961  tsetid  15962  topgrpstr  15963  resstset  15967  otpsstr  15972  otpsstrOLD  15976  odrngstr  15987  imasvalstr  16033  ipostr  17074  oppgtset  17703  mgptset  18418  sratset  19103  psrvalstr  19282  cnfldstr  19667  eltpsg  20660  indistpsALT  20727  mcubic  24474  log2cnv  24571  log2tlbnd  24572  log2ublem2  24574  log2ub  24576  bposlem7  24915  ex-cnv  27148  ex-dm  27150  ex-gcd  27168  ex-lcm  27169  ex-prmo  27170  rmydioph  37061  deccarry  40618  257prm  40772  fmtno4nprmfac193  40785  139prmALT  40810  127prm  40814  wtgoldbnnsum4prm  40979  bgoldbnnsum3prm  40981  bgoldbtbndlem1  40982  tgblthelfgott  40990  tgblthelfgottOLD  40997
  Copyright terms: Public domain W3C validator