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