![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0nn0 | Unicode version |
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
0nn0 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2189 |
. 2
![]() ![]() ![]() ![]() | |
2 | elnn0 9203 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpri 133 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | olcs 737 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 5 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 7929 ax-icn 7931 ax-addcl 7932 ax-mulcl 7934 ax-i2m1 7941 |
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 9202 |
This theorem is referenced by: 0xnn0 9270 elnn0z 9291 nn0ind-raph 9395 10nn0 9426 declei 9444 numlti 9445 nummul1c 9457 decaddc2 9464 decrmanc 9465 decrmac 9466 decaddm10 9467 decaddi 9468 decaddci 9469 decaddci2 9470 decmul1 9472 decmulnc 9475 6p5e11 9481 7p4e11 9484 8p3e11 9489 9p2e11 9495 10p10e20 9503 fz01or 10136 0elfz 10143 4fvwrd4 10165 fvinim0ffz 10266 0tonninf 10465 exple1 10602 sq10 10719 bc0k 10763 bcn1 10765 bccl 10774 fihasheq0 10800 fsumnn0cl 11438 binom 11519 bcxmas 11524 isumnn0nn 11528 geoserap 11542 ef0lem 11695 ege2le3 11706 ef4p 11729 efgt1p2 11730 efgt1p 11731 nn0o 11939 ndvdssub 11962 gcdval 11987 gcdcl 11994 dfgcd3 12038 nn0seqcvgd 12068 algcvg 12075 eucalg 12086 lcmcl 12099 pw2dvdslemn 12192 pclem0 12313 pcpre1 12319 pcfac 12377 ennnfonelemj0 12447 ennnfonelem0 12451 ennnfonelem1 12453 slotsdifdsndx 12725 slotsdifunifndx 12732 nn0subm 13879 dveflem 14624 pilem3 14641 1kp2ke3k 14913 ex-fac 14917 012of 15183 isomninnlem 15216 iswomninnlem 15235 iswomni0 15237 ismkvnnlem 15238 |
Copyright terms: Public domain | W3C validator |