![]() |
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 2140 | . 2 ⊢ 0 = 0 | |
2 | elnn0 9003 | . . . 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 1332 ∈ wcel 1481 0cc0 7644 ℕcn 8744 ℕ0cn0 9001 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-1cn 7737 ax-icn 7739 ax-addcl 7740 ax-mulcl 7742 ax-i2m1 7749 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-un 3080 df-sn 3538 df-n0 9002 |
This theorem is referenced by: 0xnn0 9070 elnn0z 9091 nn0ind-raph 9192 10nn0 9223 declei 9241 numlti 9242 nummul1c 9254 decaddc2 9261 decrmanc 9262 decrmac 9263 decaddm10 9264 decaddi 9265 decaddci 9266 decaddci2 9267 decmul1 9269 decmulnc 9272 6p5e11 9278 7p4e11 9281 8p3e11 9286 9p2e11 9292 10p10e20 9300 fz01or 9922 0elfz 9929 4fvwrd4 9948 fvinim0ffz 10049 0tonninf 10243 exple1 10380 sq10 10490 bc0k 10534 bcn1 10536 bccl 10545 fihasheq0 10572 fsumnn0cl 11204 binom 11285 bcxmas 11290 isumnn0nn 11294 geoserap 11308 ef0lem 11403 ege2le3 11414 ef4p 11437 efgt1p2 11438 efgt1p 11439 nn0o 11640 ndvdssub 11663 gcdval 11684 gcdcl 11691 dfgcd3 11734 nn0seqcvgd 11758 algcvg 11765 eucalg 11776 lcmcl 11789 pw2dvdslemn 11879 ennnfonelemj0 11950 ennnfonelem0 11954 ennnfonelem1 11956 dveflem 12895 pilem3 12912 1kp2ke3k 13107 ex-fac 13111 012of 13363 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 |
Copyright terms: Public domain | W3C validator |