Metamath Proof Explorer


Theorem ftc1anclem7

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 13-May-2018)

Ref Expression
Hypotheses ftc1anc.g G = x A B A x F t dt
ftc1anc.a φ A
ftc1anc.b φ B
ftc1anc.le φ A B
ftc1anc.s φ A B D
ftc1anc.d φ D
ftc1anc.i φ F 𝐿 1
ftc1anc.f φ F : D
Assertion ftc1anclem7 φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 + 2 t if t u w F t f t + i g t 0 < y 2 + y 2

Proof

Step Hyp Ref Expression
1 ftc1anc.g G = x A B A x F t dt
2 ftc1anc.a φ A
3 ftc1anc.b φ B
4 ftc1anc.le φ A B
5 ftc1anc.s φ A B D
6 ftc1anc.d φ D
7 ftc1anc.i φ F 𝐿 1
8 ftc1anc.f φ F : D
9 i1ff f dom 1 f :
10 9 ffvelrnda f dom 1 x f x
11 10 recnd f dom 1 x f x
12 ax-icn i
13 i1ff g dom 1 g :
14 13 ffvelrnda g dom 1 x g x
15 14 recnd g dom 1 x g x
16 mulcl i g x i g x
17 12 15 16 sylancr g dom 1 x i g x
18 addcl f x i g x f x + i g x
19 11 17 18 syl2an f dom 1 x g dom 1 x f x + i g x
20 19 anandirs f dom 1 g dom 1 x f x + i g x
21 reex V
22 21 a1i f dom 1 g dom 1 V
23 10 adantlr f dom 1 g dom 1 x f x
24 ovexd f dom 1 g dom 1 x i g x V
25 9 feqmptd f dom 1 f = x f x
26 25 adantr f dom 1 g dom 1 f = x f x
27 21 a1i g dom 1 V
28 12 a1i g dom 1 x i
29 fconstmpt × i = x i
30 29 a1i g dom 1 × i = x i
31 13 feqmptd g dom 1 g = x g x
32 27 28 14 30 31 offval2 g dom 1 × i × f g = x i g x
33 32 adantl f dom 1 g dom 1 × i × f g = x i g x
34 22 23 24 26 33 offval2 f dom 1 g dom 1 f + f × i × f g = x f x + i g x
35 absf abs :
36 35 a1i f dom 1 g dom 1 abs :
37 36 feqmptd f dom 1 g dom 1 abs = t t
38 fveq2 t = f x + i g x t = f x + i g x
39 20 34 37 38 fmptco f dom 1 g dom 1 abs f + f × i × f g = x f x + i g x
40 ftc1anclem3 f dom 1 g dom 1 abs f + f × i × f g dom 1
41 39 40 eqeltrrd f dom 1 g dom 1 x f x + i g x dom 1
42 ioombl u w dom vol
43 fveq2 x = t f x = f t
44 fveq2 x = t g x = g t
45 44 oveq2d x = t i g x = i g t
46 43 45 oveq12d x = t f x + i g x = f t + i g t
47 46 fveq2d x = t f x + i g x = f t + i g t
48 eqid x f x + i g x = x f x + i g x
49 fvex f t + i g t V
50 47 48 49 fvmpt t x f x + i g x t = f t + i g t
51 50 eqcomd t f t + i g t = x f x + i g x t
52 51 ifeq1d t if t u w f t + i g t 0 = if t u w x f x + i g x t 0
53 52 mpteq2ia t if t u w f t + i g t 0 = t if t u w x f x + i g x t 0
54 53 i1fres x f x + i g x dom 1 u w dom vol t if t u w f t + i g t 0 dom 1
55 41 42 54 sylancl f dom 1 g dom 1 t if t u w f t + i g t 0 dom 1
56 breq2 f t + i g t = if t u w f t + i g t 0 0 f t + i g t 0 if t u w f t + i g t 0
57 breq2 0 = if t u w f t + i g t 0 0 0 0 if t u w f t + i g t 0
58 elioore t u w t
59 eleq1w x = t x t
60 59 anbi2d x = t f dom 1 g dom 1 x f dom 1 g dom 1 t
61 46 eleq1d x = t f x + i g x f t + i g t
62 60 61 imbi12d x = t f dom 1 g dom 1 x f x + i g x f dom 1 g dom 1 t f t + i g t
63 62 20 chvarvv f dom 1 g dom 1 t f t + i g t
64 63 absge0d f dom 1 g dom 1 t 0 f t + i g t
65 58 64 sylan2 f dom 1 g dom 1 t u w 0 f t + i g t
66 0le0 0 0
67 66 a1i f dom 1 g dom 1 ¬ t u w 0 0
68 56 57 65 67 ifbothda f dom 1 g dom 1 0 if t u w f t + i g t 0
69 68 ralrimivw f dom 1 g dom 1 t 0 if t u w f t + i g t 0
70 ax-resscn
71 70 a1i f dom 1 g dom 1
72 c0ex 0 V
73 49 72 ifex if t u w f t + i g t 0 V
74 eqid t if t u w f t + i g t 0 = t if t u w f t + i g t 0
75 73 74 fnmpti t if t u w f t + i g t 0 Fn
76 75 a1i f dom 1 g dom 1 t if t u w f t + i g t 0 Fn
77 71 76 0pledm f dom 1 g dom 1 0 𝑝 f t if t u w f t + i g t 0 × 0 f t if t u w f t + i g t 0
78 72 a1i f dom 1 g dom 1 t 0 V
79 73 a1i f dom 1 g dom 1 t if t u w f t + i g t 0 V
80 fconstmpt × 0 = t 0
81 80 a1i f dom 1 g dom 1 × 0 = t 0
82 eqidd f dom 1 g dom 1 t if t u w f t + i g t 0 = t if t u w f t + i g t 0
83 22 78 79 81 82 ofrfval2 f dom 1 g dom 1 × 0 f t if t u w f t + i g t 0 t 0 if t u w f t + i g t 0
84 77 83 bitrd f dom 1 g dom 1 0 𝑝 f t if t u w f t + i g t 0 t 0 if t u w f t + i g t 0
85 69 84 mpbird f dom 1 g dom 1 0 𝑝 f t if t u w f t + i g t 0
86 itg2itg1 t if t u w f t + i g t 0 dom 1 0 𝑝 f t if t u w f t + i g t 0 2 t if t u w f t + i g t 0 = 1 t if t u w f t + i g t 0
87 itg1cl t if t u w f t + i g t 0 dom 1 1 t if t u w f t + i g t 0
88 87 adantr t if t u w f t + i g t 0 dom 1 0 𝑝 f t if t u w f t + i g t 0 1 t if t u w f t + i g t 0
89 86 88 eqeltrd t if t u w f t + i g t 0 dom 1 0 𝑝 f t if t u w f t + i g t 0 2 t if t u w f t + i g t 0
90 55 85 89 syl2anc f dom 1 g dom 1 2 t if t u w f t + i g t 0
91 90 ad6antlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0
92 simplll φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + φ f dom 1 g dom 1
93 2 rexrd φ A *
94 3 rexrd φ B *
95 93 94 jca φ A * B *
96 df-icc . = x * , y * t * | x t t y
97 96 elixx3g u A B A * B * u * A u u B
98 97 simprbi u A B A u u B
99 98 simpld u A B A u
100 96 elixx3g w A B A * B * w * A w w B
101 100 simprbi w A B A w w B
102 101 simprd w A B w B
103 99 102 anim12i u A B w A B A u w B
104 ioossioo A * B * A u w B u w A B
105 95 103 104 syl2an φ u A B w A B u w A B
106 5 adantr φ u A B w A B A B D
107 105 106 sstrd φ u A B w A B u w D
108 107 3adantr3 φ u A B w A B u w u w D
109 108 sselda φ u A B w A B u w t u w t D
110 8 ffvelrnda φ t D F t
111 110 adantlr φ u A B w A B u w t D F t
112 109 111 syldan φ u A B w A B u w t u w F t
113 112 adantllr φ f dom 1 g dom 1 u A B w A B u w t u w F t
114 63 adantll φ f dom 1 g dom 1 t f t + i g t
115 58 114 sylan2 φ f dom 1 g dom 1 t u w f t + i g t
116 115 adantlr φ f dom 1 g dom 1 u A B w A B u w t u w f t + i g t
117 113 116 subcld φ f dom 1 g dom 1 u A B w A B u w t u w F t f t + i g t
118 117 abscld φ f dom 1 g dom 1 u A B w A B u w t u w F t f t + i g t
119 118 rexrd φ f dom 1 g dom 1 u A B w A B u w t u w F t f t + i g t *
120 117 absge0d φ f dom 1 g dom 1 u A B w A B u w t u w 0 F t f t + i g t
121 elxrge0 F t f t + i g t 0 +∞ F t f t + i g t * 0 F t f t + i g t
122 119 120 121 sylanbrc φ f dom 1 g dom 1 u A B w A B u w t u w F t f t + i g t 0 +∞
123 0e0iccpnf 0 0 +∞
124 123 a1i φ f dom 1 g dom 1 u A B w A B u w ¬ t u w 0 0 +∞
125 122 124 ifclda φ f dom 1 g dom 1 u A B w A B u w if t u w F t f t + i g t 0 0 +∞
126 125 adantr φ f dom 1 g dom 1 u A B w A B u w t if t u w F t f t + i g t 0 0 +∞
127 126 fmpttd φ f dom 1 g dom 1 u A B w A B u w t if t u w F t f t + i g t 0 : 0 +∞
128 92 127 sylan φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w t if t u w F t f t + i g t 0 : 0 +∞
129 rpre y + y
130 129 rehalfcld y + y 2
131 130 ad2antlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w y 2
132 simpll φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + φ f dom 1 g dom 1
133 107 sselda φ u A B w A B t u w t D
134 133 adantllr φ f dom 1 g dom 1 u A B w A B t u w t D
135 110 adantlr φ f dom 1 g dom 1 t D F t
136 6 sselda φ t D t
137 136 adantlr φ f dom 1 g dom 1 t D t
138 137 114 syldan φ f dom 1 g dom 1 t D f t + i g t
139 135 138 subcld φ f dom 1 g dom 1 t D F t f t + i g t
140 139 abscld φ f dom 1 g dom 1 t D F t f t + i g t
141 140 rexrd φ f dom 1 g dom 1 t D F t f t + i g t *
142 141 adantlr φ f dom 1 g dom 1 u A B w A B t D F t f t + i g t *
143 134 142 syldan φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t *
144 139 absge0d φ f dom 1 g dom 1 t D 0 F t f t + i g t
145 144 adantlr φ f dom 1 g dom 1 u A B w A B t D 0 F t f t + i g t
146 134 145 syldan φ f dom 1 g dom 1 u A B w A B t u w 0 F t f t + i g t
147 143 146 121 sylanbrc φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t 0 +∞
148 123 a1i φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 0 +∞
149 147 148 ifclda φ f dom 1 g dom 1 u A B w A B if t u w F t f t + i g t 0 0 +∞
150 149 adantr φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 0 +∞
151 150 fmpttd φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 : 0 +∞
152 itg2cl t if t u w F t f t + i g t 0 : 0 +∞ 2 t if t u w F t f t + i g t 0 *
153 151 152 syl φ f dom 1 g dom 1 u A B w A B 2 t if t u w F t f t + i g t 0 *
154 132 153 sylan φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t u w F t f t + i g t 0 *
155 rphalfcl y + y 2 +
156 155 rpxrd y + y 2 *
157 156 ad2antlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B y 2 *
158 0cnd φ ¬ t D 0
159 110 158 ifclda φ if t D F t 0
160 subcl if t D F t 0 f t + i g t if t D F t 0 f t + i g t
161 159 63 160 syl2an φ f dom 1 g dom 1 t if t D F t 0 f t + i g t
162 161 anassrs φ f dom 1 g dom 1 t if t D F t 0 f t + i g t
163 162 abscld φ f dom 1 g dom 1 t if t D F t 0 f t + i g t
164 163 rexrd φ f dom 1 g dom 1 t if t D F t 0 f t + i g t *
165 162 absge0d φ f dom 1 g dom 1 t 0 if t D F t 0 f t + i g t
166 elxrge0 if t D F t 0 f t + i g t 0 +∞ if t D F t 0 f t + i g t * 0 if t D F t 0 f t + i g t
167 164 165 166 sylanbrc φ f dom 1 g dom 1 t if t D F t 0 f t + i g t 0 +∞
168 167 fmpttd φ f dom 1 g dom 1 t if t D F t 0 f t + i g t : 0 +∞
169 itg2cl t if t D F t 0 f t + i g t : 0 +∞ 2 t if t D F t 0 f t + i g t *
170 168 169 syl φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t *
171 170 ad3antrrr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t D F t 0 f t + i g t *
172 168 adantr φ f dom 1 g dom 1 u A B w A B t if t D F t 0 f t + i g t : 0 +∞
173 breq1 F t f t + i g t = if t u w F t f t + i g t 0 F t f t + i g t if t D F t 0 f t + i g t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
174 breq1 0 = if t u w F t f t + i g t 0 0 if t D F t 0 f t + i g t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
175 140 leidd φ f dom 1 g dom 1 t D F t f t + i g t F t f t + i g t
176 iftrue t D if t D F t 0 = F t
177 176 fvoveq1d t D if t D F t 0 f t + i g t = F t f t + i g t
178 177 adantl φ f dom 1 g dom 1 t D if t D F t 0 f t + i g t = F t f t + i g t
179 175 178 breqtrrd φ f dom 1 g dom 1 t D F t f t + i g t if t D F t 0 f t + i g t
180 179 adantlr φ f dom 1 g dom 1 u A B w A B t D F t f t + i g t if t D F t 0 f t + i g t
181 134 180 syldan φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t if t D F t 0 f t + i g t
182 181 adantlr φ f dom 1 g dom 1 u A B w A B t t u w F t f t + i g t if t D F t 0 f t + i g t
183 165 adantlr φ f dom 1 g dom 1 u A B w A B t 0 if t D F t 0 f t + i g t
184 183 adantr φ f dom 1 g dom 1 u A B w A B t ¬ t u w 0 if t D F t 0 f t + i g t
185 173 174 182 184 ifbothda φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
186 185 ralrimiva φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
187 21 a1i φ V
188 fvex F t f t + i g t V
189 188 72 ifex if t u w F t f t + i g t 0 V
190 189 a1i φ t if t u w F t f t + i g t 0 V
191 fvexd φ t if t D F t 0 f t + i g t V
192 eqidd φ t if t u w F t f t + i g t 0 = t if t u w F t f t + i g t 0
193 eqidd φ t if t D F t 0 f t + i g t = t if t D F t 0 f t + i g t
194 187 190 191 192 193 ofrfval2 φ t if t u w F t f t + i g t 0 f t if t D F t 0 f t + i g t t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
195 194 ad2antrr φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 f t if t D F t 0 f t + i g t t if t u w F t f t + i g t 0 if t D F t 0 f t + i g t
196 186 195 mpbird φ f dom 1 g dom 1 u A B w A B t if t u w F t f t + i g t 0 f t if t D F t 0 f t + i g t
197 itg2le t if t u w F t f t + i g t 0 : 0 +∞ t if t D F t 0 f t + i g t : 0 +∞ t if t u w F t f t + i g t 0 f t if t D F t 0 f t + i g t 2 t if t u w F t f t + i g t 0 2 t if t D F t 0 f t + i g t
198 151 172 196 197 syl3anc φ f dom 1 g dom 1 u A B w A B 2 t if t u w F t f t + i g t 0 2 t if t D F t 0 f t + i g t
199 132 198 sylan φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t u w F t f t + i g t 0 2 t if t D F t 0 f t + i g t
200 simpllr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t D F t 0 f t + i g t < y 2
201 154 171 157 199 200 xrlelttrd φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t u w F t f t + i g t 0 < y 2
202 154 157 201 xrltled φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 y + u A B w A B 2 t if t u w F t f t + i g t 0 y 2
203 202 adantllr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B 2 t if t u w F t f t + i g t 0 y 2
204 203 3adantr3 φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w 2 t if t u w F t f t + i g t 0 y 2
205 itg2lecl t if t u w F t f t + i g t 0 : 0 +∞ y 2 2 t if t u w F t f t + i g t 0 y 2 2 t if t u w F t f t + i g t 0
206 128 131 204 205 syl3anc φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w 2 t if t u w F t f t + i g t 0
207 206 adantr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w F t f t + i g t 0
208 130 ad3antlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < y 2
209 90 adantr f dom 1 g dom 1 r ran f ran g r 0 2 t if t u w f t + i g t 0
210 2rp 2 +
211 imassrn abs ran f ran g ran abs
212 frn abs : ran abs
213 35 212 ax-mp ran abs
214 211 213 sstri abs ran f ran g
215 214 a1i f dom 1 g dom 1 abs ran f ran g
216 9 frnd f dom 1 ran f
217 216 adantr f dom 1 g dom 1 ran f
218 13 frnd g dom 1 ran g
219 218 adantl f dom 1 g dom 1 ran g
220 217 219 unssd f dom 1 g dom 1 ran f ran g
221 220 70 sstrdi f dom 1 g dom 1 ran f ran g
222 i1f0rn f dom 1 0 ran f
223 elun1 0 ran f 0 ran f ran g
224 222 223 syl f dom 1 0 ran f ran g
225 224 adantr f dom 1 g dom 1 0 ran f ran g
226 ffn abs : abs Fn
227 35 226 ax-mp abs Fn
228 fnfvima abs Fn ran f ran g 0 ran f ran g 0 abs ran f ran g
229 227 228 mp3an1 ran f ran g 0 ran f ran g 0 abs ran f ran g
230 221 225 229 syl2anc f dom 1 g dom 1 0 abs ran f ran g
231 230 ne0d f dom 1 g dom 1 abs ran f ran g
232 ffun abs : Fun abs
233 35 232 ax-mp Fun abs
234 i1frn f dom 1 ran f Fin
235 i1frn g dom 1 ran g Fin
236 unfi ran f Fin ran g Fin ran f ran g Fin
237 234 235 236 syl2an f dom 1 g dom 1 ran f ran g Fin
238 imafi Fun abs ran f ran g Fin abs ran f ran g Fin
239 233 237 238 sylancr f dom 1 g dom 1 abs ran f ran g Fin
240 fimaxre2 abs ran f ran g abs ran f ran g Fin x y abs ran f ran g y x
241 214 239 240 sylancr f dom 1 g dom 1 x y abs ran f ran g y x
242 suprcl abs ran f ran g abs ran f ran g x y abs ran f ran g y x sup abs ran f ran g <
243 215 231 241 242 syl3anc f dom 1 g dom 1 sup abs ran f ran g <
244 243 adantr f dom 1 g dom 1 r ran f ran g r 0 sup abs ran f ran g <
245 0red f dom 1 g dom 1 r ran f ran g r 0 0
246 221 sselda f dom 1 g dom 1 r ran f ran g r
247 246 abscld f dom 1 g dom 1 r ran f ran g r
248 247 adantrr f dom 1 g dom 1 r ran f ran g r 0 r
249 absgt0 r r 0 0 < r
250 246 249 syl f dom 1 g dom 1 r ran f ran g r 0 0 < r
251 250 biimpa f dom 1 g dom 1 r ran f ran g r 0 0 < r
252 251 anasss f dom 1 g dom 1 r ran f ran g r 0 0 < r
253 215 231 241 3jca f dom 1 g dom 1 abs ran f ran g abs ran f ran g x y abs ran f ran g y x
254 253 adantr f dom 1 g dom 1 r ran f ran g abs ran f ran g abs ran f ran g x y abs ran f ran g y x
255 fnfvima abs Fn ran f ran g r ran f ran g r abs ran f ran g
256 227 255 mp3an1 ran f ran g r ran f ran g r abs ran f ran g
257 221 256 sylan f dom 1 g dom 1 r ran f ran g r abs ran f ran g
258 suprub abs ran f ran g abs ran f ran g x y abs ran f ran g y x r abs ran f ran g r sup abs ran f ran g <
259 254 257 258 syl2anc f dom 1 g dom 1 r ran f ran g r sup abs ran f ran g <
260 259 adantrr f dom 1 g dom 1 r ran f ran g r 0 r sup abs ran f ran g <
261 245 248 244 252 260 ltletrd f dom 1 g dom 1 r ran f ran g r 0 0 < sup abs ran f ran g <
262 244 261 elrpd f dom 1 g dom 1 r ran f ran g r 0 sup abs ran f ran g < +
263 262 rexlimdvaa f dom 1 g dom 1 r ran f ran g r 0 sup abs ran f ran g < +
264 263 imp f dom 1 g dom 1 r ran f ran g r 0 sup abs ran f ran g < +
265 rpmulcl 2 + sup abs ran f ran g < + 2 sup abs ran f ran g < +
266 210 264 265 sylancr f dom 1 g dom 1 r ran f ran g r 0 2 sup abs ran f ran g < +
267 209 266 rerpdivcld f dom 1 g dom 1 r ran f ran g r 0 2 t if t u w f t + i g t 0 2 sup abs ran f ran g <
268 267 adantll φ f dom 1 g dom 1 r ran f ran g r 0 2 t if t u w f t + i g t 0 2 sup abs ran f ran g <
269 268 adantlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 2 t if t u w f t + i g t 0 2 sup abs ran f ran g <
270 269 ad3antrrr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 2 sup abs ran f ran g <
271 simp-4l φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + φ
272 iccssre A B A B
273 2 3 272 syl2anc φ A B
274 273 70 sstrdi φ A B
275 274 sselda φ w A B w
276 274 sselda φ u A B u
277 subcl w u w u
278 275 276 277 syl2anr φ u A B φ w A B w u
279 278 anandis φ u A B w A B w u
280 279 abscld φ u A B w A B w u
281 280 3adantr3 φ u A B w A B u w w u
282 271 281 sylan φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u
283 282 adantr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < w u
284 rpdivcl y 2 + 2 sup abs ran f ran g < + y 2 2 sup abs ran f ran g < +
285 155 266 284 syl2anr f dom 1 g dom 1 r ran f ran g r 0 y + y 2 2 sup abs ran f ran g < +
286 285 rpred f dom 1 g dom 1 r ran f ran g r 0 y + y 2 2 sup abs ran f ran g <
287 286 adantlll φ f dom 1 g dom 1 r ran f ran g r 0 y + y 2 2 sup abs ran f ran g <
288 287 adantllr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + y 2 2 sup abs ran f ran g <
289 288 ad2antrr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < y 2 2 sup abs ran f ran g <
290 273 sseld φ u A B u
291 273 sseld φ w A B w
292 idd φ u w u w
293 290 291 292 3anim123d φ u A B w A B u w u w u w
294 293 ad2antrr φ f dom 1 g dom 1 r ran f ran g r 0 u A B w A B u w u w u w
295 294 imp φ f dom 1 g dom 1 r ran f ran g r 0 u A B w A B u w u w u w
296 63 abscld f dom 1 g dom 1 t f t + i g t
297 296 rexrd f dom 1 g dom 1 t f t + i g t *
298 elxrge0 f t + i g t 0 +∞ f t + i g t * 0 f t + i g t
299 297 64 298 sylanbrc f dom 1 g dom 1 t f t + i g t 0 +∞
300 ifcl f t + i g t 0 +∞ 0 0 +∞ if t u w f t + i g t 0 0 +∞
301 299 123 300 sylancl f dom 1 g dom 1 t if t u w f t + i g t 0 0 +∞
302 301 fmpttd f dom 1 g dom 1 t if t u w f t + i g t 0 : 0 +∞
303 243 recnd f dom 1 g dom 1 sup abs ran f ran g <
304 303 2timesd f dom 1 g dom 1 2 sup abs ran f ran g < = sup abs ran f ran g < + sup abs ran f ran g <
305 243 243 readdcld f dom 1 g dom 1 sup abs ran f ran g < + sup abs ran f ran g <
306 305 rexrd f dom 1 g dom 1 sup abs ran f ran g < + sup abs ran f ran g < *
307 abs0 0 = 0
308 307 230 eqeltrrid f dom 1 g dom 1 0 abs ran f ran g
309 suprub abs ran f ran g abs ran f ran g x y abs ran f ran g y x 0 abs ran f ran g 0 sup abs ran f ran g <
310 253 308 309 syl2anc f dom 1 g dom 1 0 sup abs ran f ran g <
311 243 243 310 310 addge0d f dom 1 g dom 1 0 sup abs ran f ran g < + sup abs ran f ran g <
312 elxrge0 sup abs ran f ran g < + sup abs ran f ran g < 0 +∞ sup abs ran f ran g < + sup abs ran f ran g < * 0 sup abs ran f ran g < + sup abs ran f ran g <
313 306 311 312 sylanbrc f dom 1 g dom 1 sup abs ran f ran g < + sup abs ran f ran g < 0 +∞
314 304 313 eqeltrd f dom 1 g dom 1 2 sup abs ran f ran g < 0 +∞
315 ifcl 2 sup abs ran f ran g < 0 +∞ 0 0 +∞ if t u w 2 sup abs ran f ran g < 0 0 +∞
316 314 123 315 sylancl f dom 1 g dom 1 if t u w 2 sup abs ran f ran g < 0 0 +∞
317 316 adantr f dom 1 g dom 1 t if t u w 2 sup abs ran f ran g < 0 0 +∞
318 317 fmpttd f dom 1 g dom 1 t if t u w 2 sup abs ran f ran g < 0 : 0 +∞
319 9 ffvelrnda f dom 1 t f t
320 319 recnd f dom 1 t f t
321 320 abscld f dom 1 t f t
322 13 ffvelrnda g dom 1 t g t
323 322 recnd g dom 1 t g t
324 323 abscld g dom 1 t g t
325 readdcl f t g t f t + g t
326 321 324 325 syl2an f dom 1 t g dom 1 t f t + g t
327 326 anandirs f dom 1 g dom 1 t f t + g t
328 305 adantr f dom 1 g dom 1 t sup abs ran f ran g < + sup abs ran f ran g <
329 mulcl i g t i g t
330 12 323 329 sylancr g dom 1 t i g t
331 abstri f t i g t f t + i g t f t + i g t
332 320 330 331 syl2an f dom 1 t g dom 1 t f t + i g t f t + i g t
333 332 anandirs f dom 1 g dom 1 t f t + i g t f t + i g t
334 absmul i g t i g t = i g t
335 12 323 334 sylancr g dom 1 t i g t = i g t
336 absi i = 1
337 336 oveq1i i g t = 1 g t
338 335 337 eqtrdi g dom 1 t i g t = 1 g t
339 324 recnd g dom 1 t g t
340 339 mulid2d g dom 1 t 1 g t = g t
341 338 340 eqtrd g dom 1 t i g t = g t
342 341 adantll f dom 1 g dom 1 t i g t = g t
343 342 oveq2d f dom 1 g dom 1 t f t + i g t = f t + g t
344 333 343 breqtrd f dom 1 g dom 1 t f t + i g t f t + g t
345 321 adantlr f dom 1 g dom 1 t f t
346 324 adantll f dom 1 g dom 1 t g t
347 243 adantr f dom 1 g dom 1 t sup abs ran f ran g <
348 253 adantr f dom 1 g dom 1 t abs ran f ran g abs ran f ran g x y abs ran f ran g y x
349 221 adantr f dom 1 g dom 1 t ran f ran g
350 9 ffnd f dom 1 f Fn
351 fnfvelrn f Fn t f t ran f
352 350 351 sylan f dom 1 t f t ran f
353 elun1 f t ran f f t ran f ran g
354 352 353 syl f dom 1 t f t ran f ran g
355 354 adantlr f dom 1 g dom 1 t f t ran f ran g
356 fnfvima abs Fn ran f ran g f t ran f ran g f t abs ran f ran g
357 227 356 mp3an1 ran f ran g f t ran f ran g f t abs ran f ran g
358 349 355 357 syl2anc f dom 1 g dom 1 t f t abs ran f ran g
359 suprub abs ran f ran g abs ran f ran g x y abs ran f ran g y x f t abs ran f ran g f t sup abs ran f ran g <
360 348 358 359 syl2anc f dom 1 g dom 1 t f t sup abs ran f ran g <
361 13 ffnd g dom 1 g Fn
362 fnfvelrn g Fn t g t ran g
363 361 362 sylan g dom 1 t g t ran g
364 elun2 g t ran g g t ran f ran g
365 363 364 syl g dom 1 t g t ran f ran g
366 365 adantll f dom 1 g dom 1 t g t ran f ran g
367 fnfvima abs Fn ran f ran g g t ran f ran g g t abs ran f ran g
368 227 367 mp3an1 ran f ran g g t ran f ran g g t abs ran f ran g
369 349 366 368 syl2anc f dom 1 g dom 1 t g t abs ran f ran g
370 suprub abs ran f ran g abs ran f ran g x y abs ran f ran g y x g t abs ran f ran g g t sup abs ran f ran g <
371 348 369 370 syl2anc f dom 1 g dom 1 t g t sup abs ran f ran g <
372 345 346 347 347 360 371 le2addd f dom 1 g dom 1 t f t + g t sup abs ran f ran g < + sup abs ran f ran g <
373 296 327 328 344 372 letrd f dom 1 g dom 1 t f t + i g t sup abs ran f ran g < + sup abs ran f ran g <
374 304 adantr f dom 1 g dom 1 t 2 sup abs ran f ran g < = sup abs ran f ran g < + sup abs ran f ran g <
375 373 374 breqtrrd f dom 1 g dom 1 t f t + i g t 2 sup abs ran f ran g <
376 58 375 sylan2 f dom 1 g dom 1 t u w f t + i g t 2 sup abs ran f ran g <
377 iftrue t u w if t u w f t + i g t 0 = f t + i g t
378 377 adantl f dom 1 g dom 1 t u w if t u w f t + i g t 0 = f t + i g t
379 iftrue t u w if t u w 2 sup abs ran f ran g < 0 = 2 sup abs ran f ran g <
380 379 adantl f dom 1 g dom 1 t u w if t u w 2 sup abs ran f ran g < 0 = 2 sup abs ran f ran g <
381 376 378 380 3brtr4d f dom 1 g dom 1 t u w if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
382 381 ex f dom 1 g dom 1 t u w if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
383 66 a1i ¬ t u w 0 0
384 iffalse ¬ t u w if t u w f t + i g t 0 = 0
385 iffalse ¬ t u w if t u w 2 sup abs ran f ran g < 0 = 0
386 383 384 385 3brtr4d ¬ t u w if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
387 382 386 pm2.61d1 f dom 1 g dom 1 if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
388 387 ralrimivw f dom 1 g dom 1 t if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
389 ovex 2 sup abs ran f ran g < V
390 389 72 ifex if t u w 2 sup abs ran f ran g < 0 V
391 390 a1i f dom 1 g dom 1 t if t u w 2 sup abs ran f ran g < 0 V
392 eqidd f dom 1 g dom 1 t if t u w 2 sup abs ran f ran g < 0 = t if t u w 2 sup abs ran f ran g < 0
393 22 79 391 82 392 ofrfval2 f dom 1 g dom 1 t if t u w f t + i g t 0 f t if t u w 2 sup abs ran f ran g < 0 t if t u w f t + i g t 0 if t u w 2 sup abs ran f ran g < 0
394 388 393 mpbird f dom 1 g dom 1 t if t u w f t + i g t 0 f t if t u w 2 sup abs ran f ran g < 0
395 itg2le t if t u w f t + i g t 0 : 0 +∞ t if t u w 2 sup abs ran f ran g < 0 : 0 +∞ t if t u w f t + i g t 0 f t if t u w 2 sup abs ran f ran g < 0 2 t if t u w f t + i g t 0 2 t if t u w 2 sup abs ran f ran g < 0
396 302 318 394 395 syl3anc f dom 1 g dom 1 2 t if t u w f t + i g t 0 2 t if t u w 2 sup abs ran f ran g < 0
397 396 adantr f dom 1 g dom 1 u w u w 2 t if t u w f t + i g t 0 2 t if t u w 2 sup abs ran f ran g < 0
398 mblvol u w dom vol vol u w = vol * u w
399 42 398 ax-mp vol u w = vol * u w
400 ovolioo u w u w vol * u w = w u
401 399 400 syl5eq u w u w vol u w = w u
402 resubcl w u w u
403 402 ancoms u w w u
404 403 3adant3 u w u w w u
405 401 404 eqeltrd u w u w vol u w
406 elrege0 sup abs ran f ran g < 0 +∞ sup abs ran f ran g < 0 sup abs ran f ran g <
407 243 310 406 sylanbrc f dom 1 g dom 1 sup abs ran f ran g < 0 +∞
408 ge0addcl sup abs ran f ran g < 0 +∞ sup abs ran f ran g < 0 +∞ sup abs ran f ran g < + sup abs ran f ran g < 0 +∞
409 407 407 408 syl2anc f dom 1 g dom 1 sup abs ran f ran g < + sup abs ran f ran g < 0 +∞
410 304 409 eqeltrd f dom 1 g dom 1 2 sup abs ran f ran g < 0 +∞
411 itg2const u w dom vol vol u w 2 sup abs ran f ran g < 0 +∞ 2 t if t u w 2 sup abs ran f ran g < 0 = 2 sup abs ran f ran g < vol u w
412 42 411 mp3an1 vol u w 2 sup abs ran f ran g < 0 +∞ 2 t if t u w 2 sup abs ran f ran g < 0 = 2 sup abs ran f ran g < vol u w
413 405 410 412 syl2anr f dom 1 g dom 1 u w u w 2 t if t u w 2 sup abs ran f ran g < 0 = 2 sup abs ran f ran g < vol u w
414 397 413 breqtrd f dom 1 g dom 1 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w
415 414 adantll φ f dom 1 g dom 1 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w
416 415 adantlr φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w
417 90 ad3antlr φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 t if t u w f t + i g t 0
418 405 adantl φ f dom 1 g dom 1 r ran f ran g r 0 u w u w vol u w
419 266 adantll φ f dom 1 g dom 1 r ran f ran g r 0 2 sup abs ran f ran g < +
420 419 adantr φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 sup abs ran f ran g < +
421 417 418 420 ledivmuld φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w
422 416 421 mpbird φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < vol u w
423 abssubge0 u w u w w u = w u
424 400 423 eqtr4d u w u w vol * u w = w u
425 399 424 syl5eq u w u w vol u w = w u
426 425 adantl φ f dom 1 g dom 1 r ran f ran g r 0 u w u w vol u w = w u
427 422 426 breqtrd φ f dom 1 g dom 1 r ran f ran g r 0 u w u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < w u
428 295 427 syldan φ f dom 1 g dom 1 r ran f ran g r 0 u A B w A B u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < w u
429 428 adantllr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 u A B w A B u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < w u
430 429 adantlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < w u
431 430 adantr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < w u
432 simpr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < w u < y 2 2 sup abs ran f ran g <
433 270 283 289 431 432 lelttrd φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < < y 2 2 sup abs ran f ran g <
434 90 adantl φ f dom 1 g dom 1 2 t if t u w f t + i g t 0
435 434 ad3antrrr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + 2 t if t u w f t + i g t 0
436 130 adantl φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + y 2
437 419 adantlr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 2 sup abs ran f ran g < +
438 437 adantr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + 2 sup abs ran f ran g < +
439 435 436 438 ltdiv1d φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + 2 t if t u w f t + i g t 0 < y 2 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < < y 2 2 sup abs ran f ran g <
440 439 ad2antrr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 < y 2 2 t if t u w f t + i g t 0 2 sup abs ran f ran g < < y 2 2 sup abs ran f ran g <
441 433 440 mpbird φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 < y 2
442 201 adantllr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B 2 t if t u w F t f t + i g t 0 < y 2
443 442 3adantr3 φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w 2 t if t u w F t f t + i g t 0 < y 2
444 443 adantr φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w F t f t + i g t 0 < y 2
445 91 207 208 208 441 444 lt2addd φ f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < y 2 r ran f ran g r 0 y + u A B w A B u w w u < y 2 2 sup abs ran f ran g < 2 t if t u w f t + i g t 0 + 2 t if t u w F t f t + i g t 0 < y 2 + y 2