This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )