![]() |
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 9210 | . 2 ⊢ ℕ ⊆ ℕ0 | |
2 | 1 | sseli 3166 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ℕcn 8950 ℕ0cn0 9207 |
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 9208 |
This theorem is referenced by: nnnn0i 9215 elnnnn0b 9251 elnnnn0c 9252 elnn0z 9297 elz2 9355 nn0ind-raph 9401 zindd 9402 fzo1fzo0n0 10215 ubmelfzo 10232 elfzom1elp1fzo 10234 fzo0sn0fzo1 10253 modqmulnn 10375 expnegap0 10562 expcllem 10565 expcl2lemap 10566 expap0 10584 expeq0 10585 mulexpzap 10594 expnlbnd 10679 apexp1 10733 facdiv 10753 faclbnd 10756 faclbnd3 10758 faclbnd6 10759 resqrexlemlo 11057 absexpzap 11124 nnf1o 11419 summodclem2a 11424 fsum3 11430 arisum 11541 expcnvap0 11545 expcnv 11547 geo2sum 11557 geo2lim 11559 geoisum1c 11563 0.999... 11564 mertenslem2 11579 fprodseq 11626 fprodfac 11658 ef0lem 11703 ege2le3 11714 efaddlem 11717 efexp 11725 dvdsmodexp 11837 nn0enne 11942 nnehalf 11944 nno 11946 nn0o 11947 divalg2 11966 ndvdssub 11970 gcddiv 12055 gcdmultiple 12056 gcdmultiplez 12057 rpmulgcd 12062 rplpwr 12063 dvdssqlem 12066 eucalgf 12090 1nprm 12149 isprm6 12182 prmdvdsexp 12183 pw2dvds 12201 oddpwdc 12209 phicl2 12249 phibndlem 12251 phiprmpw 12257 crth 12259 hashgcdlem 12273 phisum 12275 pythagtriplem10 12304 pythagtriplem6 12305 pythagtriplem7 12306 pythagtriplem12 12310 pythagtriplem14 12312 pclemub 12322 pcexp 12344 pcid 12359 pcprod 12381 pcbc 12386 prmpwdvds 12390 infpnlem1 12394 infpnlem2 12395 prmunb 12397 1arith 12402 ennnfonelemjn 12456 ghmmulg 13212 dvexp 14652 logbgcd1irr 14862 lgsval4a 14901 |
Copyright terms: Public domain | W3C validator |