![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 10nn0 | Structured version Visualization version GIF version |
Description: 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
Ref | Expression |
---|---|
10nn0 | ⊢ ;10 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 11724 | . 2 ⊢ 1 ∈ ℕ0 | |
2 | 0nn0 11723 | . 2 ⊢ 0 ∈ ℕ0 | |
3 | 1, 2 | deccl 11925 | 1 ⊢ ;10 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 0cc0 10334 1c1 10335 ℕ0cn0 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 |
Copyright terms: Public domain | W3C validator |