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 8980 | . 2 | |
2 | nnnn0d.1 | . 2 | |
3 | 1, 2 | sseldi 3095 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cn 8720 cn0 8977 |
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 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-n0 8978 |
This theorem is referenced by: nn0ge2m1nn0 9038 nnzd 9172 eluzge2nn0 9365 modsumfzodifsn 10169 addmodlteq 10171 expnnval 10296 expgt1 10331 expaddzaplem 10336 expaddzap 10337 expmulzap 10339 expnbnd 10415 facwordi 10486 faclbnd 10487 facavg 10492 bcm1k 10506 bcval5 10509 1elfz0hash 10552 resqrexlemnm 10790 resqrexlemcvg 10791 summodc 11152 zsumdc 11153 bcxmas 11258 geo2sum 11283 geo2lim 11285 geoisum1 11288 geoisum1c 11289 cvgratnnlembern 11292 cvgratnnlemsumlt 11297 cvgratnnlemfm 11298 mertenslemi1 11304 prodmodclem3 11344 prodmodclem2a 11345 eftabs 11362 efcllemp 11364 eftlub 11396 eirraplem 11483 dvdsfac 11558 divalglemnqt 11617 divalglemeunn 11618 gcdval 11648 gcdcl 11655 dvdsgcdidd 11682 mulgcd 11704 rplpwr 11715 rppwr 11716 lcmcl 11753 lcmgcdnn 11763 nprmdvds1 11820 rpexp 11831 pw2dvdslemn 11843 sqpweven 11853 2sqpwodd 11854 nn0sqrtelqelz 11884 phiprmpw 11898 crth 11900 cvgcmp2nlemabs 13227 trilpolemlt1 13234 |
Copyright terms: Public domain | W3C validator |