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