Theorem vma1

Description: The von Mangoldt function at 1 . (Contributed by Mario Carneiro, 9-Apr-2016)

	Ref	Expression
Assertion	vma1	|- ( Lam ` 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		1red	|- ( ( p e. Prime /\ k e. NN ) -> 1 e. RR )
2		prmuz2	|- ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
3	2	adantr	|- ( ( p e. Prime /\ k e. NN ) -> p e. ( ZZ>= ` 2 ) )
4		eluz2b2	|- ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
5	3 4	sylib	|- ( ( p e. Prime /\ k e. NN ) -> ( p e. NN /\ 1 < p ) )
6	5	simpld	|- ( ( p e. Prime /\ k e. NN ) -> p e. NN )
7	6	nnred	|- ( ( p e. Prime /\ k e. NN ) -> p e. RR )
8		nnnn0	|- ( k e. NN -> k e. NN0 )
9	8	adantl	|- ( ( p e. Prime /\ k e. NN ) -> k e. NN0 )
10	7 9	reexpcld	|- ( ( p e. Prime /\ k e. NN ) -> ( p ^ k ) e. RR )
11	5	simprd	|- ( ( p e. Prime /\ k e. NN ) -> 1 < p )
12	6	nncnd	|- ( ( p e. Prime /\ k e. NN ) -> p e. CC )
13	12	exp1d	|- ( ( p e. Prime /\ k e. NN ) -> ( p ^ 1 ) = p )
14	6	nnge1d	|- ( ( p e. Prime /\ k e. NN ) -> 1 <_ p )
15		simpr	|- ( ( p e. Prime /\ k e. NN ) -> k e. NN )
16		nnuz	|- NN = ( ZZ>= ` 1 )
17	15 16	eleqtrdi	|- ( ( p e. Prime /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
18	7 14 17	leexp2ad	|- ( ( p e. Prime /\ k e. NN ) -> ( p ^ 1 ) <_ ( p ^ k ) )
19	13 18	eqbrtrrd	|- ( ( p e. Prime /\ k e. NN ) -> p <_ ( p ^ k ) )
20	1 7 10 11 19	ltletrd	|- ( ( p e. Prime /\ k e. NN ) -> 1 < ( p ^ k ) )
21	1 20	ltned	|- ( ( p e. Prime /\ k e. NN ) -> 1 =/= ( p ^ k ) )
22	21	neneqd	|- ( ( p e. Prime /\ k e. NN ) -> -. 1 = ( p ^ k ) )
23	22	nrexdv	|- ( p e. Prime -> -. E. k e. NN 1 = ( p ^ k ) )
24	23	nrex	|- -. E. p e. Prime E. k e. NN 1 = ( p ^ k )
25		1nn	|- 1 e. NN
26		isppw2	|- ( 1 e. NN -> ( ( Lam ` 1 ) =/= 0 <-> E. p e. Prime E. k e. NN 1 = ( p ^ k ) ) )
27	25 26	ax-mp	|- ( ( Lam ` 1 ) =/= 0 <-> E. p e. Prime E. k e. NN 1 = ( p ^ k ) )
28	27	necon1bbii	|- ( -. E. p e. Prime E. k e. NN 1 = ( p ^ k ) <-> ( Lam ` 1 ) = 0 )
29	24 28	mpbi	|- ( Lam ` 1 ) = 0