Step |
Hyp |
Ref |
Expression |
1 |
|
chpdifbnd.a |
|- ( ph -> A e. RR+ ) |
2 |
|
chpdifbnd.1 |
|- ( ph -> 1 <_ A ) |
3 |
|
chpdifbnd.b |
|- ( ph -> B e. RR+ ) |
4 |
|
chpdifbnd.2 |
|- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B ) |
5 |
|
chpdifbnd.c |
|- C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) |
6 |
|
chpdifbnd.x |
|- ( ph -> X e. ( 1 (,) +oo ) ) |
7 |
|
chpdifbnd.y |
|- ( ph -> Y e. ( X [,] ( A x. X ) ) ) |
8 |
|
ioossre |
|- ( 1 (,) +oo ) C_ RR |
9 |
8 6
|
sselid |
|- ( ph -> X e. RR ) |
10 |
1
|
rpred |
|- ( ph -> A e. RR ) |
11 |
10 9
|
remulcld |
|- ( ph -> ( A x. X ) e. RR ) |
12 |
|
elicc2 |
|- ( ( X e. RR /\ ( A x. X ) e. RR ) -> ( Y e. ( X [,] ( A x. X ) ) <-> ( Y e. RR /\ X <_ Y /\ Y <_ ( A x. X ) ) ) ) |
13 |
9 11 12
|
syl2anc |
|- ( ph -> ( Y e. ( X [,] ( A x. X ) ) <-> ( Y e. RR /\ X <_ Y /\ Y <_ ( A x. X ) ) ) ) |
14 |
7 13
|
mpbid |
|- ( ph -> ( Y e. RR /\ X <_ Y /\ Y <_ ( A x. X ) ) ) |
15 |
14
|
simp1d |
|- ( ph -> Y e. RR ) |
16 |
|
chpcl |
|- ( Y e. RR -> ( psi ` Y ) e. RR ) |
17 |
15 16
|
syl |
|- ( ph -> ( psi ` Y ) e. RR ) |
18 |
|
chpcl |
|- ( X e. RR -> ( psi ` X ) e. RR ) |
19 |
9 18
|
syl |
|- ( ph -> ( psi ` X ) e. RR ) |
20 |
17 19
|
resubcld |
|- ( ph -> ( ( psi ` Y ) - ( psi ` X ) ) e. RR ) |
21 |
|
0red |
|- ( ph -> 0 e. RR ) |
22 |
|
1re |
|- 1 e. RR |
23 |
22
|
a1i |
|- ( ph -> 1 e. RR ) |
24 |
|
0lt1 |
|- 0 < 1 |
25 |
24
|
a1i |
|- ( ph -> 0 < 1 ) |
26 |
|
eliooord |
|- ( X e. ( 1 (,) +oo ) -> ( 1 < X /\ X < +oo ) ) |
27 |
6 26
|
syl |
|- ( ph -> ( 1 < X /\ X < +oo ) ) |
28 |
27
|
simpld |
|- ( ph -> 1 < X ) |
29 |
21 23 9 25 28
|
lttrd |
|- ( ph -> 0 < X ) |
30 |
9 29
|
elrpd |
|- ( ph -> X e. RR+ ) |
31 |
30
|
relogcld |
|- ( ph -> ( log ` X ) e. RR ) |
32 |
20 31
|
remulcld |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) e. RR ) |
33 |
|
2re |
|- 2 e. RR |
34 |
15 9
|
resubcld |
|- ( ph -> ( Y - X ) e. RR ) |
35 |
|
remulcl |
|- ( ( 2 e. RR /\ ( Y - X ) e. RR ) -> ( 2 x. ( Y - X ) ) e. RR ) |
36 |
33 34 35
|
sylancr |
|- ( ph -> ( 2 x. ( Y - X ) ) e. RR ) |
37 |
36 31
|
remulcld |
|- ( ph -> ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) e. RR ) |
38 |
3
|
rpred |
|- ( ph -> B e. RR ) |
39 |
15 9
|
readdcld |
|- ( ph -> ( Y + X ) e. RR ) |
40 |
38 39
|
remulcld |
|- ( ph -> ( B x. ( Y + X ) ) e. RR ) |
41 |
1
|
relogcld |
|- ( ph -> ( log ` A ) e. RR ) |
42 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` A ) e. RR ) -> ( 2 x. ( log ` A ) ) e. RR ) |
43 |
33 41 42
|
sylancr |
|- ( ph -> ( 2 x. ( log ` A ) ) e. RR ) |
44 |
43 15
|
remulcld |
|- ( ph -> ( ( 2 x. ( log ` A ) ) x. Y ) e. RR ) |
45 |
40 44
|
readdcld |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) e. RR ) |
46 |
37 45
|
readdcld |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) e. RR ) |
47 |
|
peano2re |
|- ( A e. RR -> ( A + 1 ) e. RR ) |
48 |
10 47
|
syl |
|- ( ph -> ( A + 1 ) e. RR ) |
49 |
38 48
|
remulcld |
|- ( ph -> ( B x. ( A + 1 ) ) e. RR ) |
50 |
|
remulcl |
|- ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR ) |
51 |
33 10 50
|
sylancr |
|- ( ph -> ( 2 x. A ) e. RR ) |
52 |
51 41
|
remulcld |
|- ( ph -> ( ( 2 x. A ) x. ( log ` A ) ) e. RR ) |
53 |
49 52
|
readdcld |
|- ( ph -> ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) e. RR ) |
54 |
5 53
|
eqeltrid |
|- ( ph -> C e. RR ) |
55 |
54 9
|
remulcld |
|- ( ph -> ( C x. X ) e. RR ) |
56 |
37 55
|
readdcld |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( C x. X ) ) e. RR ) |
57 |
17 31
|
remulcld |
|- ( ph -> ( ( psi ` Y ) x. ( log ` X ) ) e. RR ) |
58 |
|
fzfid |
|- ( ph -> ( 1 ... ( |_ ` X ) ) e. Fin ) |
59 |
14
|
simp2d |
|- ( ph -> X <_ Y ) |
60 |
|
flword2 |
|- ( ( X e. RR /\ Y e. RR /\ X <_ Y ) -> ( |_ ` Y ) e. ( ZZ>= ` ( |_ ` X ) ) ) |
61 |
9 15 59 60
|
syl3anc |
|- ( ph -> ( |_ ` Y ) e. ( ZZ>= ` ( |_ ` X ) ) ) |
62 |
|
fzss2 |
|- ( ( |_ ` Y ) e. ( ZZ>= ` ( |_ ` X ) ) -> ( 1 ... ( |_ ` X ) ) C_ ( 1 ... ( |_ ` Y ) ) ) |
63 |
61 62
|
syl |
|- ( ph -> ( 1 ... ( |_ ` X ) ) C_ ( 1 ... ( |_ ` Y ) ) ) |
64 |
63
|
sselda |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` X ) ) ) -> n e. ( 1 ... ( |_ ` Y ) ) ) |
65 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` Y ) ) -> n e. NN ) |
66 |
65
|
adantl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> n e. NN ) |
67 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
68 |
66 67
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( Lam ` n ) e. RR ) |
69 |
|
nndivre |
|- ( ( X e. RR /\ n e. NN ) -> ( X / n ) e. RR ) |
70 |
9 65 69
|
syl2an |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( X / n ) e. RR ) |
71 |
|
chpcl |
|- ( ( X / n ) e. RR -> ( psi ` ( X / n ) ) e. RR ) |
72 |
70 71
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( psi ` ( X / n ) ) e. RR ) |
73 |
68 72
|
remulcld |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) e. RR ) |
74 |
64 73
|
syldan |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` X ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) e. RR ) |
75 |
58 74
|
fsumrecl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) e. RR ) |
76 |
57 75
|
readdcld |
|- ( ph -> ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) e. RR ) |
77 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` X ) e. RR ) -> ( 2 x. ( log ` X ) ) e. RR ) |
78 |
33 31 77
|
sylancr |
|- ( ph -> ( 2 x. ( log ` X ) ) e. RR ) |
79 |
78 38
|
resubcld |
|- ( ph -> ( ( 2 x. ( log ` X ) ) - B ) e. RR ) |
80 |
79 9
|
remulcld |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) e. RR ) |
81 |
1 30
|
rpmulcld |
|- ( ph -> ( A x. X ) e. RR+ ) |
82 |
81
|
relogcld |
|- ( ph -> ( log ` ( A x. X ) ) e. RR ) |
83 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` ( A x. X ) ) e. RR ) -> ( 2 x. ( log ` ( A x. X ) ) ) e. RR ) |
84 |
33 82 83
|
sylancr |
|- ( ph -> ( 2 x. ( log ` ( A x. X ) ) ) e. RR ) |
85 |
38 84
|
readdcld |
|- ( ph -> ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) e. RR ) |
86 |
85 15
|
remulcld |
|- ( ph -> ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) e. RR ) |
87 |
19 31
|
remulcld |
|- ( ph -> ( ( psi ` X ) x. ( log ` X ) ) e. RR ) |
88 |
87 75
|
readdcld |
|- ( ph -> ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) e. RR ) |
89 |
21 9 15 29 59
|
ltletrd |
|- ( ph -> 0 < Y ) |
90 |
15 89
|
elrpd |
|- ( ph -> Y e. RR+ ) |
91 |
90
|
relogcld |
|- ( ph -> ( log ` Y ) e. RR ) |
92 |
17 91
|
remulcld |
|- ( ph -> ( ( psi ` Y ) x. ( log ` Y ) ) e. RR ) |
93 |
|
fzfid |
|- ( ph -> ( 1 ... ( |_ ` Y ) ) e. Fin ) |
94 |
|
nndivre |
|- ( ( Y e. RR /\ n e. NN ) -> ( Y / n ) e. RR ) |
95 |
15 65 94
|
syl2an |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( Y / n ) e. RR ) |
96 |
|
chpcl |
|- ( ( Y / n ) e. RR -> ( psi ` ( Y / n ) ) e. RR ) |
97 |
95 96
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( psi ` ( Y / n ) ) e. RR ) |
98 |
68 97
|
remulcld |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) e. RR ) |
99 |
93 98
|
fsumrecl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) e. RR ) |
100 |
92 99
|
readdcld |
|- ( ph -> ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) e. RR ) |
101 |
|
chpge0 |
|- ( Y e. RR -> 0 <_ ( psi ` Y ) ) |
102 |
15 101
|
syl |
|- ( ph -> 0 <_ ( psi ` Y ) ) |
103 |
30 90
|
logled |
|- ( ph -> ( X <_ Y <-> ( log ` X ) <_ ( log ` Y ) ) ) |
104 |
59 103
|
mpbid |
|- ( ph -> ( log ` X ) <_ ( log ` Y ) ) |
105 |
31 91 17 102 104
|
lemul2ad |
|- ( ph -> ( ( psi ` Y ) x. ( log ` X ) ) <_ ( ( psi ` Y ) x. ( log ` Y ) ) ) |
106 |
93 73
|
fsumrecl |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) e. RR ) |
107 |
|
vmage0 |
|- ( n e. NN -> 0 <_ ( Lam ` n ) ) |
108 |
66 107
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> 0 <_ ( Lam ` n ) ) |
109 |
|
chpge0 |
|- ( ( X / n ) e. RR -> 0 <_ ( psi ` ( X / n ) ) ) |
110 |
70 109
|
syl |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> 0 <_ ( psi ` ( X / n ) ) ) |
111 |
68 72 108 110
|
mulge0d |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) |
112 |
93 73 111 63
|
fsumless |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) |
113 |
9
|
adantr |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> X e. RR ) |
114 |
15
|
adantr |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> Y e. RR ) |
115 |
66
|
nnrpd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> n e. RR+ ) |
116 |
59
|
adantr |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> X <_ Y ) |
117 |
113 114 115 116
|
lediv1dd |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( X / n ) <_ ( Y / n ) ) |
118 |
|
chpwordi |
|- ( ( ( X / n ) e. RR /\ ( Y / n ) e. RR /\ ( X / n ) <_ ( Y / n ) ) -> ( psi ` ( X / n ) ) <_ ( psi ` ( Y / n ) ) ) |
119 |
70 95 117 118
|
syl3anc |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( psi ` ( X / n ) ) <_ ( psi ` ( Y / n ) ) ) |
120 |
72 97 68 108 119
|
lemul2ad |
|- ( ( ph /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) <_ ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
121 |
93 73 98 120
|
fsumle |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
122 |
75 106 99 112 121
|
letrd |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
123 |
57 75 92 99 105 122
|
le2addd |
|- ( ph -> ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) <_ ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) ) |
124 |
100 90
|
rerpdivcld |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) e. RR ) |
125 |
|
remulcl |
|- ( ( 2 e. RR /\ ( log ` Y ) e. RR ) -> ( 2 x. ( log ` Y ) ) e. RR ) |
126 |
33 91 125
|
sylancr |
|- ( ph -> ( 2 x. ( log ` Y ) ) e. RR ) |
127 |
38 126
|
readdcld |
|- ( ph -> ( B + ( 2 x. ( log ` Y ) ) ) e. RR ) |
128 |
124 126
|
resubcld |
|- ( ph -> ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) e. RR ) |
129 |
128
|
recnd |
|- ( ph -> ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) e. CC ) |
130 |
129
|
abscld |
|- ( ph -> ( abs ` ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) e. RR ) |
131 |
128
|
leabsd |
|- ( ph -> ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) <_ ( abs ` ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) ) |
132 |
|
fveq2 |
|- ( z = Y -> ( psi ` z ) = ( psi ` Y ) ) |
133 |
|
fveq2 |
|- ( z = Y -> ( log ` z ) = ( log ` Y ) ) |
134 |
132 133
|
oveq12d |
|- ( z = Y -> ( ( psi ` z ) x. ( log ` z ) ) = ( ( psi ` Y ) x. ( log ` Y ) ) ) |
135 |
|
fveq2 |
|- ( m = n -> ( Lam ` m ) = ( Lam ` n ) ) |
136 |
|
oveq2 |
|- ( m = n -> ( z / m ) = ( z / n ) ) |
137 |
136
|
fveq2d |
|- ( m = n -> ( psi ` ( z / m ) ) = ( psi ` ( z / n ) ) ) |
138 |
135 137
|
oveq12d |
|- ( m = n -> ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) = ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) |
139 |
138
|
cbvsumv |
|- sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) |
140 |
|
fveq2 |
|- ( z = Y -> ( |_ ` z ) = ( |_ ` Y ) ) |
141 |
140
|
oveq2d |
|- ( z = Y -> ( 1 ... ( |_ ` z ) ) = ( 1 ... ( |_ ` Y ) ) ) |
142 |
|
simpl |
|- ( ( z = Y /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> z = Y ) |
143 |
142
|
fvoveq1d |
|- ( ( z = Y /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( psi ` ( z / n ) ) = ( psi ` ( Y / n ) ) ) |
144 |
143
|
oveq2d |
|- ( ( z = Y /\ n e. ( 1 ... ( |_ ` Y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) = ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
145 |
141 144
|
sumeq12rdv |
|- ( z = Y -> sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
146 |
139 145
|
syl5eq |
|- ( z = Y -> sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) |
147 |
134 146
|
oveq12d |
|- ( z = Y -> ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) = ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) ) |
148 |
|
id |
|- ( z = Y -> z = Y ) |
149 |
147 148
|
oveq12d |
|- ( z = Y -> ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) = ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) ) |
150 |
133
|
oveq2d |
|- ( z = Y -> ( 2 x. ( log ` z ) ) = ( 2 x. ( log ` Y ) ) ) |
151 |
149 150
|
oveq12d |
|- ( z = Y -> ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) = ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) |
152 |
151
|
fveq2d |
|- ( z = Y -> ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) = ( abs ` ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) ) |
153 |
152
|
breq1d |
|- ( z = Y -> ( ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B <-> ( abs ` ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) <_ B ) ) |
154 |
23 9 28
|
ltled |
|- ( ph -> 1 <_ X ) |
155 |
23 9 15 154 59
|
letrd |
|- ( ph -> 1 <_ Y ) |
156 |
|
elicopnf |
|- ( 1 e. RR -> ( Y e. ( 1 [,) +oo ) <-> ( Y e. RR /\ 1 <_ Y ) ) ) |
157 |
22 156
|
ax-mp |
|- ( Y e. ( 1 [,) +oo ) <-> ( Y e. RR /\ 1 <_ Y ) ) |
158 |
15 155 157
|
sylanbrc |
|- ( ph -> Y e. ( 1 [,) +oo ) ) |
159 |
153 4 158
|
rspcdva |
|- ( ph -> ( abs ` ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) ) <_ B ) |
160 |
128 130 38 131 159
|
letrd |
|- ( ph -> ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) <_ B ) |
161 |
124 126 38
|
lesubaddd |
|- ( ph -> ( ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) - ( 2 x. ( log ` Y ) ) ) <_ B <-> ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) <_ ( B + ( 2 x. ( log ` Y ) ) ) ) ) |
162 |
160 161
|
mpbid |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) <_ ( B + ( 2 x. ( log ` Y ) ) ) ) |
163 |
14
|
simp3d |
|- ( ph -> Y <_ ( A x. X ) ) |
164 |
90 81
|
logled |
|- ( ph -> ( Y <_ ( A x. X ) <-> ( log ` Y ) <_ ( log ` ( A x. X ) ) ) ) |
165 |
163 164
|
mpbid |
|- ( ph -> ( log ` Y ) <_ ( log ` ( A x. X ) ) ) |
166 |
|
2pos |
|- 0 < 2 |
167 |
33 166
|
pm3.2i |
|- ( 2 e. RR /\ 0 < 2 ) |
168 |
167
|
a1i |
|- ( ph -> ( 2 e. RR /\ 0 < 2 ) ) |
169 |
|
lemul2 |
|- ( ( ( log ` Y ) e. RR /\ ( log ` ( A x. X ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( log ` Y ) <_ ( log ` ( A x. X ) ) <-> ( 2 x. ( log ` Y ) ) <_ ( 2 x. ( log ` ( A x. X ) ) ) ) ) |
170 |
91 82 168 169
|
syl3anc |
|- ( ph -> ( ( log ` Y ) <_ ( log ` ( A x. X ) ) <-> ( 2 x. ( log ` Y ) ) <_ ( 2 x. ( log ` ( A x. X ) ) ) ) ) |
171 |
165 170
|
mpbid |
|- ( ph -> ( 2 x. ( log ` Y ) ) <_ ( 2 x. ( log ` ( A x. X ) ) ) ) |
172 |
126 84 38 171
|
leadd2dd |
|- ( ph -> ( B + ( 2 x. ( log ` Y ) ) ) <_ ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) ) |
173 |
124 127 85 162 172
|
letrd |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) <_ ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) ) |
174 |
100 85 90
|
ledivmul2d |
|- ( ph -> ( ( ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) / Y ) <_ ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) <-> ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) <_ ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) ) ) |
175 |
173 174
|
mpbid |
|- ( ph -> ( ( ( psi ` Y ) x. ( log ` Y ) ) + sum_ n e. ( 1 ... ( |_ ` Y ) ) ( ( Lam ` n ) x. ( psi ` ( Y / n ) ) ) ) <_ ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) ) |
176 |
76 100 86 123 175
|
letrd |
|- ( ph -> ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) <_ ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) ) |
177 |
|
fveq2 |
|- ( z = X -> ( psi ` z ) = ( psi ` X ) ) |
178 |
|
fveq2 |
|- ( z = X -> ( log ` z ) = ( log ` X ) ) |
179 |
177 178
|
oveq12d |
|- ( z = X -> ( ( psi ` z ) x. ( log ` z ) ) = ( ( psi ` X ) x. ( log ` X ) ) ) |
180 |
|
fveq2 |
|- ( z = X -> ( |_ ` z ) = ( |_ ` X ) ) |
181 |
180
|
oveq2d |
|- ( z = X -> ( 1 ... ( |_ ` z ) ) = ( 1 ... ( |_ ` X ) ) ) |
182 |
|
simpl |
|- ( ( z = X /\ n e. ( 1 ... ( |_ ` X ) ) ) -> z = X ) |
183 |
182
|
fvoveq1d |
|- ( ( z = X /\ n e. ( 1 ... ( |_ ` X ) ) ) -> ( psi ` ( z / n ) ) = ( psi ` ( X / n ) ) ) |
184 |
183
|
oveq2d |
|- ( ( z = X /\ n e. ( 1 ... ( |_ ` X ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) = ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) |
185 |
181 184
|
sumeq12rdv |
|- ( z = X -> sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) |
186 |
139 185
|
syl5eq |
|- ( z = X -> sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) |
187 |
179 186
|
oveq12d |
|- ( z = X -> ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) = ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) ) |
188 |
|
id |
|- ( z = X -> z = X ) |
189 |
187 188
|
oveq12d |
|- ( z = X -> ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) = ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) ) |
190 |
178
|
oveq2d |
|- ( z = X -> ( 2 x. ( log ` z ) ) = ( 2 x. ( log ` X ) ) ) |
191 |
189 190
|
oveq12d |
|- ( z = X -> ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) = ( ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) - ( 2 x. ( log ` X ) ) ) ) |
192 |
191
|
fveq2d |
|- ( z = X -> ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) = ( abs ` ( ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) - ( 2 x. ( log ` X ) ) ) ) ) |
193 |
192
|
breq1d |
|- ( z = X -> ( ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B <-> ( abs ` ( ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) - ( 2 x. ( log ` X ) ) ) ) <_ B ) ) |
194 |
|
elicopnf |
|- ( 1 e. RR -> ( X e. ( 1 [,) +oo ) <-> ( X e. RR /\ 1 <_ X ) ) ) |
195 |
22 194
|
ax-mp |
|- ( X e. ( 1 [,) +oo ) <-> ( X e. RR /\ 1 <_ X ) ) |
196 |
9 154 195
|
sylanbrc |
|- ( ph -> X e. ( 1 [,) +oo ) ) |
197 |
193 4 196
|
rspcdva |
|- ( ph -> ( abs ` ( ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) - ( 2 x. ( log ` X ) ) ) ) <_ B ) |
198 |
88 30
|
rerpdivcld |
|- ( ph -> ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) e. RR ) |
199 |
198 78 38
|
absdifled |
|- ( ph -> ( ( abs ` ( ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) - ( 2 x. ( log ` X ) ) ) ) <_ B <-> ( ( ( 2 x. ( log ` X ) ) - B ) <_ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) /\ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) <_ ( ( 2 x. ( log ` X ) ) + B ) ) ) ) |
200 |
197 199
|
mpbid |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) - B ) <_ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) /\ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) <_ ( ( 2 x. ( log ` X ) ) + B ) ) ) |
201 |
200
|
simpld |
|- ( ph -> ( ( 2 x. ( log ` X ) ) - B ) <_ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) ) |
202 |
79 88 30
|
lemuldivd |
|- ( ph -> ( ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) <_ ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) <-> ( ( 2 x. ( log ` X ) ) - B ) <_ ( ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) / X ) ) ) |
203 |
201 202
|
mpbird |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) <_ ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) ) |
204 |
76 80 86 88 176 203
|
le2subd |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) - ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) ) <_ ( ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) - ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) ) ) |
205 |
57
|
recnd |
|- ( ph -> ( ( psi ` Y ) x. ( log ` X ) ) e. CC ) |
206 |
87
|
recnd |
|- ( ph -> ( ( psi ` X ) x. ( log ` X ) ) e. CC ) |
207 |
75
|
recnd |
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) e. CC ) |
208 |
205 206 207
|
pnpcan2d |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) - ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) ) = ( ( ( psi ` Y ) x. ( log ` X ) ) - ( ( psi ` X ) x. ( log ` X ) ) ) ) |
209 |
17
|
recnd |
|- ( ph -> ( psi ` Y ) e. CC ) |
210 |
19
|
recnd |
|- ( ph -> ( psi ` X ) e. CC ) |
211 |
31
|
recnd |
|- ( ph -> ( log ` X ) e. CC ) |
212 |
209 210 211
|
subdird |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) = ( ( ( psi ` Y ) x. ( log ` X ) ) - ( ( psi ` X ) x. ( log ` X ) ) ) ) |
213 |
208 212
|
eqtr4d |
|- ( ph -> ( ( ( ( psi ` Y ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) - ( ( ( psi ` X ) x. ( log ` X ) ) + sum_ n e. ( 1 ... ( |_ ` X ) ) ( ( Lam ` n ) x. ( psi ` ( X / n ) ) ) ) ) = ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) ) |
214 |
78 15
|
remulcld |
|- ( ph -> ( ( 2 x. ( log ` X ) ) x. Y ) e. RR ) |
215 |
214
|
recnd |
|- ( ph -> ( ( 2 x. ( log ` X ) ) x. Y ) e. CC ) |
216 |
38 43
|
readdcld |
|- ( ph -> ( B + ( 2 x. ( log ` A ) ) ) e. RR ) |
217 |
216 15
|
remulcld |
|- ( ph -> ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) e. RR ) |
218 |
217
|
recnd |
|- ( ph -> ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) e. CC ) |
219 |
78 9
|
remulcld |
|- ( ph -> ( ( 2 x. ( log ` X ) ) x. X ) e. RR ) |
220 |
219
|
recnd |
|- ( ph -> ( ( 2 x. ( log ` X ) ) x. X ) e. CC ) |
221 |
38 9
|
remulcld |
|- ( ph -> ( B x. X ) e. RR ) |
222 |
221
|
recnd |
|- ( ph -> ( B x. X ) e. CC ) |
223 |
222
|
negcld |
|- ( ph -> -u ( B x. X ) e. CC ) |
224 |
215 218 220 223
|
addsub4d |
|- ( ph -> ( ( ( ( 2 x. ( log ` X ) ) x. Y ) + ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) ) - ( ( ( 2 x. ( log ` X ) ) x. X ) + -u ( B x. X ) ) ) = ( ( ( ( 2 x. ( log ` X ) ) x. Y ) - ( ( 2 x. ( log ` X ) ) x. X ) ) + ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) - -u ( B x. X ) ) ) ) |
225 |
41
|
recnd |
|- ( ph -> ( log ` A ) e. CC ) |
226 |
1 30
|
relogmuld |
|- ( ph -> ( log ` ( A x. X ) ) = ( ( log ` A ) + ( log ` X ) ) ) |
227 |
225 211 226
|
comraddd |
|- ( ph -> ( log ` ( A x. X ) ) = ( ( log ` X ) + ( log ` A ) ) ) |
228 |
227
|
oveq2d |
|- ( ph -> ( 2 x. ( log ` ( A x. X ) ) ) = ( 2 x. ( ( log ` X ) + ( log ` A ) ) ) ) |
229 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
230 |
229 211 225
|
adddid |
|- ( ph -> ( 2 x. ( ( log ` X ) + ( log ` A ) ) ) = ( ( 2 x. ( log ` X ) ) + ( 2 x. ( log ` A ) ) ) ) |
231 |
228 230
|
eqtrd |
|- ( ph -> ( 2 x. ( log ` ( A x. X ) ) ) = ( ( 2 x. ( log ` X ) ) + ( 2 x. ( log ` A ) ) ) ) |
232 |
231
|
oveq2d |
|- ( ph -> ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) = ( B + ( ( 2 x. ( log ` X ) ) + ( 2 x. ( log ` A ) ) ) ) ) |
233 |
38
|
recnd |
|- ( ph -> B e. CC ) |
234 |
78
|
recnd |
|- ( ph -> ( 2 x. ( log ` X ) ) e. CC ) |
235 |
43
|
recnd |
|- ( ph -> ( 2 x. ( log ` A ) ) e. CC ) |
236 |
233 234 235
|
add12d |
|- ( ph -> ( B + ( ( 2 x. ( log ` X ) ) + ( 2 x. ( log ` A ) ) ) ) = ( ( 2 x. ( log ` X ) ) + ( B + ( 2 x. ( log ` A ) ) ) ) ) |
237 |
232 236
|
eqtrd |
|- ( ph -> ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) = ( ( 2 x. ( log ` X ) ) + ( B + ( 2 x. ( log ` A ) ) ) ) ) |
238 |
237
|
oveq1d |
|- ( ph -> ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) = ( ( ( 2 x. ( log ` X ) ) + ( B + ( 2 x. ( log ` A ) ) ) ) x. Y ) ) |
239 |
216
|
recnd |
|- ( ph -> ( B + ( 2 x. ( log ` A ) ) ) e. CC ) |
240 |
15
|
recnd |
|- ( ph -> Y e. CC ) |
241 |
234 239 240
|
adddird |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) + ( B + ( 2 x. ( log ` A ) ) ) ) x. Y ) = ( ( ( 2 x. ( log ` X ) ) x. Y ) + ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) ) ) |
242 |
238 241
|
eqtrd |
|- ( ph -> ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) = ( ( ( 2 x. ( log ` X ) ) x. Y ) + ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) ) ) |
243 |
9
|
recnd |
|- ( ph -> X e. CC ) |
244 |
234 233 243
|
subdird |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) = ( ( ( 2 x. ( log ` X ) ) x. X ) - ( B x. X ) ) ) |
245 |
220 222
|
negsubd |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) x. X ) + -u ( B x. X ) ) = ( ( ( 2 x. ( log ` X ) ) x. X ) - ( B x. X ) ) ) |
246 |
244 245
|
eqtr4d |
|- ( ph -> ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) = ( ( ( 2 x. ( log ` X ) ) x. X ) + -u ( B x. X ) ) ) |
247 |
242 246
|
oveq12d |
|- ( ph -> ( ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) - ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) ) = ( ( ( ( 2 x. ( log ` X ) ) x. Y ) + ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) ) - ( ( ( 2 x. ( log ` X ) ) x. X ) + -u ( B x. X ) ) ) ) |
248 |
34
|
recnd |
|- ( ph -> ( Y - X ) e. CC ) |
249 |
229 248 211
|
mul32d |
|- ( ph -> ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) = ( ( 2 x. ( log ` X ) ) x. ( Y - X ) ) ) |
250 |
234 240 243
|
subdid |
|- ( ph -> ( ( 2 x. ( log ` X ) ) x. ( Y - X ) ) = ( ( ( 2 x. ( log ` X ) ) x. Y ) - ( ( 2 x. ( log ` X ) ) x. X ) ) ) |
251 |
249 250
|
eqtrd |
|- ( ph -> ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) = ( ( ( 2 x. ( log ` X ) ) x. Y ) - ( ( 2 x. ( log ` X ) ) x. X ) ) ) |
252 |
38 15
|
remulcld |
|- ( ph -> ( B x. Y ) e. RR ) |
253 |
252
|
recnd |
|- ( ph -> ( B x. Y ) e. CC ) |
254 |
44
|
recnd |
|- ( ph -> ( ( 2 x. ( log ` A ) ) x. Y ) e. CC ) |
255 |
253 222 254
|
add32d |
|- ( ph -> ( ( ( B x. Y ) + ( B x. X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) = ( ( ( B x. Y ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) + ( B x. X ) ) ) |
256 |
233 240 243
|
adddid |
|- ( ph -> ( B x. ( Y + X ) ) = ( ( B x. Y ) + ( B x. X ) ) ) |
257 |
256
|
oveq1d |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) = ( ( ( B x. Y ) + ( B x. X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) |
258 |
233 235 240
|
adddird |
|- ( ph -> ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) = ( ( B x. Y ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) |
259 |
258
|
oveq1d |
|- ( ph -> ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) + ( B x. X ) ) = ( ( ( B x. Y ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) + ( B x. X ) ) ) |
260 |
255 257 259
|
3eqtr4d |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) = ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) + ( B x. X ) ) ) |
261 |
218 222
|
subnegd |
|- ( ph -> ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) - -u ( B x. X ) ) = ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) + ( B x. X ) ) ) |
262 |
260 261
|
eqtr4d |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) = ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) - -u ( B x. X ) ) ) |
263 |
251 262
|
oveq12d |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) = ( ( ( ( 2 x. ( log ` X ) ) x. Y ) - ( ( 2 x. ( log ` X ) ) x. X ) ) + ( ( ( B + ( 2 x. ( log ` A ) ) ) x. Y ) - -u ( B x. X ) ) ) ) |
264 |
224 247 263
|
3eqtr4d |
|- ( ph -> ( ( ( B + ( 2 x. ( log ` ( A x. X ) ) ) ) x. Y ) - ( ( ( 2 x. ( log ` X ) ) - B ) x. X ) ) = ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) ) |
265 |
204 213 264
|
3brtr3d |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) <_ ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) ) |
266 |
49 9
|
remulcld |
|- ( ph -> ( ( B x. ( A + 1 ) ) x. X ) e. RR ) |
267 |
52 9
|
remulcld |
|- ( ph -> ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) e. RR ) |
268 |
15 11 9 163
|
leadd1dd |
|- ( ph -> ( Y + X ) <_ ( ( A x. X ) + X ) ) |
269 |
10
|
recnd |
|- ( ph -> A e. CC ) |
270 |
269 243
|
adddirp1d |
|- ( ph -> ( ( A + 1 ) x. X ) = ( ( A x. X ) + X ) ) |
271 |
268 270
|
breqtrrd |
|- ( ph -> ( Y + X ) <_ ( ( A + 1 ) x. X ) ) |
272 |
48 9
|
remulcld |
|- ( ph -> ( ( A + 1 ) x. X ) e. RR ) |
273 |
39 272 3
|
lemul2d |
|- ( ph -> ( ( Y + X ) <_ ( ( A + 1 ) x. X ) <-> ( B x. ( Y + X ) ) <_ ( B x. ( ( A + 1 ) x. X ) ) ) ) |
274 |
271 273
|
mpbid |
|- ( ph -> ( B x. ( Y + X ) ) <_ ( B x. ( ( A + 1 ) x. X ) ) ) |
275 |
48
|
recnd |
|- ( ph -> ( A + 1 ) e. CC ) |
276 |
233 275 243
|
mulassd |
|- ( ph -> ( ( B x. ( A + 1 ) ) x. X ) = ( B x. ( ( A + 1 ) x. X ) ) ) |
277 |
274 276
|
breqtrrd |
|- ( ph -> ( B x. ( Y + X ) ) <_ ( ( B x. ( A + 1 ) ) x. X ) ) |
278 |
33
|
a1i |
|- ( ph -> 2 e. RR ) |
279 |
|
0le2 |
|- 0 <_ 2 |
280 |
279
|
a1i |
|- ( ph -> 0 <_ 2 ) |
281 |
|
log1 |
|- ( log ` 1 ) = 0 |
282 |
|
1rp |
|- 1 e. RR+ |
283 |
|
logleb |
|- ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) ) |
284 |
282 1 283
|
sylancr |
|- ( ph -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) ) |
285 |
2 284
|
mpbid |
|- ( ph -> ( log ` 1 ) <_ ( log ` A ) ) |
286 |
281 285
|
eqbrtrrid |
|- ( ph -> 0 <_ ( log ` A ) ) |
287 |
278 41 280 286
|
mulge0d |
|- ( ph -> 0 <_ ( 2 x. ( log ` A ) ) ) |
288 |
15 11 43 287 163
|
lemul2ad |
|- ( ph -> ( ( 2 x. ( log ` A ) ) x. Y ) <_ ( ( 2 x. ( log ` A ) ) x. ( A x. X ) ) ) |
289 |
51
|
recnd |
|- ( ph -> ( 2 x. A ) e. CC ) |
290 |
289 225 243
|
mulassd |
|- ( ph -> ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) = ( ( 2 x. A ) x. ( ( log ` A ) x. X ) ) ) |
291 |
229 269 225 243
|
mul4d |
|- ( ph -> ( ( 2 x. A ) x. ( ( log ` A ) x. X ) ) = ( ( 2 x. ( log ` A ) ) x. ( A x. X ) ) ) |
292 |
290 291
|
eqtrd |
|- ( ph -> ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) = ( ( 2 x. ( log ` A ) ) x. ( A x. X ) ) ) |
293 |
288 292
|
breqtrrd |
|- ( ph -> ( ( 2 x. ( log ` A ) ) x. Y ) <_ ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) ) |
294 |
40 44 266 267 277 293
|
le2addd |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) <_ ( ( ( B x. ( A + 1 ) ) x. X ) + ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) ) ) |
295 |
5
|
oveq1i |
|- ( C x. X ) = ( ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) x. X ) |
296 |
49
|
recnd |
|- ( ph -> ( B x. ( A + 1 ) ) e. CC ) |
297 |
52
|
recnd |
|- ( ph -> ( ( 2 x. A ) x. ( log ` A ) ) e. CC ) |
298 |
296 297 243
|
adddird |
|- ( ph -> ( ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) x. X ) = ( ( ( B x. ( A + 1 ) ) x. X ) + ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) ) ) |
299 |
295 298
|
syl5eq |
|- ( ph -> ( C x. X ) = ( ( ( B x. ( A + 1 ) ) x. X ) + ( ( ( 2 x. A ) x. ( log ` A ) ) x. X ) ) ) |
300 |
294 299
|
breqtrrd |
|- ( ph -> ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) <_ ( C x. X ) ) |
301 |
45 55 37 300
|
leadd2dd |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( B x. ( Y + X ) ) + ( ( 2 x. ( log ` A ) ) x. Y ) ) ) <_ ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( C x. X ) ) ) |
302 |
32 46 56 265 301
|
letrd |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) <_ ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( C x. X ) ) ) |
303 |
36
|
recnd |
|- ( ph -> ( 2 x. ( Y - X ) ) e. CC ) |
304 |
9 28
|
rplogcld |
|- ( ph -> ( log ` X ) e. RR+ ) |
305 |
9 304
|
rerpdivcld |
|- ( ph -> ( X / ( log ` X ) ) e. RR ) |
306 |
54 305
|
remulcld |
|- ( ph -> ( C x. ( X / ( log ` X ) ) ) e. RR ) |
307 |
306
|
recnd |
|- ( ph -> ( C x. ( X / ( log ` X ) ) ) e. CC ) |
308 |
303 307 211
|
adddird |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) x. ( log ` X ) ) = ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( C x. ( X / ( log ` X ) ) ) x. ( log ` X ) ) ) ) |
309 |
54
|
recnd |
|- ( ph -> C e. CC ) |
310 |
305
|
recnd |
|- ( ph -> ( X / ( log ` X ) ) e. CC ) |
311 |
309 310 211
|
mulassd |
|- ( ph -> ( ( C x. ( X / ( log ` X ) ) ) x. ( log ` X ) ) = ( C x. ( ( X / ( log ` X ) ) x. ( log ` X ) ) ) ) |
312 |
304
|
rpne0d |
|- ( ph -> ( log ` X ) =/= 0 ) |
313 |
243 211 312
|
divcan1d |
|- ( ph -> ( ( X / ( log ` X ) ) x. ( log ` X ) ) = X ) |
314 |
313
|
oveq2d |
|- ( ph -> ( C x. ( ( X / ( log ` X ) ) x. ( log ` X ) ) ) = ( C x. X ) ) |
315 |
311 314
|
eqtrd |
|- ( ph -> ( ( C x. ( X / ( log ` X ) ) ) x. ( log ` X ) ) = ( C x. X ) ) |
316 |
315
|
oveq2d |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( ( C x. ( X / ( log ` X ) ) ) x. ( log ` X ) ) ) = ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( C x. X ) ) ) |
317 |
308 316
|
eqtrd |
|- ( ph -> ( ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) x. ( log ` X ) ) = ( ( ( 2 x. ( Y - X ) ) x. ( log ` X ) ) + ( C x. X ) ) ) |
318 |
302 317
|
breqtrrd |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) <_ ( ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) x. ( log ` X ) ) ) |
319 |
36 306
|
readdcld |
|- ( ph -> ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) e. RR ) |
320 |
20 319 304
|
lemul1d |
|- ( ph -> ( ( ( psi ` Y ) - ( psi ` X ) ) <_ ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) <-> ( ( ( psi ` Y ) - ( psi ` X ) ) x. ( log ` X ) ) <_ ( ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) x. ( log ` X ) ) ) ) |
321 |
318 320
|
mpbird |
|- ( ph -> ( ( psi ` Y ) - ( psi ` X ) ) <_ ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) ) |