0nn0 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 0nn0		Unicode version

Theorem 0nn0 8985

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

**Assertion**
Ref	Expression
0nn0

**Proof of Theorem 0nn0**
Step	Hyp	Ref	Expression
1		eqid 2137	. 2
2		elnn0 8972	. . . 4 $\/$
3	2	biimpri 132	. . 3 $\/$
4	3	olcs 725	. 2
5	1, 4	ax-mp 5	1

Colors of variables: wff set class

Syntax hints: $\/$ wo 697

wceq 1331

wcel 1480

cc0 7613

cn 8713

cn0 8970

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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-1cn 7706 ax-icn 7708 ax-addcl 7709 ax-mulcl 7711 ax-i2m1 7718

This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-un 3070 df-sn 3528 df-n0 8971

This theorem is referenced by: 0xnn0 9039 elnn0z 9060 nn0ind-raph 9161 10nn0 9192 declei 9210 numlti 9211 nummul1c 9223 decaddc2 9230 decrmanc 9231 decrmac 9232 decaddm10 9233 decaddi 9234 decaddci 9235 decaddci2 9236 decmul1 9238 decmulnc 9241 6p5e11 9247 7p4e11 9250 8p3e11 9255 9p2e11 9261 10p10e20 9269 fz01or 9884 0elfz 9891 4fvwrd4 9910 fvinim0ffz 10011 0tonninf 10205 exple1 10342 sq10 10452 bc0k 10495 bcn1 10497 bccl 10506 fihasheq0 10533 fsumnn0cl 11165 binom 11246 bcxmas 11251 isumnn0nn 11255 geoserap 11269 ef0lem 11355 ege2le3 11366 ef4p 11389 efgt1p2 11390 efgt1p 11391 nn0o 11593 ndvdssub 11616 gcdval 11637 gcdcl 11644 dfgcd3 11687 nn0seqcvgd 11711 algcvg 11718 eucalg 11729 lcmcl 11742 pw2dvdslemn 11832 ennnfonelemj0 11903 ennnfonelem0 11907 ennnfonelem1 11909 dveflem 12844 pilem3 12853 1kp2ke3k 12925 ex-fac 12929 isomninnlem 13214