![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnnn0 | Unicode version |
Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
nnnn0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssnn0 8832 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3043 |
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 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-un 3025 df-in 3027 df-ss 3034 df-n0 8830 |
This theorem is referenced by: nnnn0i 8837 elnnnn0b 8873 elnnnn0c 8874 elnn0z 8919 elz2 8974 nn0ind-raph 9020 zindd 9021 fzo1fzo0n0 9801 ubmelfzo 9818 elfzom1elp1fzo 9820 fzo0sn0fzo1 9839 modqmulnn 9956 expnegap0 10142 expcllem 10145 expcl2lemap 10146 expap0 10164 expeq0 10165 mulexpzap 10174 expnlbnd 10257 facdiv 10325 faclbnd 10328 faclbnd3 10330 faclbnd6 10331 resqrexlemlo 10625 absexpzap 10692 isummolemnm 10987 summodclem2a 10989 fsum3 10995 arisum 11106 expcnvap0 11110 expcnv 11112 geo2sum 11122 geo2lim 11124 geoisum1c 11128 0.999... 11129 mertenslem2 11144 ef0lem 11164 ege2le3 11175 efaddlem 11178 efexp 11186 nn0enne 11394 nnehalf 11396 nno 11398 nn0o 11399 divalg2 11418 ndvdssub 11422 gcddiv 11500 gcdmultiple 11501 gcdmultiplez 11502 rpmulgcd 11507 rplpwr 11508 dvdssqlem 11511 eucalgf 11529 1nprm 11588 isprm6 11618 prmdvdsexp 11619 pw2dvds 11636 oddpwdc 11644 phicl2 11682 phibndlem 11684 phiprmpw 11690 crth 11692 hashgcdlem 11695 ennnfonelemjn 11707 |
Copyright terms: Public domain | W3C validator |