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 8973 | . 2 ⊢ ℕ ⊆ ℕ0 | |
2 | 1 | sseli 3088 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 ℕcn 8713 ℕ0cn0 8970 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-un 3070 df-in 3072 df-ss 3079 df-n0 8971 |
This theorem is referenced by: nnnn0i 8978 elnnnn0b 9014 elnnnn0c 9015 elnn0z 9060 elz2 9115 nn0ind-raph 9161 zindd 9162 fzo1fzo0n0 9953 ubmelfzo 9970 elfzom1elp1fzo 9972 fzo0sn0fzo1 9991 modqmulnn 10108 expnegap0 10294 expcllem 10297 expcl2lemap 10298 expap0 10316 expeq0 10317 mulexpzap 10326 expnlbnd 10409 facdiv 10477 faclbnd 10480 faclbnd3 10482 faclbnd6 10483 resqrexlemlo 10778 absexpzap 10845 isummolemnm 11141 summodclem2a 11143 fsum3 11149 arisum 11260 expcnvap0 11264 expcnv 11266 geo2sum 11276 geo2lim 11278 geoisum1c 11282 0.999... 11283 mertenslem2 11298 ef0lem 11355 ege2le3 11366 efaddlem 11369 efexp 11377 nn0enne 11588 nnehalf 11590 nno 11592 nn0o 11593 divalg2 11612 ndvdssub 11616 gcddiv 11696 gcdmultiple 11697 gcdmultiplez 11698 rpmulgcd 11703 rplpwr 11704 dvdssqlem 11707 eucalgf 11725 1nprm 11784 isprm6 11814 prmdvdsexp 11815 pw2dvds 11833 oddpwdc 11841 phicl2 11879 phibndlem 11881 phiprmpw 11887 crth 11889 hashgcdlem 11892 ennnfonelemjn 11904 dvexp 12833 |
Copyright terms: Public domain | W3C validator |