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

Metamath Proof Explorer

Theorem vma1

Proof