Theorem efvmacl

Description: The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	efvmacl	|- ( A e. NN -> ( exp ` ( Lam ` A ) ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( ( Lam ` A ) = 0 -> ( exp ` ( Lam ` A ) ) = ( exp ` 0 ) )
2		ef0	|- ( exp ` 0 ) = 1
3	1 2	eqtrdi	|- ( ( Lam ` A ) = 0 -> ( exp ` ( Lam ` A ) ) = 1 )
4	3	eleq1d	|- ( ( Lam ` A ) = 0 -> ( ( exp ` ( Lam ` A ) ) e. NN <-> 1 e. NN ) )
5		isppw2	|- ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )
6		vmappw	|- ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
7	6	fveq2d	|- ( ( p e. Prime /\ k e. NN ) -> ( exp ` ( Lam ` ( p ^ k ) ) ) = ( exp ` ( log ` p ) ) )
8		prmnn	|- ( p e. Prime -> p e. NN )
9	8	nnrpd	|- ( p e. Prime -> p e. RR+ )
10	9	reeflogd	|- ( p e. Prime -> ( exp ` ( log ` p ) ) = p )
11	10 8	eqeltrd	|- ( p e. Prime -> ( exp ` ( log ` p ) ) e. NN )
12	11	adantr	|- ( ( p e. Prime /\ k e. NN ) -> ( exp ` ( log ` p ) ) e. NN )
13	7 12	eqeltrd	|- ( ( p e. Prime /\ k e. NN ) -> ( exp ` ( Lam ` ( p ^ k ) ) ) e. NN )
14		fveq2	|- ( A = ( p ^ k ) -> ( Lam ` A ) = ( Lam ` ( p ^ k ) ) )
15	14	fveq2d	|- ( A = ( p ^ k ) -> ( exp ` ( Lam ` A ) ) = ( exp ` ( Lam ` ( p ^ k ) ) ) )
16	15	eleq1d	|- ( A = ( p ^ k ) -> ( ( exp ` ( Lam ` A ) ) e. NN <-> ( exp ` ( Lam ` ( p ^ k ) ) ) e. NN ) )
17	13 16	syl5ibrcom	|- ( ( p e. Prime /\ k e. NN ) -> ( A = ( p ^ k ) -> ( exp ` ( Lam ` A ) ) e. NN ) )
18	17	rexlimivv	|- ( E. p e. Prime E. k e. NN A = ( p ^ k ) -> ( exp ` ( Lam ` A ) ) e. NN )
19	5 18	biimtrdi	|- ( A e. NN -> ( ( Lam ` A ) =/= 0 -> ( exp ` ( Lam ` A ) ) e. NN ) )
20	19	imp	|- ( ( A e. NN /\ ( Lam ` A ) =/= 0 ) -> ( exp ` ( Lam ` A ) ) e. NN )
21		1nn	|- 1 e. NN
22	21	a1i	|- ( A e. NN -> 1 e. NN )
23	4 20 22	pm2.61ne	|- ( A e. NN -> ( exp ` ( Lam ` A ) ) e. NN )