![]() |
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 10094 expcllem 10097 expcl2lemap 10098 expap0 10116 expeq0 10117 mulexpzap 10126 expnlbnd 10209 facdiv 10277 faclbnd 10280 faclbnd3 10282 faclbnd6 10283 resqrexlemlo 10577 absexpzap 10644 isummolemnm 10937 summodclem2a 10939 fsum3 10945 arisum 11056 expcnvap0 11060 expcnv 11062 geo2sum 11072 geo2lim 11074 geoisum1c 11078 0.999... 11079 mertenslem2 11094 ef0lem 11114 ege2le3 11125 efaddlem 11128 efexp 11136 nn0enne 11344 nnehalf 11346 nno 11348 nn0o 11349 divalg2 11368 ndvdssub 11372 gcddiv 11450 gcdmultiple 11451 gcdmultiplez 11452 rpmulgcd 11457 rplpwr 11458 dvdssqlem 11461 eucalgf 11479 1nprm 11538 isprm6 11568 prmdvdsexp 11569 pw2dvds 11586 oddpwdc 11594 phicl2 11632 phibndlem 11634 phiprmpw 11640 crth 11642 hashgcdlem 11645 |
Copyright terms: Public domain | W3C validator |