![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnnn0d | Unicode version |
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnnn0d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nnnn0d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssnn0 8832 |
. 2
![]() ![]() ![]() ![]() | |
2 | nnnn0d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseldi 3045 |
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: nn0ge2m1nn0 8890 nnzd 9024 eluzge2nn0 9215 modsumfzodifsn 10010 addmodlteq 10012 expnnval 10137 expgt1 10172 expaddzaplem 10177 expaddzap 10178 expmulzap 10180 expnbnd 10256 facwordi 10327 faclbnd 10328 facavg 10333 bcm1k 10347 bcval5 10350 1elfz0hash 10393 resqrexlemnm 10630 resqrexlemcvg 10631 summodc 10991 zsumdc 10992 bcxmas 11097 geo2sum 11122 geo2lim 11124 geoisum1 11127 geoisum1c 11128 cvgratnnlembern 11131 cvgratnnlemsumlt 11136 cvgratnnlemfm 11137 mertenslemi1 11143 eftabs 11160 efcllemp 11162 eftlub 11194 eirraplem 11278 dvdsfac 11353 divalglemnqt 11412 divalglemeunn 11413 gcdval 11443 gcdcl 11450 mulgcd 11497 rplpwr 11508 rppwr 11509 lcmcl 11546 lcmgcdnn 11556 nprmdvds1 11613 rpexp 11624 pw2dvdslemn 11635 sqpweven 11645 2sqpwodd 11646 nn0sqrtelqelz 11676 phiprmpw 11690 crth 11692 cvgcmp2nlemabs 12811 trilpolemlt1 12818 |
Copyright terms: Public domain | W3C validator |