Metamath Proof Explorer

Theorem chpwordi

Description: The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion chpwordi 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( psi ` A ) <_ ( psi ` B ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( 1 ... ( |_ ` B ) ) e. Fin )
2 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` B ) ) -> n e. NN )
3 2 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ n e. ( 1 ... ( |_ ` B ) ) ) -> n e. NN )
4 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
5 3 4 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ n e. ( 1 ... ( |_ ` B ) ) ) -> ( Lam ` n ) e. RR )
6 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
7 3 6 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ n e. ( 1 ... ( |_ ` B ) ) ) -> 0 <_ ( Lam ` n ) )
8 flword2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) )
9 fzss2 
 |-  ( ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) -> ( 1 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` B ) ) )
10 8 9 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( 1 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` B ) ) )
11 1 5 7 10 fsumless 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) <_ sum_ n e. ( 1 ... ( |_ ` B ) ) ( Lam ` n ) )
12 chpval 
 |-  ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
13 12 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
14 chpval 
 |-  ( B e. RR -> ( psi ` B ) = sum_ n e. ( 1 ... ( |_ ` B ) ) ( Lam ` n ) )
15 14 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( psi ` B ) = sum_ n e. ( 1 ... ( |_ ` B ) ) ( Lam ` n ) )
16 11 13 15 3brtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( psi ` A ) <_ ( psi ` B ) )