Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nnnn0d | GIF version |
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnnn0d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
Ref | Expression |
---|---|
nnnn0d | ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssnn0 9111 | . 2 ⊢ ℕ ⊆ ℕ0 | |
2 | nnnn0d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
3 | 1, 2 | sselid 3138 | 1 ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 ℕcn 8851 ℕ0cn0 9108 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2726 df-un 3118 df-in 3120 df-ss 3127 df-n0 9109 |
This theorem is referenced by: nn0ge2m1nn0 9169 nnzd 9306 eluzge2nn0 9501 modsumfzodifsn 10325 addmodlteq 10327 expnnval 10452 expgt1 10487 expaddzaplem 10492 expaddzap 10493 expmulzap 10495 expnbnd 10572 facwordi 10647 faclbnd 10648 facavg 10653 bcm1k 10667 bcval5 10670 1elfz0hash 10713 resqrexlemnm 10954 resqrexlemcvg 10955 summodc 11318 zsumdc 11319 bcxmas 11424 geo2sum 11449 geo2lim 11451 geoisum1 11454 geoisum1c 11455 cvgratnnlembern 11458 cvgratnnlemsumlt 11463 cvgratnnlemfm 11464 mertenslemi1 11470 prodmodclem3 11510 prodmodclem2a 11511 zproddc 11514 fprodseq 11518 eftabs 11591 efcllemp 11593 eftlub 11625 eirraplem 11711 dvdsfac 11792 divalglemnqt 11851 divalglemeunn 11852 gcdval 11886 gcdcl 11893 dvdsgcdidd 11921 mulgcd 11943 rplpwr 11954 rppwr 11955 lcmcl 11998 lcmgcdnn 12008 nprmdvds1 12066 isprm5lem 12067 rpexp 12079 pw2dvdslemn 12091 sqpweven 12101 2sqpwodd 12102 nn0sqrtelqelz 12132 phiprmpw 12148 crth 12150 eulerthlema 12156 eulerthlemth 12158 eulerth 12159 fermltl 12160 odzcllem 12168 odzdvds 12171 odzphi 12172 modprm0 12180 prm23lt5 12189 pythagtriplem6 12196 pythagtriplem7 12197 pcprmpw2 12258 dvdsprmpweqle 12262 pcprod 12270 pcfac 12274 pcbc 12275 expnprm 12277 pockthlem 12280 pockthg 12281 prmunb 12286 mul4sqlem 12317 logbgcd1irraplemexp 13484 cvgcmp2nlemabs 13804 trilpolemlt1 13813 redcwlpolemeq1 13826 nconstwlpolem0 13834 |
Copyright terms: Public domain | W3C validator |