Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elnn0 | Unicode version |
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
elnn0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 9096 | . . 3 | |
2 | 1 | eleq2i 2224 | . 2 |
3 | elun 3249 | . 2 | |
4 | c0ex 7874 | . . . 4 | |
5 | 4 | elsn2 3595 | . . 3 |
6 | 5 | orbi2i 752 | . 2 |
7 | 2, 3, 6 | 3bitri 205 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 698 wceq 1335 wcel 2128 cun 3100 csn 3561 cc0 7734 cn 8838 cn0 9095 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-1cn 7827 ax-icn 7829 ax-addcl 7830 ax-mulcl 7832 ax-i2m1 7839 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 df-un 3106 df-sn 3567 df-n0 9096 |
This theorem is referenced by: 0nn0 9110 nn0ge0 9120 nnnn0addcl 9125 nnm1nn0 9136 elnnnn0b 9139 elnn0z 9185 elznn0nn 9186 elznn0 9187 elznn 9188 nn0ind-raph 9286 nn0ledivnn 9680 expp1 10435 expnegap0 10436 expcllem 10439 nn0ltexp2 10595 facp1 10615 faclbnd 10626 faclbnd3 10628 bcn1 10643 bcval5 10648 hashnncl 10681 fz1f1o 11283 arisum 11406 arisum2 11407 fprodfac 11523 ef0lem 11568 nn0enne 11805 nn0o1gt2 11808 dfgcd2 11913 mulgcd 11915 eucalgf 11947 eucalginv 11948 prmdvdsexpr 12040 rpexp1i 12044 nn0gcdsq 12090 odzdvds 12135 dvexp2 13146 |
Copyright terms: Public domain | W3C validator |