![]() |
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 2177 | . 2 ⊢ 0 = 0 | |
2 | elnn0 9174 | . . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0)) | |
3 | 2 | biimpri 133 | . . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0) |
4 | 3 | olcs 736 | . 2 ⊢ (0 = 0 → 0 ∈ ℕ0) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 0 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∨ wo 708 = wceq 1353 ∈ wcel 2148 0cc0 7808 ℕcn 8915 ℕ0cn0 9172 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-1cn 7901 ax-icn 7903 ax-addcl 7904 ax-mulcl 7906 ax-i2m1 7913 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3598 df-n0 9173 |
This theorem is referenced by: 0xnn0 9241 elnn0z 9262 nn0ind-raph 9366 10nn0 9397 declei 9415 numlti 9416 nummul1c 9428 decaddc2 9435 decrmanc 9436 decrmac 9437 decaddm10 9438 decaddi 9439 decaddci 9440 decaddci2 9441 decmul1 9443 decmulnc 9446 6p5e11 9452 7p4e11 9455 8p3e11 9460 9p2e11 9466 10p10e20 9474 fz01or 10106 0elfz 10113 4fvwrd4 10135 fvinim0ffz 10236 0tonninf 10434 exple1 10571 sq10 10685 bc0k 10729 bcn1 10731 bccl 10740 fihasheq0 10766 fsumnn0cl 11404 binom 11485 bcxmas 11490 isumnn0nn 11494 geoserap 11508 ef0lem 11661 ege2le3 11672 ef4p 11695 efgt1p2 11696 efgt1p 11697 nn0o 11904 ndvdssub 11927 gcdval 11952 gcdcl 11959 dfgcd3 12003 nn0seqcvgd 12033 algcvg 12040 eucalg 12051 lcmcl 12064 pw2dvdslemn 12157 pclem0 12278 pcpre1 12284 pcfac 12340 ennnfonelemj0 12394 ennnfonelem0 12398 ennnfonelem1 12400 slotsdifdsndx 12668 slotsdifunifndx 12675 nn0subm 13346 dveflem 14058 pilem3 14075 1kp2ke3k 14336 ex-fac 14340 012of 14605 isomninnlem 14638 iswomninnlem 14657 iswomni0 14659 ismkvnnlem 14660 |
Copyright terms: Public domain | W3C validator |