This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
7 6 adantr 
 |-  ( ( 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 biimtrdi 
 |-  ( 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 )