Theorem 9nn 11777

Description: 9 is a positive integer. (Contributed by NM, 21-Oct-2012.)

Assertion

Ref	Expression
9nn	⊢ 9 ∈ ℕ

Proof of Theorem 9nn

Step	Hyp	Ref	Expression
1		df-9 11749	. 2 ⊢ 9 = (8 + 1)
2		8nn 11774	. . 3 ⊢ 8 ∈ ℕ
3		peano2nn 11691	. . 3 ⊢ (8 ∈ ℕ → (8 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (8 + 1) ∈ ℕ
5	1, 4	eqeltri 2848	1 ⊢ 9 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7155  1c1 10581   + caddc 10583  ℕcn 11679  8c8 11740  9c9 11741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464  ax-1cn 10638

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7158  df-om 7585  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749

This theorem is referenced by:  9nn0  11963  9p1e10  12144  10nn  12158  3dvdsdec  15738  19prm  16514  prmlem2  16516  37prm  16517  43prm  16518  83prm  16519  139prm  16520  163prm  16521  317prm  16522  631prm  16523  1259lem1  16527  1259lem2  16528  1259lem3  16529  1259lem4  16530  1259lem5  16531  2503lem3  16535  tsetndx  16722  tsetid  16723  topgrpstr  16724  resstset  16728  otpsstr  16731  odrngstr  16742  imasvalstr  16788  ipostr  17834  oppgtset  18552  mgptset  19320  sratset  20029  cnfldstr  20173  psrvalstr  20683  eltpsg  21648  indistpsALT  21718  2logb9irr  25485  sqrt2cxp2logb9e3  25489  mcubic  25537  log2cnv  25634  log2tlbnd  25635  log2ublem2  25637  log2ub  25639  bposlem7  25978  ex-cnv  28326  ex-dm  28328  ex-gcd  28346  ex-lcm  28347  ex-prmo  28348  idlsrgstr  31172  hgt750lem2  32155  lcmineqlem23  39644  3lexlogpow2ineq1  39651  3lexlogpow2ineq2  39652  rmydioph  40356  deccarry  44264  257prm  44474  fmtno4nprmfac193  44487  139prmALT  44509  127prm  44512  8exp8mod9  44649  9fppr8  44650  nfermltl8rev  44655  wtgoldbnnsum4prm  44715  bgoldbnnsum3prm  44717  bgoldbtbndlem1  44718  tgblthelfgott  44728