Metamath Proof Explorer

Theorem chpdifbndlem1

Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses chpdifbnd.a 
|- ( ph -> A e. RR+ )
chpdifbnd.1 
|- ( ph -> 1 <_ A )
chpdifbnd.b 
|- ( ph -> B e. RR+ )
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 )
chpdifbnd.c 
|- C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )
chpdifbnd.x 
|- ( ph -> X e. ( 1 (,) +oo ) )
chpdifbnd.y 
|- ( ph -> Y e. ( X [,] ( A x. X ) ) )
Assertion chpdifbndlem1 
|- ( ph -> ( ( psi ` Y ) - ( psi ` X ) ) <_ ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) )

Proof

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