# Metamath Proof Explorer

## Theorem vmacl

Description: Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmacl
`|- ( A e. NN -> ( Lam ` A ) e. RR )`

### Proof

Step Hyp Ref Expression
1 eleq1
` |-  ( ( Lam ` A ) = 0 -> ( ( Lam ` A ) e. RR <-> 0 e. RR ) )`
2 isppw2
` |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )`
3 vmappw
` |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )`
4 prmnn
` |-  ( p e. Prime -> p e. NN )`
5 4 nnrpd
` |-  ( p e. Prime -> p e. RR+ )`
6 5 relogcld
` |-  ( p e. Prime -> ( log ` p ) e. RR )`
` |-  ( ( p e. Prime /\ k e. NN ) -> ( log ` p ) e. RR )`
8 3 7 eqeltrd
` |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) e. RR )`
9 fveq2
` |-  ( A = ( p ^ k ) -> ( Lam ` A ) = ( Lam ` ( p ^ k ) ) )`
10 9 eleq1d
` |-  ( A = ( p ^ k ) -> ( ( Lam ` A ) e. RR <-> ( Lam ` ( p ^ k ) ) e. RR ) )`
11 8 10 syl5ibrcom
` |-  ( ( p e. Prime /\ k e. NN ) -> ( A = ( p ^ k ) -> ( Lam ` A ) e. RR ) )`
12 11 rexlimivv
` |-  ( E. p e. Prime E. k e. NN A = ( p ^ k ) -> ( Lam ` A ) e. RR )`
13 2 12 syl6bi
` |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 -> ( Lam ` A ) e. RR ) )`
14 13 imp
` |-  ( ( A e. NN /\ ( Lam ` A ) =/= 0 ) -> ( Lam ` A ) e. RR )`
15 0red
` |-  ( A e. NN -> 0 e. RR )`
16 1 14 15 pm2.61ne
` |-  ( A e. NN -> ( Lam ` A ) e. RR )`