Metamath Proof Explorer

Theorem chtwordi

Description: The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> B e. RR )
2 ppifi 
 |-  ( B e. RR -> ( ( 0 [,] B ) i^i Prime ) e. Fin )
3 1 2 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] B ) i^i Prime ) e. Fin )
4 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> p e. ( ( 0 [,] B ) i^i Prime ) )
5 4 elin2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> p e. Prime )
6 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
7 5 6 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> p e. ( ZZ>= ` 2 ) )
8 eluz2b2 
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
9 7 8 sylib 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> ( p e. NN /\ 1 < p ) )
10 9 simpld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> p e. NN )
11 10 nnred 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> p e. RR )
12 9 simprd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> 1 < p )
13 11 12 rplogcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
14 13 rpred 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> ( log ` p ) e. RR )
15 13 rpge0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( 0 [,] B ) i^i Prime ) ) -> 0 <_ ( log ` p ) )
16 0red 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> 0 e. RR )
17 0le0 
 |-  0 <_ 0
18 17 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> 0 <_ 0 )
19 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ B )
20 iccss 
 |-  ( ( ( 0 e. RR /\ B e. RR ) /\ ( 0 <_ 0 /\ A <_ B ) ) -> ( 0 [,] A ) C_ ( 0 [,] B ) )
21 16 1 18 19 20 syl22anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( 0 [,] A ) C_ ( 0 [,] B ) )
22 21 ssrind 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( 0 [,] A ) i^i Prime ) C_ ( ( 0 [,] B ) i^i Prime ) )
23 3 14 15 22 fsumless 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) <_ sum_ p e. ( ( 0 [,] B ) i^i Prime ) ( log ` p ) )
24 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
25 24 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
26 chtval 
 |-  ( B e. RR -> ( theta ` B ) = sum_ p e. ( ( 0 [,] B ) i^i Prime ) ( log ` p ) )
27 1 26 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` B ) = sum_ p e. ( ( 0 [,] B ) i^i Prime ) ( log ` p ) )
28 23 25 27 3brtr4d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` A ) <_ ( theta ` B ) )