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 12063 | . 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 {crab 2452 class class class wbr 3989 2oc2o 6389 ≈ cen 6716 ℕcn 8878 ∥ cdvds 11749 ℙcprime 12061 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rab 2457 df-v 2732 df-un 3125 df-sn 3589 df-pr 3590 df-op 3592 df-br 3990 df-prm 12062 |
This theorem is referenced by: prmz 12065 prmssnn 12066 nprmdvds1 12094 isprm5lem 12095 isprm5 12096 coprm 12098 euclemma 12100 prmdvdsexpr 12104 cncongrprm 12111 phiprmpw 12176 fermltl 12188 prmdiv 12189 prmdiveq 12190 prmdivdiv 12191 m1dvdsndvds 12202 vfermltl 12205 powm2modprm 12206 reumodprminv 12207 modprm0 12208 nnnn0modprm0 12209 modprmn0modprm0 12210 oddprm 12213 nnoddn2prm 12214 prm23lt5 12217 pcpremul 12247 pcdvdsb 12273 pcelnn 12274 pcidlem 12276 pcid 12277 pcdvdstr 12280 pcgcd1 12281 pcprmpw2 12286 dvdsprmpweqnn 12289 dvdsprmpweqle 12290 pcaddlem 12292 pcadd 12293 pcmptcl 12294 pcmpt 12295 pcmpt2 12296 pcfaclem 12301 pcfac 12302 pcbc 12303 expnprm 12305 oddprmdvds 12306 prmpwdvds 12307 pockthlem 12308 pockthg 12309 pockthi 12310 1arith 12319 lgslem1 13695 lgslem4 13698 lgsval 13699 lgsval2lem 13705 lgsvalmod 13714 lgsmod 13721 lgsdirprm 13729 lgsne0 13733 lgsprme0 13737 2sqlem3 13747 2sqlem8 13753 |
Copyright terms: Public domain | W3C validator |