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 syl6bbr ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑃𝐾 ) ) ↔ 𝑝 ∈ { 𝑃 } ) )
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 ‘ 𝑃 ) )