![]() |
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 9208 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3166 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-n0 9206 |
This theorem is referenced by: nnnn0i 9213 elnnnn0b 9249 elnnnn0c 9250 elnn0z 9295 elz2 9353 nn0ind-raph 9399 zindd 9400 fzo1fzo0n0 10212 ubmelfzo 10229 elfzom1elp1fzo 10231 fzo0sn0fzo1 10250 modqmulnn 10372 expnegap0 10558 expcllem 10561 expcl2lemap 10562 expap0 10580 expeq0 10581 mulexpzap 10590 expnlbnd 10675 apexp1 10729 facdiv 10749 faclbnd 10752 faclbnd3 10754 faclbnd6 10755 resqrexlemlo 11053 absexpzap 11120 nnf1o 11415 summodclem2a 11420 fsum3 11426 arisum 11537 expcnvap0 11541 expcnv 11543 geo2sum 11553 geo2lim 11555 geoisum1c 11559 0.999... 11560 mertenslem2 11575 fprodseq 11622 fprodfac 11654 ef0lem 11699 ege2le3 11710 efaddlem 11713 efexp 11721 dvdsmodexp 11833 nn0enne 11938 nnehalf 11940 nno 11942 nn0o 11943 divalg2 11962 ndvdssub 11966 gcddiv 12051 gcdmultiple 12052 gcdmultiplez 12053 rpmulgcd 12058 rplpwr 12059 dvdssqlem 12062 eucalgf 12086 1nprm 12145 isprm6 12178 prmdvdsexp 12179 pw2dvds 12197 oddpwdc 12205 phicl2 12245 phibndlem 12247 phiprmpw 12253 crth 12255 hashgcdlem 12269 phisum 12271 pythagtriplem10 12300 pythagtriplem6 12301 pythagtriplem7 12302 pythagtriplem12 12306 pythagtriplem14 12308 pclemub 12318 pcexp 12340 pcid 12355 pcprod 12377 pcbc 12382 prmpwdvds 12386 infpnlem1 12390 infpnlem2 12391 prmunb 12393 1arith 12398 ennnfonelemjn 12452 ghmmulg 13192 dvexp 14627 logbgcd1irr 14837 lgsval4a 14876 |
Copyright terms: Public domain | W3C validator |