![]() |
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 2113 |
. 2
![]() ![]() ![]() ![]() | |
2 | elnn0 8877 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpri 132 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | olcs 708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 7 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-1cn 7632 ax-icn 7634 ax-addcl 7635 ax-mulcl 7637 ax-i2m1 7644 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-v 2657 df-un 3039 df-sn 3497 df-n0 8876 |
This theorem is referenced by: 0xnn0 8944 elnn0z 8965 nn0ind-raph 9066 10nn0 9097 declei 9115 numlti 9116 nummul1c 9128 decaddc2 9135 decrmanc 9136 decrmac 9137 decaddm10 9138 decaddi 9139 decaddci 9140 decaddci2 9141 decmul1 9143 decmulnc 9146 6p5e11 9152 7p4e11 9155 8p3e11 9160 9p2e11 9166 10p10e20 9174 fz01or 9778 0elfz 9785 4fvwrd4 9804 fvinim0ffz 9905 0tonninf 10099 exple1 10236 sq10 10346 bc0k 10389 bcn1 10391 bccl 10400 fihasheq0 10427 fsumnn0cl 11058 binom 11139 bcxmas 11144 isumnn0nn 11148 geoserap 11162 ef0lem 11211 ege2le3 11222 ef4p 11245 efgt1p2 11246 efgt1p 11247 nn0o 11446 ndvdssub 11469 gcdval 11490 gcdcl 11497 dfgcd3 11538 nn0seqcvgd 11562 algcvg 11569 eucalg 11580 lcmcl 11593 pw2dvdslemn 11682 ennnfonelemj0 11753 ennnfonelem0 11757 ennnfonelem1 11759 1kp2ke3k 12620 ex-fac 12624 isomninnlem 12906 |
Copyright terms: Public domain | W3C validator |