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