# Metamath Proof Explorer

## Theorem vmappw

Description: Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmappw ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \Lambda \left({{P}}^{{K}}\right)=\mathrm{log}{P}$

### Proof

Step Hyp Ref Expression
1 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
2 nnnn0 ${⊢}{K}\in ℕ\to {K}\in {ℕ}_{0}$
3 nnexpcl ${⊢}\left({P}\in ℕ\wedge {K}\in {ℕ}_{0}\right)\to {{P}}^{{K}}\in ℕ$
4 1 2 3 syl2an ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to {{P}}^{{K}}\in ℕ$
5 eqid ${⊢}\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}=\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}$
6 5 vmaval ${⊢}{{P}}^{{K}}\in ℕ\to \Lambda \left({{P}}^{{K}}\right)=if\left(\left|\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}\right|=1,\mathrm{log}\bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\},0\right)$
7 4 6 syl ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \Lambda \left({{P}}^{{K}}\right)=if\left(\left|\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}\right|=1,\mathrm{log}\bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\},0\right)$
8 df-rab ${⊢}\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}=\left\{{p}|\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)\right\}$
9 prmdvdsexpb ${⊢}\left({p}\in ℙ\wedge {P}\in ℙ\wedge {K}\in ℕ\right)\to \left({p}\parallel {{P}}^{{K}}↔{p}={P}\right)$
10 9 biimpd ${⊢}\left({p}\in ℙ\wedge {P}\in ℙ\wedge {K}\in ℕ\right)\to \left({p}\parallel {{P}}^{{K}}\to {p}={P}\right)$
11 10 3coml ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\wedge {p}\in ℙ\right)\to \left({p}\parallel {{P}}^{{K}}\to {p}={P}\right)$
12 11 3expa ${⊢}\left(\left({P}\in ℙ\wedge {K}\in ℕ\right)\wedge {p}\in ℙ\right)\to \left({p}\parallel {{P}}^{{K}}\to {p}={P}\right)$
13 12 expimpd ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left(\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)\to {p}={P}\right)$
14 simpl ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to {P}\in ℙ$
15 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
16 iddvdsexp ${⊢}\left({P}\in ℤ\wedge {K}\in ℕ\right)\to {P}\parallel {{P}}^{{K}}$
17 15 16 sylan ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to {P}\parallel {{P}}^{{K}}$
18 14 17 jca ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left({P}\in ℙ\wedge {P}\parallel {{P}}^{{K}}\right)$
19 eleq1 ${⊢}{p}={P}\to \left({p}\in ℙ↔{P}\in ℙ\right)$
20 breq1 ${⊢}{p}={P}\to \left({p}\parallel {{P}}^{{K}}↔{P}\parallel {{P}}^{{K}}\right)$
21 19 20 anbi12d ${⊢}{p}={P}\to \left(\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)↔\left({P}\in ℙ\wedge {P}\parallel {{P}}^{{K}}\right)\right)$
22 18 21 syl5ibrcom ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left({p}={P}\to \left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)\right)$
23 13 22 impbid ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left(\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)↔{p}={P}\right)$
24 velsn ${⊢}{p}\in \left\{{P}\right\}↔{p}={P}$
25 23 24 syl6bbr ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left(\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)↔{p}\in \left\{{P}\right\}\right)$
26 25 abbi1dv ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left\{{p}|\left({p}\in ℙ\wedge {p}\parallel {{P}}^{{K}}\right)\right\}=\left\{{P}\right\}$
27 8 26 syl5eq ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}=\left\{{P}\right\}$
28 27 fveq2d ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left|\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}\right|=\left|\left\{{P}\right\}\right|$
29 hashsng ${⊢}{P}\in ℙ\to \left|\left\{{P}\right\}\right|=1$
30 29 adantr ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left|\left\{{P}\right\}\right|=1$
31 28 30 eqtrd ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \left|\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}\right|=1$
32 31 iftrued ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to if\left(\left|\left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}\right|=1,\mathrm{log}\bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\},0\right)=\mathrm{log}\bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}$
33 27 unieqd ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}=\bigcup \left\{{P}\right\}$
34 unisng ${⊢}{P}\in ℙ\to \bigcup \left\{{P}\right\}={P}$
35 34 adantr ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \bigcup \left\{{P}\right\}={P}$
36 33 35 eqtrd ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}={P}$
37 36 fveq2d ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \mathrm{log}\bigcup \left\{{p}\in ℙ|{p}\parallel {{P}}^{{K}}\right\}=\mathrm{log}{P}$
38 7 32 37 3eqtrd ${⊢}\left({P}\in ℙ\wedge {K}\in ℕ\right)\to \Lambda \left({{P}}^{{K}}\right)=\mathrm{log}{P}$