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 9108 | . 2 | |
2 | nnnn0d.1 | . 2 | |
3 | 1, 2 | sseldi 3135 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2135 cn 8848 cn0 9105 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-n0 9106 |
This theorem is referenced by: nn0ge2m1nn0 9166 nnzd 9303 eluzge2nn0 9498 modsumfzodifsn 10321 addmodlteq 10323 expnnval 10448 expgt1 10483 expaddzaplem 10488 expaddzap 10489 expmulzap 10491 expnbnd 10567 facwordi 10642 faclbnd 10643 facavg 10648 bcm1k 10662 bcval5 10665 1elfz0hash 10708 resqrexlemnm 10946 resqrexlemcvg 10947 summodc 11310 zsumdc 11311 bcxmas 11416 geo2sum 11441 geo2lim 11443 geoisum1 11446 geoisum1c 11447 cvgratnnlembern 11450 cvgratnnlemsumlt 11455 cvgratnnlemfm 11456 mertenslemi1 11462 prodmodclem3 11502 prodmodclem2a 11503 zproddc 11506 fprodseq 11510 eftabs 11583 efcllemp 11585 eftlub 11617 eirraplem 11703 dvdsfac 11783 divalglemnqt 11842 divalglemeunn 11843 gcdval 11877 gcdcl 11884 dvdsgcdidd 11912 mulgcd 11934 rplpwr 11945 rppwr 11946 lcmcl 11983 lcmgcdnn 11993 nprmdvds1 12051 rpexp 12062 pw2dvdslemn 12074 sqpweven 12084 2sqpwodd 12085 nn0sqrtelqelz 12115 phiprmpw 12131 crth 12133 eulerthlema 12139 eulerthlemth 12141 eulerth 12142 fermltl 12143 odzcllem 12151 odzdvds 12154 odzphi 12155 modprm0 12163 prm23lt5 12172 pythagtriplem6 12179 pythagtriplem7 12180 pcprmpw2 12241 dvdsprmpweqle 12245 pcprod 12253 pcfac 12257 pcbc 12258 expnprm 12260 logbgcd1irraplemexp 13427 cvgcmp2nlemabs 13745 trilpolemlt1 13754 redcwlpolemeq1 13767 nconstwlpolem0 13775 |
Copyright terms: Public domain | W3C validator |