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 2164 | . 2 | |
2 | elnn0 9107 | . . . 4 | |
3 | 2 | biimpri 132 | . . 3 |
4 | 3 | olcs 726 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wo 698 wceq 1342 wcel 2135 cc0 7744 cn 8848 cn0 9105 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-1cn 7837 ax-icn 7839 ax-addcl 7840 ax-mulcl 7842 ax-i2m1 7849 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-n0 9106 |
This theorem is referenced by: 0xnn0 9174 elnn0z 9195 nn0ind-raph 9299 10nn0 9330 declei 9348 numlti 9349 nummul1c 9361 decaddc2 9368 decrmanc 9369 decrmac 9370 decaddm10 9371 decaddi 9372 decaddci 9373 decaddci2 9374 decmul1 9376 decmulnc 9379 6p5e11 9385 7p4e11 9388 8p3e11 9393 9p2e11 9399 10p10e20 9407 fz01or 10036 0elfz 10043 4fvwrd4 10065 fvinim0ffz 10166 0tonninf 10364 exple1 10501 sq10 10614 bc0k 10658 bcn1 10660 bccl 10669 fihasheq0 10696 fsumnn0cl 11330 binom 11411 bcxmas 11416 isumnn0nn 11420 geoserap 11434 ef0lem 11587 ege2le3 11598 ef4p 11621 efgt1p2 11622 efgt1p 11623 nn0o 11829 ndvdssub 11852 gcdval 11877 gcdcl 11884 dfgcd3 11928 nn0seqcvgd 11952 algcvg 11959 eucalg 11970 lcmcl 11983 pw2dvdslemn 12074 pclem0 12195 pcpre1 12201 pcfac 12257 ennnfonelemj0 12271 ennnfonelem0 12275 ennnfonelem1 12277 dveflem 13228 pilem3 13245 1kp2ke3k 13442 ex-fac 13446 012of 13709 isomninnlem 13743 iswomninnlem 13762 iswomni0 13764 ismkvnnlem 13765 |
Copyright terms: Public domain | W3C validator |