![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnnn0 | GIF version |
Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
nnnn0 | ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssnn0 8774 | . 2 ⊢ ℕ ⊆ ℕ0 | |
2 | 1 | sseli 3035 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ℕcn 8520 ℕ0cn0 8771 |
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 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-n0 8772 |
This theorem is referenced by: nnnn0i 8779 elnnnn0b 8815 elnnnn0c 8816 elnn0z 8861 elz2 8916 nn0ind-raph 8962 zindd 8963 fzo1fzo0n0 9743 ubmelfzo 9760 elfzom1elp1fzo 9762 fzo0sn0fzo1 9781 modqmulnn 9898 expnegap0 10078 expcllem 10081 expcl2lemap 10082 expap0 10100 expeq0 10101 mulexpzap 10110 expnlbnd 10193 facdiv 10261 faclbnd 10264 faclbnd3 10266 faclbnd6 10267 resqrexlemlo 10561 absexpzap 10628 isummolemnm 10922 summodclem2a 10924 fsum3 10930 arisum 11041 expcnvap0 11045 expcnv 11047 geo2sum 11057 geo2lim 11059 geoisum1c 11063 0.999... 11064 mertenslem2 11079 ef0lem 11099 ege2le3 11110 efaddlem 11113 efexp 11121 nn0enne 11329 nnehalf 11331 nno 11333 nn0o 11334 divalg2 11353 ndvdssub 11357 gcddiv 11435 gcdmultiple 11436 gcdmultiplez 11437 rpmulgcd 11442 rplpwr 11443 dvdssqlem 11446 eucalgf 11464 1nprm 11523 isprm6 11553 prmdvdsexp 11554 pw2dvds 11571 oddpwdc 11579 phicl2 11617 phibndlem 11619 phiprmpw 11625 crth 11627 hashgcdlem 11630 |
Copyright terms: Public domain | W3C validator |