vmappw

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

		Ref	Expression
	Assertion	vmappw	$⊢ (P \in ℙ \land K \in ℕ) \to Λ (P^{K}) = \log P$

Proof

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

Metamath Proof Explorer

Theorem vmappw

Proof