Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0nn0 | GIF version |
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
0nn0 | ⊢ 0 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2139 | . 2 ⊢ 0 = 0 | |
2 | elnn0 8979 | . . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0)) | |
3 | 2 | biimpri 132 | . . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0) |
4 | 3 | olcs 725 | . 2 ⊢ (0 = 0 → 0 ∈ ℕ0) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 0 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∨ wo 697 = wceq 1331 ∈ wcel 1480 0cc0 7620 ℕcn 8720 ℕ0cn0 8977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-1cn 7713 ax-icn 7715 ax-addcl 7716 ax-mulcl 7718 ax-i2m1 7725 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-sn 3533 df-n0 8978 |
This theorem is referenced by: 0xnn0 9046 elnn0z 9067 nn0ind-raph 9168 10nn0 9199 declei 9217 numlti 9218 nummul1c 9230 decaddc2 9237 decrmanc 9238 decrmac 9239 decaddm10 9240 decaddi 9241 decaddci 9242 decaddci2 9243 decmul1 9245 decmulnc 9248 6p5e11 9254 7p4e11 9257 8p3e11 9262 9p2e11 9268 10p10e20 9276 fz01or 9891 0elfz 9898 4fvwrd4 9917 fvinim0ffz 10018 0tonninf 10212 exple1 10349 sq10 10459 bc0k 10502 bcn1 10504 bccl 10513 fihasheq0 10540 fsumnn0cl 11172 binom 11253 bcxmas 11258 isumnn0nn 11262 geoserap 11276 ef0lem 11366 ege2le3 11377 ef4p 11400 efgt1p2 11401 efgt1p 11402 nn0o 11604 ndvdssub 11627 gcdval 11648 gcdcl 11655 dfgcd3 11698 nn0seqcvgd 11722 algcvg 11729 eucalg 11740 lcmcl 11753 pw2dvdslemn 11843 ennnfonelemj0 11914 ennnfonelem0 11918 ennnfonelem1 11920 dveflem 12855 pilem3 12864 1kp2ke3k 12936 ex-fac 12940 isomninnlem 13225 |
Copyright terms: Public domain | W3C validator |