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 |
|
pntlem1.m |
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) |
17 |
|
pntlem1.n |
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) |
18 |
|
pntlem1.U |
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U ) |
19 |
|
pntlem1.K |
|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) |
20 |
|
pntlem1.o |
|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) |
21 |
|
pntlem1.v |
|- ( ph -> V e. RR+ ) |
22 |
|
pntlem1.V |
|- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) |
23 |
|
pntlem1.j |
|- ( ph -> J e. ( M ..^ N ) ) |
24 |
|
pntlem1.i |
|- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) |
25 |
1 2 3 4 5 6
|
pntlemd |
|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) ) |
26 |
25
|
simp1d |
|- ( ph -> L e. RR+ ) |
27 |
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+ ) ) ) |
28 |
27
|
simp1d |
|- ( ph -> E e. RR+ ) |
29 |
26 28
|
rpmulcld |
|- ( ph -> ( L x. E ) e. RR+ ) |
30 |
|
4re |
|- 4 e. RR |
31 |
|
4pos |
|- 0 < 4 |
32 |
30 31
|
elrpii |
|- 4 e. RR+ |
33 |
|
rpdivcl |
|- ( ( ( L x. E ) e. RR+ /\ 4 e. RR+ ) -> ( ( L x. E ) / 4 ) e. RR+ ) |
34 |
29 32 33
|
sylancl |
|- ( ph -> ( ( L x. E ) / 4 ) e. RR+ ) |
35 |
34
|
rpred |
|- ( ph -> ( ( L x. E ) / 4 ) e. RR ) |
36 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
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 ) ) ) ) ) |
37 |
36
|
simp1d |
|- ( ph -> Z e. RR+ ) |
38 |
37 21
|
rpdivcld |
|- ( ph -> ( Z / V ) e. RR+ ) |
39 |
38
|
rpred |
|- ( ph -> ( Z / V ) e. RR ) |
40 |
35 39
|
remulcld |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. RR ) |
41 |
|
fzfid |
|- ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) e. Fin ) |
42 |
24 41
|
eqeltrid |
|- ( ph -> I e. Fin ) |
43 |
|
hashcl |
|- ( I e. Fin -> ( # ` I ) e. NN0 ) |
44 |
42 43
|
syl |
|- ( ph -> ( # ` I ) e. NN0 ) |
45 |
44
|
nn0red |
|- ( ph -> ( # ` I ) e. RR ) |
46 |
40
|
recnd |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. CC ) |
47 |
|
1rp |
|- 1 e. RR+ |
48 |
|
rpaddcl |
|- ( ( 1 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 1 + ( L x. E ) ) e. RR+ ) |
49 |
47 29 48
|
sylancr |
|- ( ph -> ( 1 + ( L x. E ) ) e. RR+ ) |
50 |
49 21
|
rpmulcld |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR+ ) |
51 |
37 50
|
rpdivcld |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR+ ) |
52 |
51
|
rpred |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR ) |
53 |
|
reflcl |
|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR ) |
54 |
52 53
|
syl |
|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR ) |
55 |
54
|
recnd |
|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. CC ) |
56 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
57 |
46 55 56
|
add32d |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) = ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
58 |
|
peano2re |
|- ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. RR -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) e. RR ) |
59 |
40 58
|
syl |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) e. RR ) |
60 |
59 54
|
readdcld |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) e. RR ) |
61 |
|
reflcl |
|- ( ( Z / V ) e. RR -> ( |_ ` ( Z / V ) ) e. RR ) |
62 |
39 61
|
syl |
|- ( ph -> ( |_ ` ( Z / V ) ) e. RR ) |
63 |
|
peano2re |
|- ( ( |_ ` ( Z / V ) ) e. RR -> ( ( |_ ` ( Z / V ) ) + 1 ) e. RR ) |
64 |
62 63
|
syl |
|- ( ph -> ( ( |_ ` ( Z / V ) ) + 1 ) e. RR ) |
65 |
29
|
rphalfcld |
|- ( ph -> ( ( L x. E ) / 2 ) e. RR+ ) |
66 |
65 38
|
rpmulcld |
|- ( ph -> ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) e. RR+ ) |
67 |
66
|
rpred |
|- ( ph -> ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) e. RR ) |
68 |
67 52
|
readdcld |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR ) |
69 |
|
rpdivcl |
|- ( ( 4 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 4 / ( L x. E ) ) e. RR+ ) |
70 |
32 29 69
|
sylancr |
|- ( ph -> ( 4 / ( L x. E ) ) e. RR+ ) |
71 |
70
|
rpred |
|- ( ph -> ( 4 / ( L x. E ) ) e. RR ) |
72 |
37
|
rpsqrtcld |
|- ( ph -> ( sqrt ` Z ) e. RR+ ) |
73 |
72
|
rpred |
|- ( ph -> ( sqrt ` Z ) e. RR ) |
74 |
36
|
simp3d |
|- ( 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 ) ) ) ) |
75 |
74
|
simp1d |
|- ( ph -> ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) ) |
76 |
50
|
rpred |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR ) |
77 |
27
|
simp2d |
|- ( ph -> K e. RR+ ) |
78 |
|
elfzoelz |
|- ( J e. ( M ..^ N ) -> J e. ZZ ) |
79 |
23 78
|
syl |
|- ( ph -> J e. ZZ ) |
80 |
79
|
peano2zd |
|- ( ph -> ( J + 1 ) e. ZZ ) |
81 |
77 80
|
rpexpcld |
|- ( ph -> ( K ^ ( J + 1 ) ) e. RR+ ) |
82 |
81
|
rpred |
|- ( ph -> ( K ^ ( J + 1 ) ) e. RR ) |
83 |
22
|
simplrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) |
84 |
77
|
rpcnd |
|- ( ph -> K e. CC ) |
85 |
77 79
|
rpexpcld |
|- ( ph -> ( K ^ J ) e. RR+ ) |
86 |
85
|
rpcnd |
|- ( ph -> ( K ^ J ) e. CC ) |
87 |
84 86
|
mulcomd |
|- ( ph -> ( K x. ( K ^ J ) ) = ( ( K ^ J ) x. K ) ) |
88 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemg |
|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) ) |
89 |
88
|
simp1d |
|- ( ph -> M e. NN ) |
90 |
|
elfzouz |
|- ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) ) |
91 |
23 90
|
syl |
|- ( ph -> J e. ( ZZ>= ` M ) ) |
92 |
|
eluznn |
|- ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN ) |
93 |
89 91 92
|
syl2anc |
|- ( ph -> J e. NN ) |
94 |
93
|
nnnn0d |
|- ( ph -> J e. NN0 ) |
95 |
84 94
|
expp1d |
|- ( ph -> ( K ^ ( J + 1 ) ) = ( ( K ^ J ) x. K ) ) |
96 |
87 95
|
eqtr4d |
|- ( ph -> ( K x. ( K ^ J ) ) = ( K ^ ( J + 1 ) ) ) |
97 |
83 96
|
breqtrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K ^ ( J + 1 ) ) ) |
98 |
76 82 97
|
ltled |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) ) |
99 |
|
fzofzp1 |
|- ( J e. ( M ..^ N ) -> ( J + 1 ) e. ( M ... N ) ) |
100 |
23 99
|
syl |
|- ( ph -> ( J + 1 ) e. ( M ... N ) ) |
101 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemh |
|- ( ( ph /\ ( J + 1 ) e. ( M ... N ) ) -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) ) |
102 |
100 101
|
mpdan |
|- ( ph -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) ) |
103 |
102
|
simprd |
|- ( ph -> ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) |
104 |
76 82 73 98 103
|
letrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) ) |
105 |
76 73 72
|
lemul2d |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) <-> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) ) |
106 |
104 105
|
mpbid |
|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) |
107 |
37
|
rprege0d |
|- ( ph -> ( Z e. RR /\ 0 <_ Z ) ) |
108 |
|
remsqsqrt |
|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
109 |
107 108
|
syl |
|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z ) |
110 |
106 109
|
breqtrd |
|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z ) |
111 |
37
|
rpred |
|- ( ph -> Z e. RR ) |
112 |
73 111 50
|
lemuldivd |
|- ( ph -> ( ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z <-> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
113 |
110 112
|
mpbid |
|- ( ph -> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
114 |
21
|
rpcnd |
|- ( ph -> V e. CC ) |
115 |
114
|
mulid2d |
|- ( ph -> ( 1 x. V ) = V ) |
116 |
|
1red |
|- ( ph -> 1 e. RR ) |
117 |
49
|
rpred |
|- ( ph -> ( 1 + ( L x. E ) ) e. RR ) |
118 |
|
1re |
|- 1 e. RR |
119 |
|
ltaddrp |
|- ( ( 1 e. RR /\ ( L x. E ) e. RR+ ) -> 1 < ( 1 + ( L x. E ) ) ) |
120 |
118 29 119
|
sylancr |
|- ( ph -> 1 < ( 1 + ( L x. E ) ) ) |
121 |
116 117 21 120
|
ltmul1dd |
|- ( ph -> ( 1 x. V ) < ( ( 1 + ( L x. E ) ) x. V ) ) |
122 |
115 121
|
eqbrtrrd |
|- ( ph -> V < ( ( 1 + ( L x. E ) ) x. V ) ) |
123 |
21 50 37
|
ltdiv2d |
|- ( ph -> ( V < ( ( 1 + ( L x. E ) ) x. V ) <-> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) < ( Z / V ) ) ) |
124 |
122 123
|
mpbid |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) < ( Z / V ) ) |
125 |
52 39 124
|
ltled |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( Z / V ) ) |
126 |
73 52 39 113 125
|
letrd |
|- ( ph -> ( sqrt ` Z ) <_ ( Z / V ) ) |
127 |
71 73 39 75 126
|
letrd |
|- ( ph -> ( 4 / ( L x. E ) ) <_ ( Z / V ) ) |
128 |
71 39 39 127
|
leadd2dd |
|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( ( Z / V ) + ( Z / V ) ) ) |
129 |
38
|
rpcnd |
|- ( ph -> ( Z / V ) e. CC ) |
130 |
129
|
2timesd |
|- ( ph -> ( 2 x. ( Z / V ) ) = ( ( Z / V ) + ( Z / V ) ) ) |
131 |
128 130
|
breqtrrd |
|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( 2 x. ( Z / V ) ) ) |
132 |
39 71
|
readdcld |
|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) e. RR ) |
133 |
|
2re |
|- 2 e. RR |
134 |
|
remulcl |
|- ( ( 2 e. RR /\ ( Z / V ) e. RR ) -> ( 2 x. ( Z / V ) ) e. RR ) |
135 |
133 39 134
|
sylancr |
|- ( ph -> ( 2 x. ( Z / V ) ) e. RR ) |
136 |
132 135 34
|
lemul2d |
|- ( ph -> ( ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( 2 x. ( Z / V ) ) <-> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) <_ ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) ) ) |
137 |
131 136
|
mpbid |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) <_ ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) ) |
138 |
34
|
rpcnd |
|- ( ph -> ( ( L x. E ) / 4 ) e. CC ) |
139 |
70
|
rpcnd |
|- ( ph -> ( 4 / ( L x. E ) ) e. CC ) |
140 |
138 129 139
|
adddid |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) ) ) |
141 |
29
|
rpcnne0d |
|- ( ph -> ( ( L x. E ) e. CC /\ ( L x. E ) =/= 0 ) ) |
142 |
|
rpcnne0 |
|- ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) ) |
143 |
32 142
|
mp1i |
|- ( ph -> ( 4 e. CC /\ 4 =/= 0 ) ) |
144 |
|
divcan6 |
|- ( ( ( ( L x. E ) e. CC /\ ( L x. E ) =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) = 1 ) |
145 |
141 143 144
|
syl2anc |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) = 1 ) |
146 |
145
|
oveq2d |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) ) |
147 |
140 146
|
eqtrd |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) ) |
148 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
149 |
138 148 129
|
mulassd |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. 2 ) x. ( Z / V ) ) = ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) ) |
150 |
29
|
rpcnd |
|- ( ph -> ( L x. E ) e. CC ) |
151 |
|
2rp |
|- 2 e. RR+ |
152 |
|
rpcnne0 |
|- ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) ) |
153 |
151 152
|
mp1i |
|- ( ph -> ( 2 e. CC /\ 2 =/= 0 ) ) |
154 |
|
divdiv1 |
|- ( ( ( L x. E ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( L x. E ) / 2 ) / 2 ) = ( ( L x. E ) / ( 2 x. 2 ) ) ) |
155 |
150 153 153 154
|
syl3anc |
|- ( ph -> ( ( ( L x. E ) / 2 ) / 2 ) = ( ( L x. E ) / ( 2 x. 2 ) ) ) |
156 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
157 |
156
|
oveq2i |
|- ( ( L x. E ) / ( 2 x. 2 ) ) = ( ( L x. E ) / 4 ) |
158 |
155 157
|
eqtr2di |
|- ( ph -> ( ( L x. E ) / 4 ) = ( ( ( L x. E ) / 2 ) / 2 ) ) |
159 |
158
|
oveq1d |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. 2 ) = ( ( ( ( L x. E ) / 2 ) / 2 ) x. 2 ) ) |
160 |
150
|
halfcld |
|- ( ph -> ( ( L x. E ) / 2 ) e. CC ) |
161 |
153
|
simprd |
|- ( ph -> 2 =/= 0 ) |
162 |
160 148 161
|
divcan1d |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) / 2 ) x. 2 ) = ( ( L x. E ) / 2 ) ) |
163 |
159 162
|
eqtrd |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. 2 ) = ( ( L x. E ) / 2 ) ) |
164 |
163
|
oveq1d |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. 2 ) x. ( Z / V ) ) = ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) ) |
165 |
149 164
|
eqtr3d |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) = ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) ) |
166 |
137 147 165
|
3brtr3d |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) <_ ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) ) |
167 |
|
flle |
|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
168 |
52 167
|
syl |
|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) |
169 |
59 54 67 52 166 168
|
le2addd |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) <_ ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
170 |
65
|
rpred |
|- ( ph -> ( ( L x. E ) / 2 ) e. RR ) |
171 |
49
|
rprecred |
|- ( ph -> ( 1 / ( 1 + ( L x. E ) ) ) e. RR ) |
172 |
170 171
|
readdcld |
|- ( ph -> ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) e. RR ) |
173 |
29
|
rpred |
|- ( ph -> ( L x. E ) e. RR ) |
174 |
28
|
rpred |
|- ( ph -> E e. RR ) |
175 |
26
|
rpred |
|- ( ph -> L e. RR ) |
176 |
|
eliooord |
|- ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) ) |
177 |
4 176
|
syl |
|- ( ph -> ( 0 < L /\ L < 1 ) ) |
178 |
177
|
simprd |
|- ( ph -> L < 1 ) |
179 |
175 116 28 178
|
ltmul1dd |
|- ( ph -> ( L x. E ) < ( 1 x. E ) ) |
180 |
28
|
rpcnd |
|- ( ph -> E e. CC ) |
181 |
180
|
mulid2d |
|- ( ph -> ( 1 x. E ) = E ) |
182 |
179 181
|
breqtrd |
|- ( ph -> ( L x. E ) < E ) |
183 |
27
|
simp3d |
|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) |
184 |
183
|
simp1d |
|- ( ph -> E e. ( 0 (,) 1 ) ) |
185 |
|
eliooord |
|- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) ) |
186 |
184 185
|
syl |
|- ( ph -> ( 0 < E /\ E < 1 ) ) |
187 |
186
|
simprd |
|- ( ph -> E < 1 ) |
188 |
173 174 116 182 187
|
lttrd |
|- ( ph -> ( L x. E ) < 1 ) |
189 |
173 116 116 188
|
ltadd2dd |
|- ( ph -> ( 1 + ( L x. E ) ) < ( 1 + 1 ) ) |
190 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
191 |
189 190
|
breqtrrdi |
|- ( ph -> ( 1 + ( L x. E ) ) < 2 ) |
192 |
49
|
rpregt0d |
|- ( ph -> ( ( 1 + ( L x. E ) ) e. RR /\ 0 < ( 1 + ( L x. E ) ) ) ) |
193 |
133
|
a1i |
|- ( ph -> 2 e. RR ) |
194 |
|
2pos |
|- 0 < 2 |
195 |
194
|
a1i |
|- ( ph -> 0 < 2 ) |
196 |
29
|
rpregt0d |
|- ( ph -> ( ( L x. E ) e. RR /\ 0 < ( L x. E ) ) ) |
197 |
|
ltdiv2 |
|- ( ( ( ( 1 + ( L x. E ) ) e. RR /\ 0 < ( 1 + ( L x. E ) ) ) /\ ( 2 e. RR /\ 0 < 2 ) /\ ( ( L x. E ) e. RR /\ 0 < ( L x. E ) ) ) -> ( ( 1 + ( L x. E ) ) < 2 <-> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) ) |
198 |
192 193 195 196 197
|
syl121anc |
|- ( ph -> ( ( 1 + ( L x. E ) ) < 2 <-> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) ) |
199 |
191 198
|
mpbid |
|- ( ph -> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) |
200 |
49
|
rpcnd |
|- ( ph -> ( 1 + ( L x. E ) ) e. CC ) |
201 |
49
|
rpcnne0d |
|- ( ph -> ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) ) |
202 |
|
divsubdir |
|- ( ( ( 1 + ( L x. E ) ) e. CC /\ 1 e. CC /\ ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) ) -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) ) |
203 |
200 56 201 202
|
syl3anc |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) ) |
204 |
|
ax-1cn |
|- 1 e. CC |
205 |
|
pncan2 |
|- ( ( 1 e. CC /\ ( L x. E ) e. CC ) -> ( ( 1 + ( L x. E ) ) - 1 ) = ( L x. E ) ) |
206 |
204 150 205
|
sylancr |
|- ( ph -> ( ( 1 + ( L x. E ) ) - 1 ) = ( L x. E ) ) |
207 |
206
|
oveq1d |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) |
208 |
|
divid |
|- ( ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) -> ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) = 1 ) |
209 |
201 208
|
syl |
|- ( ph -> ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) = 1 ) |
210 |
209
|
oveq1d |
|- ( ph -> ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) = ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) ) |
211 |
203 207 210
|
3eqtr3d |
|- ( ph -> ( ( L x. E ) / ( 1 + ( L x. E ) ) ) = ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) ) |
212 |
199 211
|
breqtrd |
|- ( ph -> ( ( L x. E ) / 2 ) < ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) ) |
213 |
170 171 116
|
ltaddsubd |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) < 1 <-> ( ( L x. E ) / 2 ) < ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) ) ) |
214 |
212 213
|
mpbird |
|- ( ph -> ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) < 1 ) |
215 |
172 116 38 214
|
ltmul1dd |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) < ( 1 x. ( Z / V ) ) ) |
216 |
|
reccl |
|- ( ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) -> ( 1 / ( 1 + ( L x. E ) ) ) e. CC ) |
217 |
201 216
|
syl |
|- ( ph -> ( 1 / ( 1 + ( L x. E ) ) ) e. CC ) |
218 |
160 217 129
|
adddird |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) ) |
219 |
200 114
|
mulcomd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) = ( V x. ( 1 + ( L x. E ) ) ) ) |
220 |
219
|
oveq2d |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) ) |
221 |
37
|
rpcnd |
|- ( ph -> Z e. CC ) |
222 |
21
|
rpcnne0d |
|- ( ph -> ( V e. CC /\ V =/= 0 ) ) |
223 |
|
divdiv1 |
|- ( ( Z e. CC /\ ( V e. CC /\ V =/= 0 ) /\ ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) ) -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) ) |
224 |
221 222 201 223
|
syl3anc |
|- ( ph -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) ) |
225 |
49
|
rpne0d |
|- ( ph -> ( 1 + ( L x. E ) ) =/= 0 ) |
226 |
129 200 225
|
divrec2d |
|- ( ph -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) |
227 |
220 224 226
|
3eqtr2d |
|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) = ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) |
228 |
227
|
oveq2d |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) ) |
229 |
218 228
|
eqtr4d |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) |
230 |
129
|
mulid2d |
|- ( ph -> ( 1 x. ( Z / V ) ) = ( Z / V ) ) |
231 |
215 229 230
|
3brtr3d |
|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) < ( Z / V ) ) |
232 |
60 68 39 169 231
|
lelttrd |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( Z / V ) ) |
233 |
|
fllep1 |
|- ( ( Z / V ) e. RR -> ( Z / V ) <_ ( ( |_ ` ( Z / V ) ) + 1 ) ) |
234 |
39 233
|
syl |
|- ( ph -> ( Z / V ) <_ ( ( |_ ` ( Z / V ) ) + 1 ) ) |
235 |
60 39 64 232 234
|
ltletrd |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( ( |_ ` ( Z / V ) ) + 1 ) ) |
236 |
57 235
|
eqbrtrd |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) < ( ( |_ ` ( Z / V ) ) + 1 ) ) |
237 |
40 54
|
readdcld |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) e. RR ) |
238 |
237 62 116
|
ltadd1d |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) <-> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) < ( ( |_ ` ( Z / V ) ) + 1 ) ) ) |
239 |
236 238
|
mpbird |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) ) |
240 |
40 54 62
|
ltaddsubd |
|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) <-> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) ) |
241 |
239 240
|
mpbid |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
242 |
39
|
flcld |
|- ( ph -> ( |_ ` ( Z / V ) ) e. ZZ ) |
243 |
|
fzval3 |
|- ( ( |_ ` ( Z / V ) ) e. ZZ -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) |
244 |
242 243
|
syl |
|- ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) |
245 |
24 244
|
eqtrid |
|- ( ph -> I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) |
246 |
245
|
fveq2d |
|- ( ph -> ( # ` I ) = ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) ) |
247 |
|
flword2 |
|- ( ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ ( Z / V ) e. RR /\ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( Z / V ) ) -> ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
248 |
52 39 125 247
|
syl3anc |
|- ( ph -> ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
249 |
|
eluzp1p1 |
|- ( ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) -> ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
250 |
248 249
|
syl |
|- ( ph -> ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
251 |
|
hashfzo |
|- ( ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) -> ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) = ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
252 |
250 251
|
syl |
|- ( ph -> ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) = ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) |
253 |
62
|
recnd |
|- ( ph -> ( |_ ` ( Z / V ) ) e. CC ) |
254 |
253 55 56
|
pnpcan2d |
|- ( ph -> ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) = ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
255 |
246 252 254
|
3eqtrd |
|- ( ph -> ( # ` I ) = ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) |
256 |
241 255
|
breqtrrd |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( # ` I ) ) |
257 |
40 45 256
|
ltled |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) <_ ( # ` I ) ) |
258 |
35 45 38
|
lemuldivd |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) <_ ( # ` I ) <-> ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) ) ) |
259 |
257 258
|
mpbid |
|- ( ph -> ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) ) |
260 |
21
|
rpred |
|- ( ph -> V e. RR ) |
261 |
76 82 73 97 103
|
ltletrd |
|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( sqrt ` Z ) ) |
262 |
260 76 73 122 261
|
lttrd |
|- ( ph -> V < ( sqrt ` Z ) ) |
263 |
260 73 262
|
ltled |
|- ( ph -> V <_ ( sqrt ` Z ) ) |
264 |
21
|
rprege0d |
|- ( ph -> ( V e. RR /\ 0 <_ V ) ) |
265 |
72
|
rprege0d |
|- ( ph -> ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) |
266 |
|
le2sq |
|- ( ( ( V e. RR /\ 0 <_ V ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( V <_ ( sqrt ` Z ) <-> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) ) |
267 |
264 265 266
|
syl2anc |
|- ( ph -> ( V <_ ( sqrt ` Z ) <-> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) ) |
268 |
263 267
|
mpbid |
|- ( ph -> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) |
269 |
|
resqrtth |
|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) ^ 2 ) = Z ) |
270 |
107 269
|
syl |
|- ( ph -> ( ( sqrt ` Z ) ^ 2 ) = Z ) |
271 |
268 270
|
breqtrd |
|- ( ph -> ( V ^ 2 ) <_ Z ) |
272 |
|
2z |
|- 2 e. ZZ |
273 |
|
rpexpcl |
|- ( ( V e. RR+ /\ 2 e. ZZ ) -> ( V ^ 2 ) e. RR+ ) |
274 |
21 272 273
|
sylancl |
|- ( ph -> ( V ^ 2 ) e. RR+ ) |
275 |
274
|
rpred |
|- ( ph -> ( V ^ 2 ) e. RR ) |
276 |
275 111 37
|
lemul2d |
|- ( ph -> ( ( V ^ 2 ) <_ Z <-> ( Z x. ( V ^ 2 ) ) <_ ( Z x. Z ) ) ) |
277 |
271 276
|
mpbid |
|- ( ph -> ( Z x. ( V ^ 2 ) ) <_ ( Z x. Z ) ) |
278 |
221
|
sqvald |
|- ( ph -> ( Z ^ 2 ) = ( Z x. Z ) ) |
279 |
277 278
|
breqtrrd |
|- ( ph -> ( Z x. ( V ^ 2 ) ) <_ ( Z ^ 2 ) ) |
280 |
111
|
resqcld |
|- ( ph -> ( Z ^ 2 ) e. RR ) |
281 |
111 280 274
|
lemuldivd |
|- ( ph -> ( ( Z x. ( V ^ 2 ) ) <_ ( Z ^ 2 ) <-> Z <_ ( ( Z ^ 2 ) / ( V ^ 2 ) ) ) ) |
282 |
279 281
|
mpbid |
|- ( ph -> Z <_ ( ( Z ^ 2 ) / ( V ^ 2 ) ) ) |
283 |
21
|
rpne0d |
|- ( ph -> V =/= 0 ) |
284 |
221 114 283
|
sqdivd |
|- ( ph -> ( ( Z / V ) ^ 2 ) = ( ( Z ^ 2 ) / ( V ^ 2 ) ) ) |
285 |
282 284
|
breqtrrd |
|- ( ph -> Z <_ ( ( Z / V ) ^ 2 ) ) |
286 |
|
rpexpcl |
|- ( ( ( Z / V ) e. RR+ /\ 2 e. ZZ ) -> ( ( Z / V ) ^ 2 ) e. RR+ ) |
287 |
38 272 286
|
sylancl |
|- ( ph -> ( ( Z / V ) ^ 2 ) e. RR+ ) |
288 |
37 287
|
logled |
|- ( ph -> ( Z <_ ( ( Z / V ) ^ 2 ) <-> ( log ` Z ) <_ ( log ` ( ( Z / V ) ^ 2 ) ) ) ) |
289 |
285 288
|
mpbid |
|- ( ph -> ( log ` Z ) <_ ( log ` ( ( Z / V ) ^ 2 ) ) ) |
290 |
|
relogexp |
|- ( ( ( Z / V ) e. RR+ /\ 2 e. ZZ ) -> ( log ` ( ( Z / V ) ^ 2 ) ) = ( 2 x. ( log ` ( Z / V ) ) ) ) |
291 |
38 272 290
|
sylancl |
|- ( ph -> ( log ` ( ( Z / V ) ^ 2 ) ) = ( 2 x. ( log ` ( Z / V ) ) ) ) |
292 |
289 291
|
breqtrd |
|- ( ph -> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) ) |
293 |
37
|
relogcld |
|- ( ph -> ( log ` Z ) e. RR ) |
294 |
38
|
relogcld |
|- ( ph -> ( log ` ( Z / V ) ) e. RR ) |
295 |
|
ledivmul |
|- ( ( ( log ` Z ) e. RR /\ ( log ` ( Z / V ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) <-> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) ) ) |
296 |
293 294 193 195 295
|
syl112anc |
|- ( ph -> ( ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) <-> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) ) ) |
297 |
292 296
|
mpbird |
|- ( ph -> ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) ) |
298 |
34
|
rprege0d |
|- ( ph -> ( ( ( L x. E ) / 4 ) e. RR /\ 0 <_ ( ( L x. E ) / 4 ) ) ) |
299 |
45 38
|
rerpdivcld |
|- ( ph -> ( ( # ` I ) / ( Z / V ) ) e. RR ) |
300 |
36
|
simp2d |
|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) ) |
301 |
300
|
simp1d |
|- ( ph -> 1 < Z ) |
302 |
111 301
|
rplogcld |
|- ( ph -> ( log ` Z ) e. RR+ ) |
303 |
302
|
rphalfcld |
|- ( ph -> ( ( log ` Z ) / 2 ) e. RR+ ) |
304 |
303
|
rprege0d |
|- ( ph -> ( ( ( log ` Z ) / 2 ) e. RR /\ 0 <_ ( ( log ` Z ) / 2 ) ) ) |
305 |
|
lemul12a |
|- ( ( ( ( ( ( L x. E ) / 4 ) e. RR /\ 0 <_ ( ( L x. E ) / 4 ) ) /\ ( ( # ` I ) / ( Z / V ) ) e. RR ) /\ ( ( ( ( log ` Z ) / 2 ) e. RR /\ 0 <_ ( ( log ` Z ) / 2 ) ) /\ ( log ` ( Z / V ) ) e. RR ) ) -> ( ( ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) /\ ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) ) |
306 |
298 299 304 294 305
|
syl22anc |
|- ( ph -> ( ( ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) /\ ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) ) |
307 |
259 297 306
|
mp2and |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) |
308 |
302
|
rpcnd |
|- ( ph -> ( log ` Z ) e. CC ) |
309 |
|
8nn |
|- 8 e. NN |
310 |
|
nnrp |
|- ( 8 e. NN -> 8 e. RR+ ) |
311 |
309 310
|
ax-mp |
|- 8 e. RR+ |
312 |
|
rpcnne0 |
|- ( 8 e. RR+ -> ( 8 e. CC /\ 8 =/= 0 ) ) |
313 |
311 312
|
mp1i |
|- ( ph -> ( 8 e. CC /\ 8 =/= 0 ) ) |
314 |
|
div23 |
|- ( ( ( L x. E ) e. CC /\ ( log ` Z ) e. CC /\ ( 8 e. CC /\ 8 =/= 0 ) ) -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) |
315 |
150 308 313 314
|
syl3anc |
|- ( ph -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) |
316 |
|
divmuldiv |
|- ( ( ( ( L x. E ) e. CC /\ ( log ` Z ) e. CC ) /\ ( ( 4 e. CC /\ 4 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) ) |
317 |
150 308 143 153 316
|
syl22anc |
|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) ) |
318 |
|
4t2e8 |
|- ( 4 x. 2 ) = 8 |
319 |
318
|
oveq2i |
|- ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) |
320 |
317 319
|
eqtr2di |
|- ( ph -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) ) |
321 |
315 320
|
eqtr3d |
|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) = ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) ) |
322 |
45
|
recnd |
|- ( ph -> ( # ` I ) e. CC ) |
323 |
294
|
recnd |
|- ( ph -> ( log ` ( Z / V ) ) e. CC ) |
324 |
38
|
rpcnne0d |
|- ( ph -> ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) |
325 |
|
divass |
|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( ( # ` I ) x. ( log ` ( Z / V ) ) ) / ( Z / V ) ) = ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) |
326 |
|
div23 |
|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( ( # ` I ) x. ( log ` ( Z / V ) ) ) / ( Z / V ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) |
327 |
325 326
|
eqtr3d |
|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) |
328 |
322 323 324 327
|
syl3anc |
|- ( ph -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) |
329 |
307 321 328
|
3brtr4d |
|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) <_ ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) |
330 |
|
rpdivcl |
|- ( ( ( L x. E ) e. RR+ /\ 8 e. RR+ ) -> ( ( L x. E ) / 8 ) e. RR+ ) |
331 |
29 311 330
|
sylancl |
|- ( ph -> ( ( L x. E ) / 8 ) e. RR+ ) |
332 |
331 302
|
rpmulcld |
|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR+ ) |
333 |
332
|
rpred |
|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR ) |
334 |
294 38
|
rerpdivcld |
|- ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR ) |
335 |
45 334
|
remulcld |
|- ( ph -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR ) |
336 |
183
|
simp3d |
|- ( ph -> ( U - E ) e. RR+ ) |
337 |
333 335 336
|
lemul2d |
|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) <_ ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <-> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) ) |
338 |
329 337
|
mpbid |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |
339 |
336
|
rpcnd |
|- ( ph -> ( U - E ) e. CC ) |
340 |
334
|
recnd |
|- ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. CC ) |
341 |
339 322 340
|
mul12d |
|- ( ph -> ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |
342 |
338 341
|
breqtrd |
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) |