Theorem 10nn0 11928

Description: 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)

Assertion

Ref	Expression
10nn0	⊢ ;10 ∈ ℕ0

Proof of Theorem 10nn0

Step	Hyp	Ref	Expression
1		1nn0 11724	. 2 ⊢ 1 ∈ ℕ0
2		0nn0 11723	. 2 ⊢ 0 ∈ ℕ0
3	1, 2	deccl 11925	1 ⊢ ;10 ∈ ℕ0

Syntax hints:   ∈ wcel 2051  0cc0 10334  1c1 10335  ℕ₀cn0 11706  ;cdc 11910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-ov 6978  df-om 7396  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-ltxr 10478  df-nn 11439  df-2 11502  df-3 11503  df-4 11504  df-5 11505  df-6 11506  df-7 11507  df-8 11508  df-9 11509  df-n0 11707  df-dec 11911

This theorem is referenced by:  decnncl  11931  dec0u  11932  dec0h  11933  decsuc  11942  decle  11945  decma  11962  decmac  11963  decma2c  11964  decadd  11965  decaddc  11966  decsubi  11974  decmul1OLD  11976  decmul1c  11977  decmul2c  11978  decmul10add  11981  9t11e99  12042  sq10  13438  dec2dvds  16254  decsplit0b  16271  decsplit1  16273  decsplit  16274  karatsuba  16275  139prm  16312  317prm  16314  1259lem1  16319  1259lem3  16321  2503lem1  16325  4001lem1  16329  4001lem3  16331  9p10ne21  28042  dfdec100  30317  dp20u  30325  dp20h  30326  dp2clq  30328  dpmul100  30344  dpmul1000  30346  dpexpp1  30355  0dp2dp  30356  dpmul  30360  dpmul4  30361  hgt750lemd  31600  hgt750lem2  31604  hgt750leme  31610  tgoldbachgnn  31611  sqdeccom12  38641  rmydioph  39041  tgoldbach  43380