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 ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( Λ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( log ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
3 nnexpcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
4 1 2 3 syl2an ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
5 eqid ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) }
6 5 vmaval ⊢ ( ( 𝑃 ↑ 𝐾 ) ∈ ℕ → ( Λ ‘ ( 𝑃 ↑ 𝐾 ) ) = if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) , 0 ) )
7 4 6 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( Λ ‘ ( 𝑃 ↑ 𝐾 ) ) = if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) , 0 ) )
8 df-rab ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } = { 𝑝 ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) }
9 prmdvdsexpb ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ↔ 𝑝 = 𝑃 ) )
10 9 biimpd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) → 𝑝 = 𝑃 ) )
11 10 3coml ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) → 𝑝 = 𝑃 ) )
12 11 3expa ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) → 𝑝 = 𝑃 ) )
13 12 expimpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) → 𝑝 = 𝑃 ) )
14 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∈ ℙ )
15 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
16 iddvdsexp ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∥ ( 𝑃 ↑ 𝐾 ) )
17 15 16 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∥ ( 𝑃 ↑ 𝐾 ) )
18 14 17 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝑃 ↑ 𝐾 ) ) )
19 eleq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ ℙ ↔ 𝑃 ∈ ℙ ) )
20 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ↔ 𝑃 ∥ ( 𝑃 ↑ 𝐾 ) ) )
21 19 20 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝑃 ↑ 𝐾 ) ) ) )
22 18 21 syl5ibrcom ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑝 = 𝑃 → ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) ) )
23 13 22 impbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) ↔ 𝑝 = 𝑃 ) )
24 velsn ⊢ ( 𝑝 ∈ { 𝑃 } ↔ 𝑝 = 𝑃 )
25 23 24 bitr4di ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) ↔ 𝑝 ∈ { 𝑃 } ) )
26 25 abbi1dv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → { 𝑝 ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) ) } = { 𝑃 } )
27 8 26 syl5eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } = { 𝑃 } )
28 27 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = ( ♯ ‘ { 𝑃 } ) )
29 hashsng ⊢ ( 𝑃 ∈ ℙ → ( ♯ ‘ { 𝑃 } ) = 1 )
30 29 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑃 } ) = 1 )
31 28 30 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = 1 )
32 31 iftrued ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) , 0 ) = ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) )
33 27 unieqd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } = ∪ { 𝑃 } )
34 unisng ⊢ ( 𝑃 ∈ ℙ → ∪ { 𝑃 } = 𝑃 )
35 34 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∪ { 𝑃 } = 𝑃 )
36 33 35 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } = 𝑃 )
37 36 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝑃 ↑ 𝐾 ) } ) = ( log ‘ 𝑃 ) )
38 7 32 37 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( Λ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( log ‘ 𝑃 ) )