![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 10nn0 | 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 8371 | . 2 ⊢ 1 ∈ ℕ0 | |
2 | 0nn0 8370 | . 2 ⊢ 0 ∈ ℕ0 | |
3 | 1, 2 | deccl 8572 | 1 ⊢ ;10 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1434 0cc0 7043 1c1 7044 ℕ0cn0 8355 ;cdc 8558 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-setind 4288 ax-cnex 7129 ax-resscn 7130 ax-1cn 7131 ax-1re 7132 ax-icn 7133 ax-addcl 7134 ax-addrcl 7135 ax-mulcl 7136 ax-addcom 7138 ax-mulcom 7139 ax-addass 7140 ax-mulass 7141 ax-distr 7142 ax-i2m1 7143 ax-1rid 7145 ax-0id 7146 ax-rnegex 7147 ax-cnre 7149 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-int 3645 df-br 3794 df-opab 3848 df-id 4056 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-iota 4897 df-fun 4934 df-fv 4940 df-riota 5499 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-sub 7348 df-inn 8107 df-2 8165 df-3 8166 df-4 8167 df-5 8168 df-6 8169 df-7 8170 df-8 8171 df-9 8172 df-n0 8356 df-dec 8559 |
This theorem is referenced by: decnncl 8577 dec0u 8578 dec0h 8579 decsuc 8588 decle 8591 decma 8608 decmac 8609 decma2c 8610 decadd 8611 decaddc 8612 decsubi 8620 decmul1 8621 decmul1c 8622 decmul2c 8623 decmul10add 8626 9t11e99 8687 |
Copyright terms: Public domain | W3C validator |