Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > prmnn | GIF version |
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
prmnn | ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isprm 12030 | . 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 {crab 2446 class class class wbr 3977 2oc2o 6370 ≈ cen 6696 ℕcn 8849 ∥ cdvds 11717 ℙcprime 12028 |
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-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rab 2451 df-v 2724 df-un 3116 df-sn 3577 df-pr 3578 df-op 3580 df-br 3978 df-prm 12029 |
This theorem is referenced by: prmz 12032 prmssnn 12033 nprmdvds1 12061 isprm5lem 12062 isprm5 12063 coprm 12065 euclemma 12067 prmdvdsexpr 12071 cncongrprm 12078 phiprmpw 12143 fermltl 12155 prmdiv 12156 prmdiveq 12157 prmdivdiv 12158 m1dvdsndvds 12169 vfermltl 12172 powm2modprm 12173 reumodprminv 12174 modprm0 12175 nnnn0modprm0 12176 modprmn0modprm0 12177 oddprm 12180 nnoddn2prm 12181 prm23lt5 12184 pcpremul 12214 pcdvdsb 12240 pcelnn 12241 pcidlem 12243 pcid 12244 pcdvdstr 12247 pcgcd1 12248 pcprmpw2 12253 dvdsprmpweqnn 12256 dvdsprmpweqle 12257 pcaddlem 12259 pcadd 12260 pcmptcl 12261 pcmpt 12262 pcmpt2 12263 pcfaclem 12268 pcfac 12269 pcbc 12270 expnprm 12272 oddprmdvds 12273 prmpwdvds 12274 pockthlem 12275 pockthg 12276 pockthi 12277 1arith 12286 |
Copyright terms: Public domain | W3C validator |