Theorem chtlepsi

Description: The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	chtlepsi	|- ( A e. RR -> ( theta ` A ) <_ ( psi ` A ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	|- ( A e. RR -> ( 1 ... ( |_ ` A ) ) e. Fin )
2		elfznn	|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
3	2	adantl	|- ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
4		vmacl	|- ( n e. NN -> ( Lam ` n ) e. RR )
5	3 4	syl	|- ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. RR )
6		vmage0	|- ( n e. NN -> 0 <_ ( Lam ` n ) )
7	3 6	syl	|- ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ ( Lam ` n ) )
8		ppisval	|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
9		inss1	|- ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) )
10		2eluzge1	|- 2 e. ( ZZ>= ` 1 )
11		fzss1	|- ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) )
12	10 11	mp1i	|- ( A e. RR -> ( 2 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) )
13	9 12	sstrid	|- ( A e. RR -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 1 ... ( |_ ` A ) ) )
14	8 13	eqsstrd	|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) C_ ( 1 ... ( |_ ` A ) ) )
15	1 5 7 14	fsumless	|- ( A e. RR -> sum_ n e. ( ( 0 [,] A ) i^i Prime ) ( Lam ` n ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
16		chtval	|- ( A e. RR -> ( theta ` A ) = sum_ n e. ( ( 0 [,] A ) i^i Prime ) ( log ` n ) )
17		simpr	|- ( ( A e. RR /\ n e. ( ( 0 [,] A ) i^i Prime ) ) -> n e. ( ( 0 [,] A ) i^i Prime ) )
18	17	elin2d	|- ( ( A e. RR /\ n e. ( ( 0 [,] A ) i^i Prime ) ) -> n e. Prime )
19		vmaprm	|- ( n e. Prime -> ( Lam ` n ) = ( log ` n ) )
20	18 19	syl	|- ( ( A e. RR /\ n e. ( ( 0 [,] A ) i^i Prime ) ) -> ( Lam ` n ) = ( log ` n ) )
21	20	sumeq2dv	|- ( A e. RR -> sum_ n e. ( ( 0 [,] A ) i^i Prime ) ( Lam ` n ) = sum_ n e. ( ( 0 [,] A ) i^i Prime ) ( log ` n ) )
22	16 21	eqtr4d	|- ( A e. RR -> ( theta ` A ) = sum_ n e. ( ( 0 [,] A ) i^i Prime ) ( Lam ` n ) )
23		chpval	|- ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
24	15 22 23	3brtr4d	|- ( A e. RR -> ( theta ` A ) <_ ( psi ` A ) )