![]() |
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 2189 | . 2 ⊢ 0 = 0 | |
2 | elnn0 9209 | . . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0)) | |
3 | 2 | biimpri 133 | . . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0) |
4 | 3 | olcs 737 | . 2 ⊢ (0 = 0 → 0 ∈ ℕ0) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 0 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∨ wo 709 = wceq 1364 ∈ wcel 2160 0cc0 7842 ℕcn 8950 ℕ0cn0 9207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-1cn 7935 ax-icn 7937 ax-addcl 7938 ax-mulcl 7940 ax-i2m1 7947 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-sn 3613 df-n0 9208 |
This theorem is referenced by: 0xnn0 9276 elnn0z 9297 nn0ind-raph 9401 10nn0 9432 declei 9450 numlti 9451 nummul1c 9463 decaddc2 9470 decrmanc 9471 decrmac 9472 decaddm10 9473 decaddi 9474 decaddci 9475 decaddci2 9476 decmul1 9478 decmulnc 9481 6p5e11 9487 7p4e11 9490 8p3e11 9495 9p2e11 9501 10p10e20 9509 fz01or 10143 0elfz 10150 4fvwrd4 10172 fvinim0ffz 10273 0tonninf 10472 exple1 10610 sq10 10727 bc0k 10771 bcn1 10773 bccl 10782 fihasheq0 10808 fsumnn0cl 11446 binom 11527 bcxmas 11532 isumnn0nn 11536 geoserap 11550 ef0lem 11703 ege2le3 11714 ef4p 11737 efgt1p2 11738 efgt1p 11739 nn0o 11947 ndvdssub 11970 gcdval 11995 gcdcl 12002 dfgcd3 12046 nn0seqcvgd 12076 algcvg 12083 eucalg 12094 lcmcl 12107 pw2dvdslemn 12200 pclem0 12321 pcpre1 12327 pcfac 12385 ennnfonelemj0 12455 ennnfonelem0 12459 ennnfonelem1 12461 slotsdifdsndx 12735 slotsdifunifndx 12742 nn0subm 13903 fczpsrbag 13966 dveflem 14664 pilem3 14681 1kp2ke3k 14954 ex-fac 14958 012of 15224 isomninnlem 15257 iswomninnlem 15276 iswomni0 15278 ismkvnnlem 15279 |
Copyright terms: Public domain | W3C validator |