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 )