Theorem 9nn0 11733

Description: 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Assertion

Ref	Expression
9nn0	⊢ 9 ∈ ℕ0

Proof of Theorem 9nn0

Step	Hyp	Ref	Expression
1		9nn 11544	. 2 ⊢ 9 ∈ ℕ
2	1	nnnn0i 11716	1 ⊢ 9 ∈ ℕ0

Syntax hints:   ∈ wcel 2050  9c9 11502  ℕ₀cn0 11707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-1cn 10393

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708

This theorem is referenced by:  deccl  11926  le9lt10  11939  decsucc  11953  9p2e11  12000  9p3e12  12001  9p4e13  12002  9p5e14  12003  9p6e15  12004  9p7e16  12005  9p8e17  12006  9p9e18  12007  9t3e27  12036  9t4e36  12037  9t5e45  12038  9t6e54  12039  9t7e63  12040  9t8e72  12041  9t9e81  12042  sq10e99m1  13440  3dvds2dec  15542  2exp8  16279  19prm  16307  prmlem2  16309  37prm  16310  83prm  16312  139prm  16313  163prm  16314  317prm  16315  631prm  16316  1259lem1  16320  1259lem2  16321  1259lem3  16322  1259lem4  16323  1259lem5  16324  1259prm  16325  2503lem1  16326  2503lem2  16327  2503lem3  16328  2503prm  16329  4001lem1  16330  4001lem2  16331  4001lem3  16332  4001lem4  16333  cnfldfun  20259  tuslem  22579  setsmsds  22789  tnglem  22952  tngds  22960  log2ublem3  25228  log2ub  25229  bposlem8  25569  9p10ne21  28026  dp2lt10  30306  1mhdrd  30338  hgt750lem2  31568  hgt750leme  31574  kur14lem8  32042  sqdeccom12  38604  fmtno5lem1  43081  fmtno5lem3  43083  fmtno5lem4  43084  fmtno5  43085  257prm  43089  fmtno4prmfac  43100  fmtno4nprmfac193  43102  fmtno5fac  43110  139prmALT  43125  127prm  43129  m11nprm  43132  2exp340mod341  43264  tgblthelfgott  43346  tgoldbachlt  43347