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 syl6bbr
 |-  ( ( 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 ) )