Metamath Proof Explorer


Theorem pntlemb

Description: Lemma for pnt . Unpack all the lower bounds contained in W , in the form they will be used. For comparison with Equation 10.6.27 of Shapiro, p. 434, Z is x. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a
|- ( ph -> A e. RR+ )
pntlem1.b
|- ( ph -> B e. RR+ )
pntlem1.l
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d
|- D = ( A + 1 )
pntlem1.f
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlem1.u
|- ( ph -> U e. RR+ )
pntlem1.u2
|- ( ph -> U <_ A )
pntlem1.e
|- E = ( U / D )
pntlem1.k
|- K = ( exp ` ( B / E ) )
pntlem1.y
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c
|- ( ph -> C e. RR+ )
pntlem1.w
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
pntlem1.z
|- ( ph -> Z e. ( W [,) +oo ) )
Assertion pntlemb
|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem1.a
 |-  ( ph -> A e. RR+ )
3 pntlem1.b
 |-  ( ph -> B e. RR+ )
4 pntlem1.l
 |-  ( ph -> L e. ( 0 (,) 1 ) )
5 pntlem1.d
 |-  D = ( A + 1 )
6 pntlem1.f
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7 pntlem1.u
 |-  ( ph -> U e. RR+ )
8 pntlem1.u2
 |-  ( ph -> U <_ A )
9 pntlem1.e
 |-  E = ( U / D )
10 pntlem1.k
 |-  K = ( exp ` ( B / E ) )
11 pntlem1.y
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12 pntlem1.x
 |-  ( ph -> ( X e. RR+ /\ Y < X ) )
13 pntlem1.c
 |-  ( ph -> C e. RR+ )
14 pntlem1.w
 |-  W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15 pntlem1.z
 |-  ( ph -> Z e. ( W [,) +oo ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 pntlema
 |-  ( ph -> W e. RR+ )
17 16 rpred
 |-  ( ph -> W e. RR )
18 pnfxr
 |-  +oo e. RR*
19 elico2
 |-  ( ( W e. RR /\ +oo e. RR* ) -> ( Z e. ( W [,) +oo ) <-> ( Z e. RR /\ W <_ Z /\ Z < +oo ) ) )
20 17 18 19 sylancl
 |-  ( ph -> ( Z e. ( W [,) +oo ) <-> ( Z e. RR /\ W <_ Z /\ Z < +oo ) ) )
21 15 20 mpbid
 |-  ( ph -> ( Z e. RR /\ W <_ Z /\ Z < +oo ) )
22 21 simp1d
 |-  ( ph -> Z e. RR )
23 21 simp2d
 |-  ( ph -> W <_ Z )
24 22 16 23 rpgecld
 |-  ( ph -> Z e. RR+ )
25 1re
 |-  1 e. RR
26 25 a1i
 |-  ( ph -> 1 e. RR )
27 ere
 |-  _e e. RR
28 27 a1i
 |-  ( ph -> _e e. RR )
29 24 rpsqrtcld
 |-  ( ph -> ( sqrt ` Z ) e. RR+ )
30 29 rpred
 |-  ( ph -> ( sqrt ` Z ) e. RR )
31 1lt2
 |-  1 < 2
32 egt2lt3
 |-  ( 2 < _e /\ _e < 3 )
33 32 simpli
 |-  2 < _e
34 2re
 |-  2 e. RR
35 25 34 27 lttri
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
36 31 33 35 mp2an
 |-  1 < _e
37 36 a1i
 |-  ( ph -> 1 < _e )
38 4re
 |-  4 e. RR
39 38 a1i
 |-  ( ph -> 4 e. RR )
40 32 simpri
 |-  _e < 3
41 3lt4
 |-  3 < 4
42 3re
 |-  3 e. RR
43 27 42 38 lttri
 |-  ( ( _e < 3 /\ 3 < 4 ) -> _e < 4 )
44 40 41 43 mp2an
 |-  _e < 4
45 44 a1i
 |-  ( ph -> _e < 4 )
46 4nn
 |-  4 e. NN
47 nnrp
 |-  ( 4 e. NN -> 4 e. RR+ )
48 46 47 ax-mp
 |-  4 e. RR+
49 1 2 3 4 5 6 pntlemd
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
50 49 simp1d
 |-  ( ph -> L e. RR+ )
51 1 2 3 4 5 6 7 8 9 10 pntlemc
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
52 51 simp1d
 |-  ( ph -> E e. RR+ )
53 50 52 rpmulcld
 |-  ( ph -> ( L x. E ) e. RR+ )
54 rpdivcl
 |-  ( ( 4 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 4 / ( L x. E ) ) e. RR+ )
55 48 53 54 sylancr
 |-  ( ph -> ( 4 / ( L x. E ) ) e. RR+ )
56 55 rpred
 |-  ( ph -> ( 4 / ( L x. E ) ) e. RR )
57 53 rpred
 |-  ( ph -> ( L x. E ) e. RR )
58 52 rpred
 |-  ( ph -> E e. RR )
59 50 rpred
 |-  ( ph -> L e. RR )
60 eliooord
 |-  ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
61 4 60 syl
 |-  ( ph -> ( 0 < L /\ L < 1 ) )
62 61 simprd
 |-  ( ph -> L < 1 )
63 59 26 52 62 ltmul1dd
 |-  ( ph -> ( L x. E ) < ( 1 x. E ) )
64 52 rpcnd
 |-  ( ph -> E e. CC )
65 64 mulid2d
 |-  ( ph -> ( 1 x. E ) = E )
66 63 65 breqtrd
 |-  ( ph -> ( L x. E ) < E )
67 51 simp3d
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
68 67 simp1d
 |-  ( ph -> E e. ( 0 (,) 1 ) )
69 eliooord
 |-  ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
70 68 69 syl
 |-  ( ph -> ( 0 < E /\ E < 1 ) )
71 70 simprd
 |-  ( ph -> E < 1 )
72 57 58 26 66 71 lttrd
 |-  ( ph -> ( L x. E ) < 1 )
73 4pos
 |-  0 < 4
74 39 73 jctir
 |-  ( ph -> ( 4 e. RR /\ 0 < 4 ) )
75 ltmul2
 |-  ( ( ( L x. E ) e. RR /\ 1 e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( L x. E ) < 1 <-> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) ) )
76 57 26 74 75 syl3anc
 |-  ( ph -> ( ( L x. E ) < 1 <-> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) ) )
77 72 76 mpbid
 |-  ( ph -> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) )
78 4cn
 |-  4 e. CC
79 78 mulid1i
 |-  ( 4 x. 1 ) = 4
80 77 79 breqtrdi
 |-  ( ph -> ( 4 x. ( L x. E ) ) < 4 )
81 39 39 53 ltmuldivd
 |-  ( ph -> ( ( 4 x. ( L x. E ) ) < 4 <-> 4 < ( 4 / ( L x. E ) ) ) )
82 80 81 mpbid
 |-  ( ph -> 4 < ( 4 / ( L x. E ) ) )
83 11 simpld
 |-  ( ph -> Y e. RR+ )
84 83 55 rpaddcld
 |-  ( ph -> ( Y + ( 4 / ( L x. E ) ) ) e. RR+ )
85 84 rpred
 |-  ( ph -> ( Y + ( 4 / ( L x. E ) ) ) e. RR )
86 56 83 ltaddrp2d
 |-  ( ph -> ( 4 / ( L x. E ) ) < ( Y + ( 4 / ( L x. E ) ) ) )
87 85 resqcld
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR )
88 12 simpld
 |-  ( ph -> X e. RR+ )
89 51 simp2d
 |-  ( ph -> K e. RR+ )
90 2z
 |-  2 e. ZZ
91 rpexpcl
 |-  ( ( K e. RR+ /\ 2 e. ZZ ) -> ( K ^ 2 ) e. RR+ )
92 89 90 91 sylancl
 |-  ( ph -> ( K ^ 2 ) e. RR+ )
93 88 92 rpmulcld
 |-  ( ph -> ( X x. ( K ^ 2 ) ) e. RR+ )
94 4z
 |-  4 e. ZZ
95 rpexpcl
 |-  ( ( ( X x. ( K ^ 2 ) ) e. RR+ /\ 4 e. ZZ ) -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
96 93 94 95 sylancl
 |-  ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
97 3nn0
 |-  3 e. NN0
98 2nn
 |-  2 e. NN
99 97 98 decnncl
 |-  ; 3 2 e. NN
100 nnrp
 |-  ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
101 99 100 ax-mp
 |-  ; 3 2 e. RR+
102 rpmulcl
 |-  ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
103 101 3 102 sylancr
 |-  ( ph -> ( ; 3 2 x. B ) e. RR+ )
104 67 simp3d
 |-  ( ph -> ( U - E ) e. RR+ )
105 rpexpcl
 |-  ( ( E e. RR+ /\ 2 e. ZZ ) -> ( E ^ 2 ) e. RR+ )
106 52 90 105 sylancl
 |-  ( ph -> ( E ^ 2 ) e. RR+ )
107 50 106 rpmulcld
 |-  ( ph -> ( L x. ( E ^ 2 ) ) e. RR+ )
108 104 107 rpmulcld
 |-  ( ph -> ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. RR+ )
109 103 108 rpdivcld
 |-  ( ph -> ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) e. RR+ )
110 3rp
 |-  3 e. RR+
111 rpmulcl
 |-  ( ( U e. RR+ /\ 3 e. RR+ ) -> ( U x. 3 ) e. RR+ )
112 7 110 111 sylancl
 |-  ( ph -> ( U x. 3 ) e. RR+ )
113 112 13 rpaddcld
 |-  ( ph -> ( ( U x. 3 ) + C ) e. RR+ )
114 109 113 rpmulcld
 |-  ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR+ )
115 114 rpred
 |-  ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR )
116 115 rpefcld
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) e. RR+ )
117 96 116 rpaddcld
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. RR+ )
118 87 117 ltaddrpd
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) )
119 118 14 breqtrrdi
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < W )
120 87 17 22 119 23 ltletrd
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < Z )
121 24 rprege0d
 |-  ( ph -> ( Z e. RR /\ 0 <_ Z ) )
122 resqrtth
 |-  ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) ^ 2 ) = Z )
123 121 122 syl
 |-  ( ph -> ( ( sqrt ` Z ) ^ 2 ) = Z )
124 120 123 breqtrrd
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) )
125 84 rprege0d
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) e. RR /\ 0 <_ ( Y + ( 4 / ( L x. E ) ) ) ) )
126 29 rprege0d
 |-  ( ph -> ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) )
127 lt2sq
 |-  ( ( ( ( Y + ( 4 / ( L x. E ) ) ) e. RR /\ 0 <_ ( Y + ( 4 / ( L x. E ) ) ) ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) <-> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
128 125 126 127 syl2anc
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) <-> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
129 124 128 mpbird
 |-  ( ph -> ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) )
130 56 85 30 86 129 lttrd
 |-  ( ph -> ( 4 / ( L x. E ) ) < ( sqrt ` Z ) )
131 39 56 30 82 130 lttrd
 |-  ( ph -> 4 < ( sqrt ` Z ) )
132 28 39 30 45 131 lttrd
 |-  ( ph -> _e < ( sqrt ` Z ) )
133 26 28 30 37 132 lttrd
 |-  ( ph -> 1 < ( sqrt ` Z ) )
134 0le1
 |-  0 <_ 1
135 134 a1i
 |-  ( ph -> 0 <_ 1 )
136 lt2sq
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( 1 < ( sqrt ` Z ) <-> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
137 26 135 126 136 syl21anc
 |-  ( ph -> ( 1 < ( sqrt ` Z ) <-> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
138 133 137 mpbid
 |-  ( ph -> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) )
139 sq1
 |-  ( 1 ^ 2 ) = 1
140 139 a1i
 |-  ( ph -> ( 1 ^ 2 ) = 1 )
141 138 140 123 3brtr3d
 |-  ( ph -> 1 < Z )
142 28 30 132 ltled
 |-  ( ph -> _e <_ ( sqrt ` Z ) )
143 22 83 rerpdivcld
 |-  ( ph -> ( Z / Y ) e. RR )
144 83 rpred
 |-  ( ph -> Y e. RR )
145 144 55 ltaddrpd
 |-  ( ph -> Y < ( Y + ( 4 / ( L x. E ) ) ) )
146 144 85 30 145 129 lttrd
 |-  ( ph -> Y < ( sqrt ` Z ) )
147 144 30 29 146 ltmul2dd
 |-  ( ph -> ( ( sqrt ` Z ) x. Y ) < ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
148 remsqsqrt
 |-  ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
149 121 148 syl
 |-  ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
150 147 149 breqtrd
 |-  ( ph -> ( ( sqrt ` Z ) x. Y ) < Z )
151 30 22 83 ltmuldivd
 |-  ( ph -> ( ( ( sqrt ` Z ) x. Y ) < Z <-> ( sqrt ` Z ) < ( Z / Y ) ) )
152 150 151 mpbid
 |-  ( ph -> ( sqrt ` Z ) < ( Z / Y ) )
153 30 143 152 ltled
 |-  ( ph -> ( sqrt ` Z ) <_ ( Z / Y ) )
154 141 142 153 3jca
 |-  ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
155 56 30 130 ltled
 |-  ( ph -> ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) )
156 88 relogcld
 |-  ( ph -> ( log ` X ) e. RR )
157 89 rpred
 |-  ( ph -> K e. RR )
158 67 simp2d
 |-  ( ph -> 1 < K )
159 157 158 rplogcld
 |-  ( ph -> ( log ` K ) e. RR+ )
160 156 159 rerpdivcld
 |-  ( ph -> ( ( log ` X ) / ( log ` K ) ) e. RR )
161 readdcl
 |-  ( ( ( ( log ` X ) / ( log ` K ) ) e. RR /\ 2 e. RR ) -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) e. RR )
162 160 34 161 sylancl
 |-  ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) e. RR )
163 24 relogcld
 |-  ( ph -> ( log ` Z ) e. RR )
164 163 159 rerpdivcld
 |-  ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR )
165 nndivre
 |-  ( ( ( ( log ` Z ) / ( log ` K ) ) e. RR /\ 4 e. NN ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
166 164 46 165 sylancl
 |-  ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
167 93 relogcld
 |-  ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) e. RR )
168 nndivre
 |-  ( ( ( log ` Z ) e. RR /\ 4 e. NN ) -> ( ( log ` Z ) / 4 ) e. RR )
169 163 46 168 sylancl
 |-  ( ph -> ( ( log ` Z ) / 4 ) e. RR )
170 relogexp
 |-  ( ( ( X x. ( K ^ 2 ) ) e. RR+ /\ 4 e. ZZ ) -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) = ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) )
171 93 94 170 sylancl
 |-  ( ph -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) = ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) )
172 96 rpred
 |-  ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR )
173 117 rpred
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. RR )
174 172 116 ltaddrpd
 |-  ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) < ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
175 rpexpcl
 |-  ( ( ( Y + ( 4 / ( L x. E ) ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
176 84 90 175 sylancl
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
177 173 176 ltaddrpd
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
178 87 recnd
 |-  ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. CC )
179 117 rpcnd
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. CC )
180 178 179 addcomd
 |-  ( ph -> ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) = ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
181 14 180 syl5eq
 |-  ( ph -> W = ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
182 177 181 breqtrrd
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < W )
183 173 17 22 182 23 ltletrd
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < Z )
184 172 173 22 174 183 lttrd
 |-  ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z )
185 logltb
 |-  ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ /\ Z e. RR+ ) -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z <-> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) ) )
186 96 24 185 syl2anc
 |-  ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z <-> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) ) )
187 184 186 mpbid
 |-  ( ph -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) )
188 171 187 eqbrtrrd
 |-  ( ph -> ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) )
189 ltmuldiv2
 |-  ( ( ( log ` ( X x. ( K ^ 2 ) ) ) e. RR /\ ( log ` Z ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) <-> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) ) )
190 167 163 74 189 syl3anc
 |-  ( ph -> ( ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) <-> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) ) )
191 188 190 mpbid
 |-  ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) )
192 167 169 159 191 ltdiv1dd
 |-  ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) < ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) )
193 88 92 relogmuld
 |-  ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) = ( ( log ` X ) + ( log ` ( K ^ 2 ) ) ) )
194 relogexp
 |-  ( ( K e. RR+ /\ 2 e. ZZ ) -> ( log ` ( K ^ 2 ) ) = ( 2 x. ( log ` K ) ) )
195 89 90 194 sylancl
 |-  ( ph -> ( log ` ( K ^ 2 ) ) = ( 2 x. ( log ` K ) ) )
196 195 oveq2d
 |-  ( ph -> ( ( log ` X ) + ( log ` ( K ^ 2 ) ) ) = ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) )
197 193 196 eqtrd
 |-  ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) = ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) )
198 197 oveq1d
 |-  ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) )
199 156 recnd
 |-  ( ph -> ( log ` X ) e. CC )
200 2cnd
 |-  ( ph -> 2 e. CC )
201 159 rpcnd
 |-  ( ph -> ( log ` K ) e. CC )
202 200 201 mulcld
 |-  ( ph -> ( 2 x. ( log ` K ) ) e. CC )
203 159 rpcnne0d
 |-  ( ph -> ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) )
204 divdir
 |-  ( ( ( log ` X ) e. CC /\ ( 2 x. ( log ` K ) ) e. CC /\ ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) ) -> ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) )
205 199 202 203 204 syl3anc
 |-  ( ph -> ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) )
206 203 simprd
 |-  ( ph -> ( log ` K ) =/= 0 )
207 200 201 206 divcan4d
 |-  ( ph -> ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) = 2 )
208 207 oveq2d
 |-  ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) = ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
209 198 205 208 3eqtrd
 |-  ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
210 163 recnd
 |-  ( ph -> ( log ` Z ) e. CC )
211 rpcnne0
 |-  ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) )
212 48 211 mp1i
 |-  ( ph -> ( 4 e. CC /\ 4 =/= 0 ) )
213 divdiv32
 |-  ( ( ( log ` Z ) e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) /\ ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) ) -> ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
214 210 212 203 213 syl3anc
 |-  ( ph -> ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
215 192 209 214 3brtr3d
 |-  ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) < ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
216 162 166 215 ltled
 |-  ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
217 113 rpred
 |-  ( ph -> ( ( U x. 3 ) + C ) e. RR )
218 108 103 rpdivcld
 |-  ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) e. RR+ )
219 218 rpred
 |-  ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) e. RR )
220 219 163 remulcld
 |-  ( ph -> ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) e. RR )
221 113 rpcnd
 |-  ( ph -> ( ( U x. 3 ) + C ) e. CC )
222 108 rpcnne0d
 |-  ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) )
223 103 rpcnne0d
 |-  ( ph -> ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) )
224 divdiv2
 |-  ( ( ( ( U x. 3 ) + C ) e. CC /\ ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
225 221 222 223 224 syl3anc
 |-  ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
226 103 rpcnd
 |-  ( ph -> ( ; 3 2 x. B ) e. CC )
227 221 226 mulcomd
 |-  ( ph -> ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) = ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) )
228 227 oveq1d
 |-  ( ph -> ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
229 div23
 |-  ( ( ( ; 3 2 x. B ) e. CC /\ ( ( U x. 3 ) + C ) e. CC /\ ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) ) -> ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
230 226 221 222 229 syl3anc
 |-  ( ph -> ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
231 225 228 230 3eqtrd
 |-  ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
232 115 reefcld
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) e. RR )
233 232 96 ltaddrp2d
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
234 232 173 22 233 183 lttrd
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < Z )
235 24 reeflogd
 |-  ( ph -> ( exp ` ( log ` Z ) ) = Z )
236 234 235 breqtrrd
 |-  ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) )
237 eflt
 |-  ( ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR /\ ( log ` Z ) e. RR ) -> ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) <-> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) ) )
238 115 163 237 syl2anc
 |-  ( ph -> ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) <-> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) ) )
239 236 238 mpbird
 |-  ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) )
240 231 239 eqbrtrd
 |-  ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) < ( log ` Z ) )
241 217 163 218 ltdivmuld
 |-  ( ph -> ( ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) < ( log ` Z ) <-> ( ( U x. 3 ) + C ) < ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) ) )
242 240 241 mpbid
 |-  ( ph -> ( ( U x. 3 ) + C ) < ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
243 217 220 242 ltled
 |-  ( ph -> ( ( U x. 3 ) + C ) <_ ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
244 104 rpcnd
 |-  ( ph -> ( U - E ) e. CC )
245 107 rpcnd
 |-  ( ph -> ( L x. ( E ^ 2 ) ) e. CC )
246 divass
 |-  ( ( ( U - E ) e. CC /\ ( L x. ( E ^ 2 ) ) e. CC /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) = ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) )
247 244 245 223 246 syl3anc
 |-  ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) = ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) )
248 247 oveq1d
 |-  ( ph -> ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) = ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) )
249 243 248 breqtrd
 |-  ( ph -> ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) )
250 155 216 249 3jca
 |-  ( ph -> ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
251 24 154 250 3jca
 |-  ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )