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