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 2157 | . 2 ⊢ 0 = 0 | |
2 | elnn0 9092 | . . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0)) | |
3 | 2 | biimpri 132 | . . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0) |
4 | 3 | olcs 726 | . 2 ⊢ (0 = 0 → 0 ∈ ℕ0) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 0 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∨ wo 698 = wceq 1335 ∈ wcel 2128 0cc0 7732 ℕcn 8833 ℕ0cn0 9090 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-1cn 7825 ax-icn 7827 ax-addcl 7828 ax-mulcl 7830 ax-i2m1 7837 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 df-un 3106 df-sn 3566 df-n0 9091 |
This theorem is referenced by: 0xnn0 9159 elnn0z 9180 nn0ind-raph 9281 10nn0 9312 declei 9330 numlti 9331 nummul1c 9343 decaddc2 9350 decrmanc 9351 decrmac 9352 decaddm10 9353 decaddi 9354 decaddci 9355 decaddci2 9356 decmul1 9358 decmulnc 9361 6p5e11 9367 7p4e11 9370 8p3e11 9375 9p2e11 9381 10p10e20 9389 fz01or 10013 0elfz 10020 4fvwrd4 10039 fvinim0ffz 10140 0tonninf 10338 exple1 10475 sq10 10586 bc0k 10630 bcn1 10632 bccl 10641 fihasheq0 10668 fsumnn0cl 11300 binom 11381 bcxmas 11386 isumnn0nn 11390 geoserap 11404 ef0lem 11557 ege2le3 11568 ef4p 11591 efgt1p2 11592 efgt1p 11593 nn0o 11798 ndvdssub 11821 gcdval 11843 gcdcl 11850 dfgcd3 11894 nn0seqcvgd 11918 algcvg 11925 eucalg 11936 lcmcl 11949 pw2dvdslemn 12040 ennnfonelemj0 12141 ennnfonelem0 12145 ennnfonelem1 12147 dveflem 13098 pilem3 13115 1kp2ke3k 13311 ex-fac 13315 012of 13578 isomninnlem 13612 iswomninnlem 13631 iswomni0 13633 ismkvnnlem 13634 |
Copyright terms: Public domain | W3C validator |