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 
|- ( ( P e. Prime /\ K e. NN ) -> ( Lam ` ( P ^ K ) ) = ( log ` P ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
3 nnexpcl 
 |-  ( ( P e. NN /\ K e. NN0 ) -> ( P ^ K ) e. NN )
4 1 2 3 syl2an 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. NN )
5 eqid 
 |-  { p e. Prime | p || ( P ^ K ) } = { p e. Prime | p || ( P ^ K ) }
6 5 vmaval 
 |-  ( ( P ^ K ) e. NN -> ( Lam ` ( P ^ K ) ) = if ( ( # ` { p e. Prime | p || ( P ^ K ) } ) = 1 , ( log ` U. { p e. Prime | p || ( P ^ K ) } ) , 0 ) )
7 4 6 syl 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( Lam ` ( P ^ K ) ) = if ( ( # ` { p e. Prime | p || ( P ^ K ) } ) = 1 , ( log ` U. { p e. Prime | p || ( P ^ K ) } ) , 0 ) )
8 df-rab 
 |-  { p e. Prime | p || ( P ^ K ) } = { p | ( p e. Prime /\ p || ( P ^ K ) ) }
9 prmdvdsexpb 
 |-  ( ( p e. Prime /\ P e. Prime /\ K e. NN ) -> ( p || ( P ^ K ) <-> p = P ) )
10 9 biimpd 
 |-  ( ( p e. Prime /\ P e. Prime /\ K e. NN ) -> ( p || ( P ^ K ) -> p = P ) )
11 10 3coml 
 |-  ( ( P e. Prime /\ K e. NN /\ p e. Prime ) -> ( p || ( P ^ K ) -> p = P ) )
12 11 3expa 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ p e. Prime ) -> ( p || ( P ^ K ) -> p = P ) )
13 12 expimpd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( p e. Prime /\ p || ( P ^ K ) ) -> p = P ) )
14 simpl 
 |-  ( ( P e. Prime /\ K e. NN ) -> P e. Prime )
15 prmz 
 |-  ( P e. Prime -> P e. ZZ )
16 iddvdsexp 
 |-  ( ( P e. ZZ /\ K e. NN ) -> P || ( P ^ K ) )
17 15 16 sylan 
 |-  ( ( P e. Prime /\ K e. NN ) -> P || ( P ^ K ) )
18 14 17 jca 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P e. Prime /\ P || ( P ^ K ) ) )
19 eleq1 
 |-  ( p = P -> ( p e. Prime <-> P e. Prime ) )
20 breq1 
 |-  ( p = P -> ( p || ( P ^ K ) <-> P || ( P ^ K ) ) )
21 19 20 anbi12d 
 |-  ( p = P -> ( ( p e. Prime /\ p || ( P ^ K ) ) <-> ( P e. Prime /\ P || ( P ^ K ) ) ) )
22 18 21 syl5ibrcom 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( p = P -> ( p e. Prime /\ p || ( P ^ K ) ) ) )
23 13 22 impbid 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( p e. Prime /\ p || ( P ^ K ) ) <-> p = P ) )
24 velsn 
 |-  ( p e. { P } <-> p = P )
25 23 24 bitr4di 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( p e. Prime /\ p || ( P ^ K ) ) <-> p e. { P } ) )
26 25 abbi1dv 
 |-  ( ( P e. Prime /\ K e. NN ) -> { p | ( p e. Prime /\ p || ( P ^ K ) ) } = { P } )
27 8 26 syl5eq 
 |-  ( ( P e. Prime /\ K e. NN ) -> { p e. Prime | p || ( P ^ K ) } = { P } )
28 27 fveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { p e. Prime | p || ( P ^ K ) } ) = ( # ` { P } ) )
29 hashsng 
 |-  ( P e. Prime -> ( # ` { P } ) = 1 )
30 29 adantr 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { P } ) = 1 )
31 28 30 eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { p e. Prime | p || ( P ^ K ) } ) = 1 )
32 31 iftrued 
 |-  ( ( P e. Prime /\ K e. NN ) -> if ( ( # ` { p e. Prime | p || ( P ^ K ) } ) = 1 , ( log ` U. { p e. Prime | p || ( P ^ K ) } ) , 0 ) = ( log ` U. { p e. Prime | p || ( P ^ K ) } ) )
33 27 unieqd 
 |-  ( ( P e. Prime /\ K e. NN ) -> U. { p e. Prime | p || ( P ^ K ) } = U. { P } )
34 unisng 
 |-  ( P e. Prime -> U. { P } = P )
35 34 adantr 
 |-  ( ( P e. Prime /\ K e. NN ) -> U. { P } = P )
36 33 35 eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> U. { p e. Prime | p || ( P ^ K ) } = P )
37 36 fveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( log ` U. { p e. Prime | p || ( P ^ K ) } ) = ( log ` P ) )
38 7 32 37 3eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( Lam ` ( P ^ K ) ) = ( log ` P ) )