Metamath Proof Explorer


Theorem ftc1anclem8

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 29-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 ftc1anclem8 φ 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 + f t + i g t 0 < y

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 1 2 3 4 5 6 7 8 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
10 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
11 3simpa u A B w A B u w u A B w A B
12 ioossre u w
13 12 a1i φ f dom 1 g dom 1 u w
14 rembl dom vol
15 14 a1i φ f dom 1 g dom 1 dom vol
16 fvex f t + i g t V
17 c0ex 0 V
18 16 17 ifex if t u w f t + i g t 0 V
19 18 a1i φ f dom 1 g dom 1 t u w if t u w f t + i g t 0 V
20 eldifn t u w ¬ t u w
21 20 adantl φ f dom 1 g dom 1 t u w ¬ t u w
22 21 iffalsed φ f dom 1 g dom 1 t u w if t u w f t + i g t 0 = 0
23 iftrue t u w if t u w f t + i g t 0 = f t + i g t
24 23 mpteq2ia t u w if t u w f t + i g t 0 = t u w f t + i g t
25 resmpt u w t f t + i g t u w = t u w f t + i g t
26 12 25 ax-mp t f t + i g t u w = t u w f t + i g t
27 24 26 eqtr4i t u w if t u w f t + i g t 0 = t f t + i g t u w
28 i1ff f dom 1 f :
29 28 ffvelrnda f dom 1 t f t
30 29 recnd f dom 1 t f t
31 ax-icn i
32 i1ff g dom 1 g :
33 32 ffvelrnda g dom 1 t g t
34 33 recnd g dom 1 t g t
35 mulcl i g t i g t
36 31 34 35 sylancr g dom 1 t i g t
37 addcl f t i g t f t + i g t
38 30 36 37 syl2an f dom 1 t g dom 1 t f t + i g t
39 38 anandirs f dom 1 g dom 1 t f t + i g t
40 reex V
41 40 a1i f dom 1 g dom 1 V
42 29 adantlr f dom 1 g dom 1 t f t
43 36 adantll f dom 1 g dom 1 t i g t
44 28 feqmptd f dom 1 f = t f t
45 44 adantr f dom 1 g dom 1 f = t f t
46 40 a1i g dom 1 V
47 31 a1i g dom 1 t i
48 fconstmpt × i = t i
49 48 a1i g dom 1 × i = t i
50 32 feqmptd g dom 1 g = t g t
51 46 47 33 49 50 offval2 g dom 1 × i × f g = t i g t
52 51 adantl f dom 1 g dom 1 × i × f g = t i g t
53 41 42 43 45 52 offval2 f dom 1 g dom 1 f + f × i × f g = t f t + i g t
54 absf abs :
55 54 a1i f dom 1 g dom 1 abs :
56 55 feqmptd f dom 1 g dom 1 abs = x x
57 fveq2 x = f t + i g t x = f t + i g t
58 39 53 56 57 fmptco f dom 1 g dom 1 abs f + f × i × f g = t f t + i g t
59 ftc1anclem3 f dom 1 g dom 1 abs f + f × i × f g dom 1
60 58 59 eqeltrrd f dom 1 g dom 1 t f t + i g t dom 1
61 i1fmbf t f t + i g t dom 1 t f t + i g t MblFn
62 60 61 syl f dom 1 g dom 1 t f t + i g t MblFn
63 ioombl u w dom vol
64 mbfres t f t + i g t MblFn u w dom vol t f t + i g t u w MblFn
65 62 63 64 sylancl f dom 1 g dom 1 t f t + i g t u w MblFn
66 27 65 eqeltrid f dom 1 g dom 1 t u w if t u w f t + i g t 0 MblFn
67 66 adantl φ f dom 1 g dom 1 t u w if t u w f t + i g t 0 MblFn
68 13 15 19 22 67 mbfss φ f dom 1 g dom 1 t if t u w f t + i g t 0 MblFn
69 68 adantr φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 MblFn
70 39 abscld f dom 1 g dom 1 t f t + i g t
71 39 absge0d f dom 1 g dom 1 t 0 f t + i g t
72 elrege0 f t + i g t 0 +∞ f t + i g t 0 f t + i g t
73 70 71 72 sylanbrc f dom 1 g dom 1 t f t + i g t 0 +∞
74 0e0icopnf 0 0 +∞
75 ifcl f t + i g t 0 +∞ 0 0 +∞ if t u w f t + i g t 0 0 +∞
76 73 74 75 sylancl f dom 1 g dom 1 t if t u w f t + i g t 0 0 +∞
77 76 fmpttd f dom 1 g dom 1 t if t u w f t + i g t 0 : 0 +∞
78 77 ad2antlr φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 : 0 +∞
79 70 rexrd f dom 1 g dom 1 t f t + i g t *
80 elxrge0 f t + i g t 0 +∞ f t + i g t * 0 f t + i g t
81 79 71 80 sylanbrc f dom 1 g dom 1 t f t + i g t 0 +∞
82 0e0iccpnf 0 0 +∞
83 ifcl f t + i g t 0 +∞ 0 0 +∞ if t u w f t + i g t 0 0 +∞
84 81 82 83 sylancl f dom 1 g dom 1 t if t u w f t + i g t 0 0 +∞
85 84 fmpttd f dom 1 g dom 1 t if t u w f t + i g t 0 : 0 +∞
86 85 ad2antlr φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 : 0 +∞
87 ifcl f t + i g t 0 +∞ 0 0 +∞ if t D f t + i g t 0 0 +∞
88 81 82 87 sylancl f dom 1 g dom 1 t if t D f t + i g t 0 0 +∞
89 88 fmpttd f dom 1 g dom 1 t if t D f t + i g t 0 : 0 +∞
90 ffn f : f Fn
91 frn f : ran f
92 ax-resscn
93 91 92 sstrdi f : ran f
94 ffn abs : abs Fn
95 54 94 ax-mp abs Fn
96 fnco abs Fn f Fn ran f abs f Fn
97 95 96 mp3an1 f Fn ran f abs f Fn
98 90 93 97 syl2anc f : abs f Fn
99 28 98 syl f dom 1 abs f Fn
100 99 adantr f dom 1 g dom 1 abs f Fn
101 ffn g : g Fn
102 frn g : ran g
103 102 92 sstrdi g : ran g
104 fnco abs Fn g Fn ran g abs g Fn
105 95 104 mp3an1 g Fn ran g abs g Fn
106 101 103 105 syl2anc g : abs g Fn
107 32 106 syl g dom 1 abs g Fn
108 107 adantl f dom 1 g dom 1 abs g Fn
109 inidm =
110 28 adantr f dom 1 g dom 1 f :
111 fvco3 f : t abs f t = f t
112 110 111 sylan f dom 1 g dom 1 t abs f t = f t
113 32 adantl f dom 1 g dom 1 g :
114 fvco3 g : t abs g t = g t
115 113 114 sylan f dom 1 g dom 1 t abs g t = g t
116 100 108 41 41 109 112 115 offval f dom 1 g dom 1 abs f + f abs g = t f t + g t
117 30 addid1d f dom 1 t f t + 0 = f t
118 117 mpteq2dva f dom 1 t f t + 0 = t f t
119 40 a1i f dom 1 V
120 17 a1i f dom 1 t 0 V
121 31 a1i f dom 1 t i
122 48 a1i f dom 1 × i = t i
123 fconstmpt × 0 = t 0
124 123 a1i f dom 1 × 0 = t 0
125 119 121 120 122 124 offval2 f dom 1 × i × f × 0 = t i 0
126 it0e0 i 0 = 0
127 126 mpteq2i t i 0 = t 0
128 125 127 eqtrdi f dom 1 × i × f × 0 = t 0
129 119 29 120 44 128 offval2 f dom 1 f + f × i × f × 0 = t f t + 0
130 118 129 44 3eqtr4d f dom 1 f + f × i × f × 0 = f
131 130 coeq2d f dom 1 abs f + f × i × f × 0 = abs f
132 i1f0 × 0 dom 1
133 ftc1anclem3 f dom 1 × 0 dom 1 abs f + f × i × f × 0 dom 1
134 132 133 mpan2 f dom 1 abs f + f × i × f × 0 dom 1
135 131 134 eqeltrrd f dom 1 abs f dom 1
136 135 adantr f dom 1 g dom 1 abs f dom 1
137 coeq2 f = g abs f = abs g
138 137 eleq1d f = g abs f dom 1 abs g dom 1
139 138 135 vtoclga g dom 1 abs g dom 1
140 139 adantl f dom 1 g dom 1 abs g dom 1
141 136 140 i1fadd f dom 1 g dom 1 abs f + f abs g dom 1
142 116 141 eqeltrrd f dom 1 g dom 1 t f t + g t dom 1
143 30 abscld f dom 1 t f t
144 30 absge0d f dom 1 t 0 f t
145 elrege0 f t 0 +∞ f t 0 f t
146 143 144 145 sylanbrc f dom 1 t f t 0 +∞
147 34 abscld g dom 1 t g t
148 34 absge0d g dom 1 t 0 g t
149 elrege0 g t 0 +∞ g t 0 g t
150 147 148 149 sylanbrc g dom 1 t g t 0 +∞
151 ge0addcl f t 0 +∞ g t 0 +∞ f t + g t 0 +∞
152 146 150 151 syl2an f dom 1 t g dom 1 t f t + g t 0 +∞
153 152 anandirs f dom 1 g dom 1 t f t + g t 0 +∞
154 153 fmpttd f dom 1 g dom 1 t f t + g t : 0 +∞
155 0plef t f t + g t : 0 +∞ t f t + g t : 0 𝑝 f t f t + g t
156 154 155 sylib f dom 1 g dom 1 t f t + g t : 0 𝑝 f t f t + g t
157 156 simprd f dom 1 g dom 1 0 𝑝 f t f t + g t
158 itg2itg1 t f t + g t dom 1 0 𝑝 f t f t + g t 2 t f t + g t = 1 t f t + g t
159 itg1cl t f t + g t dom 1 1 t f t + g t
160 159 adantr t f t + g t dom 1 0 𝑝 f t f t + g t 1 t f t + g t
161 158 160 eqeltrd t f t + g t dom 1 0 𝑝 f t f t + g t 2 t f t + g t
162 142 157 161 syl2anc f dom 1 g dom 1 2 t f t + g t
163 icossicc 0 +∞ 0 +∞
164 fss t f t + g t : 0 +∞ 0 +∞ 0 +∞ t f t + g t : 0 +∞
165 154 163 164 sylancl f dom 1 g dom 1 t f t + g t : 0 +∞
166 0re 0
167 ifcl f t + i g t 0 if t D f t + i g t 0
168 70 166 167 sylancl f dom 1 g dom 1 t if t D f t + i g t 0
169 readdcl f t g t f t + g t
170 143 147 169 syl2an f dom 1 t g dom 1 t f t + g t
171 170 anandirs f dom 1 g dom 1 t f t + g t
172 70 leidd f dom 1 g dom 1 t f t + i g t f t + i g t
173 breq1 f t + i g t = if t D f t + i g t 0 f t + i g t f t + i g t if t D f t + i g t 0 f t + i g t
174 breq1 0 = if t D f t + i g t 0 0 f t + i g t if t D f t + i g t 0 f t + i g t
175 173 174 ifboth f t + i g t f t + i g t 0 f t + i g t if t D f t + i g t 0 f t + i g t
176 172 71 175 syl2anc f dom 1 g dom 1 t if t D f t + i g t 0 f t + i g t
177 abstri f t i g t f t + i g t f t + i g t
178 30 36 177 syl2an f dom 1 t g dom 1 t f t + i g t f t + i g t
179 178 anandirs f dom 1 g dom 1 t f t + i g t f t + i g t
180 absmul i g t i g t = i g t
181 31 34 180 sylancr g dom 1 t i g t = i g t
182 absi i = 1
183 182 oveq1i i g t = 1 g t
184 181 183 eqtrdi g dom 1 t i g t = 1 g t
185 147 recnd g dom 1 t g t
186 185 mulid2d g dom 1 t 1 g t = g t
187 184 186 eqtrd g dom 1 t i g t = g t
188 187 adantll f dom 1 g dom 1 t i g t = g t
189 188 oveq2d f dom 1 g dom 1 t f t + i g t = f t + g t
190 179 189 breqtrd f dom 1 g dom 1 t f t + i g t f t + g t
191 168 70 171 176 190 letrd f dom 1 g dom 1 t if t D f t + i g t 0 f t + g t
192 191 ralrimiva f dom 1 g dom 1 t if t D f t + i g t 0 f t + g t
193 eqidd f dom 1 g dom 1 t if t D f t + i g t 0 = t if t D f t + i g t 0
194 eqidd f dom 1 g dom 1 t f t + g t = t f t + g t
195 41 168 171 193 194 ofrfval2 f dom 1 g dom 1 t if t D f t + i g t 0 f t f t + g t t if t D f t + i g t 0 f t + g t
196 192 195 mpbird f dom 1 g dom 1 t if t D f t + i g t 0 f t f t + g t
197 itg2le t if t D f t + i g t 0 : 0 +∞ t f t + g t : 0 +∞ t if t D f t + i g t 0 f t f t + g t 2 t if t D f t + i g t 0 2 t f t + g t
198 89 165 196 197 syl3anc f dom 1 g dom 1 2 t if t D f t + i g t 0 2 t f t + g t
199 itg2lecl t if t D f t + i g t 0 : 0 +∞ 2 t f t + g t 2 t if t D f t + i g t 0 2 t f t + g t 2 t if t D f t + i g t 0
200 89 162 198 199 syl3anc f dom 1 g dom 1 2 t if t D f t + i g t 0
201 200 ad2antlr φ f dom 1 g dom 1 u A B w A B 2 t if t D f t + i g t 0
202 89 ad2antlr φ f dom 1 g dom 1 u A B w A B t if t D f t + i g t 0 : 0 +∞
203 breq1 f t + i g t = if t u w f t + i g t 0 f t + i g t if t D f t + i g t 0 if t u w f t + i g t 0 if t D f t + i g t 0
204 breq1 0 = if t u w f t + i g t 0 0 if t D f t + i g t 0 if t u w f t + i g t 0 if t D f t + i g t 0
205 elioore t u w t
206 205 172 sylan2 f dom 1 g dom 1 t u w f t + i g t f t + i g t
207 206 adantll φ f dom 1 g dom 1 t u w f t + i g t f t + i g t
208 207 adantlr φ f dom 1 g dom 1 u A B w A B t u w f t + i g t f t + i g t
209 2 rexrd φ A *
210 3 rexrd φ B *
211 209 210 jca φ A * B *
212 df-icc . = x * , y * t * | x t t y
213 212 elixx3g u A B A * B * u * A u u B
214 213 simprbi u A B A u u B
215 214 simpld u A B A u
216 212 elixx3g w A B A * B * w * A w w B
217 216 simprbi w A B A w w B
218 217 simprd w A B w B
219 215 218 anim12i u A B w A B A u w B
220 ioossioo A * B * A u w B u w A B
221 211 219 220 syl2an φ u A B w A B u w A B
222 5 adantr φ u A B w A B A B D
223 221 222 sstrd φ u A B w A B u w D
224 223 sselda φ u A B w A B t u w t D
225 iftrue t D if t D f t + i g t 0 = f t + i g t
226 224 225 syl φ u A B w A B t u w if t D f t + i g t 0 = f t + i g t
227 226 adantllr φ f dom 1 g dom 1 u A B w A B t u w if t D f t + i g t 0 = f t + i g t
228 208 227 breqtrrd φ f dom 1 g dom 1 u A B w A B t u w f t + i g t if t D f t + i g t 0
229 breq2 f t + i g t = if t D f t + i g t 0 0 f t + i g t 0 if t D f t + i g t 0
230 breq2 0 = if t D f t + i g t 0 0 0 0 if t D f t + i g t 0
231 6 sselda φ t D t
232 231 adantlr φ f dom 1 g dom 1 t D t
233 71 adantll φ f dom 1 g dom 1 t 0 f t + i g t
234 232 233 syldan φ f dom 1 g dom 1 t D 0 f t + i g t
235 0le0 0 0
236 235 a1i φ f dom 1 g dom 1 ¬ t D 0 0
237 229 230 234 236 ifbothda φ f dom 1 g dom 1 0 if t D f t + i g t 0
238 237 ad2antrr φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 if t D f t + i g t 0
239 203 204 228 238 ifbothda φ f dom 1 g dom 1 u A B w A B if t u w f t + i g t 0 if t D f t + i g t 0
240 239 ralrimivw φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 if t D f t + i g t 0
241 40 a1i φ V
242 18 a1i φ t if t u w f t + i g t 0 V
243 16 17 ifex if t D f t + i g t 0 V
244 243 a1i φ t if t D f t + i g t 0 V
245 eqidd φ t if t u w f t + i g t 0 = t if t u w f t + i g t 0
246 eqidd φ t if t D f t + i g t 0 = t if t D f t + i g t 0
247 241 242 244 245 246 ofrfval2 φ t if t u w f t + i g t 0 f t if t D f t + i g t 0 t if t u w f t + i g t 0 if t D f t + i g t 0
248 247 ad2antrr φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 f t if t D f t + i g t 0 t if t u w f t + i g t 0 if t D f t + i g t 0
249 240 248 mpbird φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 f t if t D f t + i g t 0
250 itg2le t if t u w f t + i g t 0 : 0 +∞ t if t D f t + i g t 0 : 0 +∞ t if t u w f t + i g t 0 f t if t D f t + i g t 0 2 t if t u w f t + i g t 0 2 t if t D f t + i g t 0
251 86 202 249 250 syl3anc φ f dom 1 g dom 1 u A B w A B 2 t if t u w f t + i g t 0 2 t if t D f t + i g t 0
252 itg2lecl t if t u w f t + i g t 0 : 0 +∞ 2 t if t D f t + i g t 0 2 t if t u w f t + i g t 0 2 t if t D f t + i g t 0 2 t if t u w f t + i g t 0
253 86 201 251 252 syl3anc φ f dom 1 g dom 1 u A B w A B 2 t if t u w f t + i g t 0
254 8 ffvelrnda φ t D F t
255 254 adantlr φ u A B w A B t D F t
256 224 255 syldan φ u A B w A B t u w F t
257 256 adantllr φ f dom 1 g dom 1 u A B w A B t u w F t
258 205 39 sylan2 f dom 1 g dom 1 t u w f t + i g t
259 258 adantll φ f dom 1 g dom 1 t u w f t + i g t
260 259 adantlr φ f dom 1 g dom 1 u A B w A B t u w f t + i g t
261 257 260 subcld φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t
262 261 abscld φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t
263 261 absge0d φ f dom 1 g dom 1 u A B w A B t u w 0 F t f t + i g t
264 elrege0 F t f t + i g t 0 +∞ F t f t + i g t 0 F t f t + i g t
265 262 263 264 sylanbrc φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t 0 +∞
266 74 a1i φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 0 +∞
267 265 266 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 +∞
268 267 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 +∞
269 268 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 +∞
270 262 rexrd φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t *
271 elxrge0 F t f t + i g t 0 +∞ F t f t + i g t * 0 F t f t + i g t
272 270 263 271 sylanbrc φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t 0 +∞
273 82 a1i φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 0 +∞
274 272 273 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 +∞
275 274 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 +∞
276 275 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 +∞
277 recncf : cn
278 prid1g : cn
279 277 278 ax-mp
280 ftc1anclem2 F : D F 𝐿 1 2 t if t D F t 0
281 279 280 mp3an3 F : D F 𝐿 1 2 t if t D F t 0
282 8 7 281 syl2anc φ 2 t if t D F t 0
283 imcncf : cn
284 prid2g : cn
285 283 284 ax-mp
286 ftc1anclem2 F : D F 𝐿 1 2 t if t D F t 0
287 285 286 mp3an3 F : D F 𝐿 1 2 t if t D F t 0
288 8 7 287 syl2anc φ 2 t if t D F t 0
289 282 288 readdcld φ 2 t if t D F t 0 + 2 t if t D F t 0
290 289 ad2antrr φ f dom 1 g dom 1 u A B w A B 2 t if t D F t 0 + 2 t if t D F t 0
291 201 290 readdcld φ f dom 1 g dom 1 u A B w A B 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0
292 ge0addcl x 0 +∞ y 0 +∞ x + y 0 +∞
293 292 adantl φ f dom 1 g dom 1 x 0 +∞ y 0 +∞ x + y 0 +∞
294 ifcl f t + i g t 0 +∞ 0 0 +∞ if t D f t + i g t 0 0 +∞
295 73 74 294 sylancl f dom 1 g dom 1 t if t D f t + i g t 0 0 +∞
296 295 fmpttd f dom 1 g dom 1 t if t D f t + i g t 0 : 0 +∞
297 296 adantl φ f dom 1 g dom 1 t if t D f t + i g t 0 : 0 +∞
298 292 adantl φ x 0 +∞ y 0 +∞ x + y 0 +∞
299 254 recld φ t D F t
300 299 recnd φ t D F t
301 300 abscld φ t D F t
302 300 absge0d φ t D 0 F t
303 elrege0 F t 0 +∞ F t 0 F t
304 301 302 303 sylanbrc φ t D F t 0 +∞
305 74 a1i φ ¬ t D 0 0 +∞
306 304 305 ifclda φ if t D F t 0 0 +∞
307 306 adantr φ t if t D F t 0 0 +∞
308 307 fmpttd φ t if t D F t 0 : 0 +∞
309 254 imcld φ t D F t
310 309 recnd φ t D F t
311 310 abscld φ t D F t
312 310 absge0d φ t D 0 F t
313 elrege0 F t 0 +∞ F t 0 F t
314 311 312 313 sylanbrc φ t D F t 0 +∞
315 314 305 ifclda φ if t D F t 0 0 +∞
316 315 adantr φ t if t D F t 0 0 +∞
317 316 fmpttd φ t if t D F t 0 : 0 +∞
318 298 308 317 241 241 109 off φ t if t D F t 0 + f t if t D F t 0 : 0 +∞
319 318 adantr φ f dom 1 g dom 1 t if t D F t 0 + f t if t D F t 0 : 0 +∞
320 40 a1i φ f dom 1 g dom 1 V
321 293 297 319 320 320 109 off φ f dom 1 g dom 1 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞
322 fss t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞ 0 +∞ 0 +∞ t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞
323 321 163 322 sylancl φ f dom 1 g dom 1 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞
324 323 adantr φ f dom 1 g dom 1 u A B w A B t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞
325 0xr 0 *
326 325 a1i φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 *
327 270 326 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 *
328 254 adantlr φ f dom 1 g dom 1 t D F t
329 39 adantll φ f dom 1 g dom 1 t f t + i g t
330 232 329 syldan φ f dom 1 g dom 1 t D f t + i g t
331 328 330 subcld φ f dom 1 g dom 1 t D F t f t + i g t
332 331 abscld φ f dom 1 g dom 1 t D F t f t + i g t
333 332 rexrd φ f dom 1 g dom 1 t D F t f t + i g t *
334 325 a1i φ f dom 1 g dom 1 ¬ t D 0 *
335 333 334 ifclda φ f dom 1 g dom 1 if t D F t f t + i g t 0 *
336 335 adantr φ f dom 1 g dom 1 u A B w A B if t D F t f t + i g t 0 *
337 330 abscld φ f dom 1 g dom 1 t D f t + i g t
338 0red φ f dom 1 g dom 1 ¬ t D 0
339 337 338 ifclda φ f dom 1 g dom 1 if t D f t + i g t 0
340 0red φ ¬ t D 0
341 301 340 ifclda φ if t D F t 0
342 311 340 ifclda φ if t D F t 0
343 341 342 readdcld φ if t D F t 0 + if t D F t 0
344 343 adantr φ f dom 1 g dom 1 if t D F t 0 + if t D F t 0
345 339 344 readdcld φ f dom 1 g dom 1 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
346 345 rexrd φ f dom 1 g dom 1 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 *
347 346 adantr φ f dom 1 g dom 1 u A B w A B if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 *
348 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 f t + i g t 0 if t u w F t f t + i g t 0 if t D F t f t + i g t 0
349 breq1 0 = if t u w F t f t + i g t 0 0 if t D F t f t + i g t 0 if t u w F t f t + i g t 0 if t D F t f t + i g t 0
350 224 adantllr φ f dom 1 g dom 1 u A B w A B t u w t D
351 332 leidd φ f dom 1 g dom 1 t D F t f t + i g t F t f t + i g t
352 351 adantlr φ f dom 1 g dom 1 u A B w A B t D F t f t + i g t F t f t + i g t
353 iftrue t D if t D F t f t + i g t 0 = F t f t + i g t
354 353 adantl φ f dom 1 g dom 1 u A B w A B t D if t D F t f t + i g t 0 = F t f t + i g t
355 352 354 breqtrrd φ 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 f t + i g t 0
356 350 355 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 f t + i g t 0
357 breq2 F t f t + i g t = if t D F t f t + i g t 0 0 F t f t + i g t 0 if t D F t f t + i g t 0
358 breq2 0 = if t D F t f t + i g t 0 0 0 0 if t D F t f t + i g t 0
359 331 absge0d φ f dom 1 g dom 1 t D 0 F t f t + i g t
360 357 358 359 236 ifbothda φ f dom 1 g dom 1 0 if t D F t f t + i g t 0
361 360 ad2antrr φ f dom 1 g dom 1 u A B w A B ¬ t u w 0 if t D F t f t + i g t 0
362 348 349 356 361 ifbothda φ f dom 1 g dom 1 u A B w A B if t u w F t f t + i g t 0 if t D F t f t + i g t 0
363 254 negcld φ t D F t
364 363 adantlr φ f dom 1 g dom 1 t D F t
365 330 364 addcld φ f dom 1 g dom 1 t D f t + i g t + F t
366 365 abscld φ f dom 1 g dom 1 t D f t + i g t + F t
367 363 abscld φ t D F t
368 367 adantlr φ f dom 1 g dom 1 t D F t
369 337 368 readdcld φ f dom 1 g dom 1 t D f t + i g t + F t
370 301 311 readdcld φ t D F t + F t
371 370 adantlr φ f dom 1 g dom 1 t D F t + F t
372 337 371 readdcld φ f dom 1 g dom 1 t D f t + i g t + F t + F t
373 330 364 abstrid φ f dom 1 g dom 1 t D f t + i g t + F t f t + i g t + F t
374 mulcl i F t i F t
375 31 310 374 sylancr φ t D i F t
376 300 375 abstrid φ t D F t + i F t F t + i F t
377 254 absnegd φ t D F t = F t
378 254 replimd φ t D F t = F t + i F t
379 378 fveq2d φ t D F t = F t + i F t
380 377 379 eqtrd φ t D F t = F t + i F t
381 absmul i F t i F t = i F t
382 31 310 381 sylancr φ t D i F t = i F t
383 182 oveq1i i F t = 1 F t
384 382 383 eqtrdi φ t D i F t = 1 F t
385 311 recnd φ t D F t
386 385 mulid2d φ t D 1 F t = F t
387 384 386 eqtr2d φ t D F t = i F t
388 387 oveq2d φ t D F t + F t = F t + i F t
389 376 380 388 3brtr4d φ t D F t F t + F t
390 389 adantlr φ f dom 1 g dom 1 t D F t F t + F t
391 368 371 337 390 leadd2dd φ f dom 1 g dom 1 t D f t + i g t + F t f t + i g t + F t + F t
392 366 369 372 373 391 letrd φ f dom 1 g dom 1 t D f t + i g t + F t f t + i g t + F t + F t
393 328 330 abssubd φ f dom 1 g dom 1 t D F t f t + i g t = f t + i g t - F t
394 353 adantl φ f dom 1 g dom 1 t D if t D F t f t + i g t 0 = F t f t + i g t
395 330 328 negsubd φ f dom 1 g dom 1 t D f t + i g t + F t = f t + i g t - F t
396 395 fveq2d φ f dom 1 g dom 1 t D f t + i g t + F t = f t + i g t - F t
397 393 394 396 3eqtr4d φ f dom 1 g dom 1 t D if t D F t f t + i g t 0 = f t + i g t + F t
398 iftrue t D if t D f t + i g t + F t + F t 0 = f t + i g t + F t + F t
399 398 adantl φ f dom 1 g dom 1 t D if t D f t + i g t + F t + F t 0 = f t + i g t + F t + F t
400 392 397 399 3brtr4d φ f dom 1 g dom 1 t D if t D F t f t + i g t 0 if t D f t + i g t + F t + F t 0
401 400 ex φ f dom 1 g dom 1 t D if t D F t f t + i g t 0 if t D f t + i g t + F t + F t 0
402 235 a1i ¬ t D 0 0
403 iffalse ¬ t D if t D F t f t + i g t 0 = 0
404 iffalse ¬ t D if t D f t + i g t + F t + F t 0 = 0
405 402 403 404 3brtr4d ¬ t D if t D F t f t + i g t 0 if t D f t + i g t + F t + F t 0
406 401 405 pm2.61d1 φ f dom 1 g dom 1 if t D F t f t + i g t 0 if t D f t + i g t + F t + F t 0
407 iftrue t D if t D F t 0 = F t
408 iftrue t D if t D F t 0 = F t
409 407 408 oveq12d t D if t D F t 0 + if t D F t 0 = F t + F t
410 225 409 oveq12d t D if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 = f t + i g t + F t + F t
411 410 398 eqtr4d t D if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 = if t D f t + i g t + F t + F t 0
412 00id 0 + 0 = 0
413 412 oveq2i 0 + 0 + 0 = 0 + 0
414 413 412 eqtri 0 + 0 + 0 = 0
415 iffalse ¬ t D if t D f t + i g t 0 = 0
416 iffalse ¬ t D if t D F t 0 = 0
417 iffalse ¬ t D if t D F t 0 = 0
418 416 417 oveq12d ¬ t D if t D F t 0 + if t D F t 0 = 0 + 0
419 415 418 oveq12d ¬ t D if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 = 0 + 0 + 0
420 414 419 404 3eqtr4a ¬ t D if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 = if t D f t + i g t + F t + F t 0
421 411 420 pm2.61i if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 = if t D f t + i g t + F t + F t 0
422 406 421 breqtrrdi φ f dom 1 g dom 1 if t D F t f t + i g t 0 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
423 422 adantr φ f dom 1 g dom 1 u A B w A B if t D F t f t + i g t 0 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
424 327 336 347 362 423 xrletrd φ f dom 1 g dom 1 u A B w A B if t u w F t f t + i g t 0 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
425 424 ralrimivw φ 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 + i g t 0 + if t D F t 0 + if t D F t 0
426 fvex F t f t + i g t V
427 426 17 ifex if t u w F t f t + i g t 0 V
428 427 a1i φ t if t u w F t f t + i g t 0 V
429 ovexd φ t if t D f t + i g t 0 + if t D F t 0 + if t D F t 0 V
430 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
431 ovexd φ t if t D F t 0 + if t D F t 0 V
432 341 adantr φ t if t D F t 0
433 342 adantr φ t if t D F t 0
434 eqidd φ t if t D F t 0 = t if t D F t 0
435 eqidd φ t if t D F t 0 = t if t D F t 0
436 241 432 433 434 435 offval2 φ t if t D F t 0 + f t if t D F t 0 = t if t D F t 0 + if t D F t 0
437 241 244 431 246 436 offval2 φ t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 = t if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
438 241 428 429 430 437 ofrfval2 φ t if t u w F t f t + i g t 0 f t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 t if t u w F t f t + i g t 0 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
439 438 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 + i g t 0 + f t if t D F t 0 + f t if t D F t 0 t if t u w F t f t + i g t 0 if t D f t + i g t 0 + if t D F t 0 + if t D F t 0
440 425 439 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 + i g t 0 + f t if t D F t 0 + f t if t D F t 0
441 itg2le t if t u w F t f t + i g t 0 : 0 +∞ t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 : 0 +∞ t if t u w F t f t + i g t 0 f t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 2 t if t u w F t f t + i g t 0 2 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0
442 276 324 440 441 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 + i g t 0 + f t if t D F t 0 + f t if t D F t 0
443 6 adantr φ f dom 1 g dom 1 D
444 243 a1i φ f dom 1 g dom 1 t D if t D f t + i g t 0 V
445 eldifn t D ¬ t D
446 445 iffalsed t D if t D f t + i g t 0 = 0
447 446 adantl φ f dom 1 g dom 1 t D if t D f t + i g t 0 = 0
448 ovexd f dom 1 g dom 1 t i g t V
449 41 42 448 45 52 offval2 f dom 1 g dom 1 f + f × i × f g = t f t + i g t
450 39 449 56 57 fmptco f dom 1 g dom 1 abs f + f × i × f g = t f t + i g t
451 450 reseq1d f dom 1 g dom 1 abs f + f × i × f g D = t f t + i g t D
452 6 resmptd φ t f t + i g t D = t D f t + i g t
453 451 452 sylan9eqr φ f dom 1 g dom 1 abs f + f × i × f g D = t D f t + i g t
454 225 mpteq2ia t D if t D f t + i g t 0 = t D f t + i g t
455 453 454 eqtr4di φ f dom 1 g dom 1 abs f + f × i × f g D = t D if t D f t + i g t 0
456 i1fmbf abs f + f × i × f g dom 1 abs f + f × i × f g MblFn
457 59 456 syl f dom 1 g dom 1 abs f + f × i × f g MblFn
458 8 fdmd φ dom F = D
459 iblmbf F 𝐿 1 F MblFn
460 mbfdm F MblFn dom F dom vol
461 7 459 460 3syl φ dom F dom vol
462 458 461 eqeltrrd φ D dom vol
463 mbfres abs f + f × i × f g MblFn D dom vol abs f + f × i × f g D MblFn
464 457 462 463 syl2anr φ f dom 1 g dom 1 abs f + f × i × f g D MblFn
465 455 464 eqeltrrd φ f dom 1 g dom 1 t D if t D f t + i g t 0 MblFn
466 443 15 444 447 465 mbfss φ f dom 1 g dom 1 t if t D f t + i g t 0 MblFn
467 200 adantl φ f dom 1 g dom 1 2 t if t D f t + i g t 0
468 0cnd φ ¬ t D 0
469 300 468 ifclda φ if t D F t 0
470 469 adantr φ t if t D F t 0
471 eqidd φ t if t D F t 0 = t if t D F t 0
472 54 a1i φ abs :
473 472 feqmptd φ abs = x x
474 fveq2 x = if t D F t 0 x = if t D F t 0
475 fvif if t D F t 0 = if t D F t 0
476 abs0 0 = 0
477 ifeq2 0 = 0 if t D F t 0 = if t D F t 0
478 476 477 ax-mp if t D F t 0 = if t D F t 0
479 475 478 eqtri if t D F t 0 = if t D F t 0
480 474 479 eqtrdi x = if t D F t 0 x = if t D F t 0
481 470 471 473 480 fmptco φ abs t if t D F t 0 = t if t D F t 0
482 299 340 ifclda φ if t D F t 0
483 482 adantr φ t if t D F t 0
484 483 fmpttd φ t if t D F t 0 :
485 14 a1i φ dom vol
486 482 adantr φ t D if t D F t 0
487 445 adantl φ t D ¬ t D
488 487 iffalsed φ t D if t D F t 0 = 0
489 iftrue t D if t D F t 0 = F t
490 489 mpteq2ia t D if t D F t 0 = t D F t
491 8 feqmptd φ F = t D F t
492 7 459 syl φ F MblFn
493 491 492 eqeltrrd φ t D F t MblFn
494 254 ismbfcn2 φ t D F t MblFn t D F t MblFn t D F t MblFn
495 493 494 mpbid φ t D F t MblFn t D F t MblFn
496 495 simpld φ t D F t MblFn
497 490 496 eqeltrid φ t D if t D F t 0 MblFn
498 6 485 486 488 497 mbfss φ t if t D F t 0 MblFn
499 ftc1anclem1 t if t D F t 0 : t if t D F t 0 MblFn abs t if t D F t 0 MblFn
500 484 498 499 syl2anc φ abs t if t D F t 0 MblFn
501 481 500 eqeltrrd φ t if t D F t 0 MblFn
502 501 308 282 317 288 itg2addnc φ 2 t if t D F t 0 + f t if t D F t 0 = 2 t if t D F t 0 + 2 t if t D F t 0
503 502 289 eqeltrd φ 2 t if t D F t 0 + f t if t D F t 0
504 503 adantr φ f dom 1 g dom 1 2 t if t D F t 0 + f t if t D F t 0
505 466 297 467 319 504 itg2addnc φ f dom 1 g dom 1 2 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 = 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + f t if t D F t 0
506 502 adantr φ f dom 1 g dom 1 2 t if t D F t 0 + f t if t D F t 0 = 2 t if t D F t 0 + 2 t if t D F t 0
507 506 oveq2d φ f dom 1 g dom 1 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + f t if t D F t 0 = 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0
508 505 507 eqtrd φ f dom 1 g dom 1 2 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 = 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0
509 508 adantr φ f dom 1 g dom 1 u A B w A B 2 t if t D f t + i g t 0 + f t if t D F t 0 + f t if t D F t 0 = 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0
510 442 509 breqtrd φ 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 + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0
511 itg2lecl t if t u w F t f t + i g t 0 : 0 +∞ 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0 2 t if t u w F t f t + i g t 0 2 t if t D f t + i g t 0 + 2 t if t D F t 0 + 2 t if t D F t 0 2 t if t u w F t f t + i g t 0
512 276 291 510 511 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
513 69 78 253 269 512 itg2addnc φ f dom 1 g dom 1 u A B w A B 2 t if t u w f t + i g t 0 + f t if t u w F t f t + i g t 0 = 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
514 241 242 428 245 430 offval2 φ t if t u w f t + i g t 0 + f t if t u w F t f t + i g t 0 = t if t u w f t + i g t 0 + if t u w F t f t + i g t 0
515 eqeq2 f t + i g t + F t f t + i g t = if t u w f t + i g t + F t f t + i g t 0 if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = f t + i g t + F t f t + i g t if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = if t u w f t + i g t + F t f t + i g t 0
516 eqeq2 0 = if t u w f t + i g t + F t f t + i g t 0 if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = 0 if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = if t u w f t + i g t + F t f t + i g t 0
517 iftrue t u w if t u w F t f t + i g t 0 = F t f t + i g t
518 23 517 oveq12d t u w if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = f t + i g t + F t f t + i g t
519 518 adantl φ t u w if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = f t + i g t + F t f t + i g t
520 iffalse ¬ t u w if t u w f t + i g t 0 = 0
521 iffalse ¬ t u w if t u w F t f t + i g t 0 = 0
522 520 521 oveq12d ¬ t u w if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = 0 + 0
523 522 412 eqtrdi ¬ t u w if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = 0
524 523 adantl φ ¬ t u w if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = 0
525 515 516 519 524 ifbothda φ if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = if t u w f t + i g t + F t f t + i g t 0
526 525 mpteq2dv φ t if t u w f t + i g t 0 + if t u w F t f t + i g t 0 = t if t u w f t + i g t + F t f t + i g t 0
527 514 526 eqtrd φ t if t u w f t + i g t 0 + f t if t u w F t f t + i g t 0 = t if t u w f t + i g t + F t f t + i g t 0
528 527 ad2antrr φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 + f t if t u w F t f t + i g t 0 = t if t u w f t + i g t + F t f t + i g t 0
529 simplr φ f dom 1 g dom 1 u A B w A B f dom 1 g dom 1
530 258 abscld f dom 1 g dom 1 t u w f t + i g t
531 530 recnd f dom 1 g dom 1 t u w f t + i g t
532 529 531 sylan φ f dom 1 g dom 1 u A B w A B t u w f t + i g t
533 262 recnd φ f dom 1 g dom 1 u A B w A B t u w F t f t + i g t
534 532 533 addcomd φ f dom 1 g dom 1 u A B w A B t u w f t + i g t + F t f t + i g t = F t f t + i g t + f t + i g t
535 534 ifeq1da φ f dom 1 g dom 1 u A B w A B if t u w f t + i g t + F t f t + i g t 0 = if t u w F t f t + i g t + f t + i g t 0
536 535 mpteq2dv φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t + F t f t + i g t 0 = t if t u w F t f t + i g t + f t + i g t 0
537 528 536 eqtrd φ f dom 1 g dom 1 u A B w A B t if t u w f t + i g t 0 + f 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 + f t + i g t 0
538 537 fveq2d φ f dom 1 g dom 1 u A B w A B 2 t if t u w f t + i g t 0 + f t if t u w F t f t + i g t 0 = 2 t if t u w F t f t + i g t + f t + i g t 0
539 513 538 eqtr3d φ f dom 1 g dom 1 u A B w A B 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 = 2 t if t u w F t f t + i g t + f t + i g t 0
540 10 11 539 syl2an φ 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 t if t u w F t f t + i g t 0 = 2 t if t u w F t f t + i g t + f t + i g t 0
541 540 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 t if t u w F t f t + i g t 0 = 2 t if t u w F t f t + i g t + f t + i g t 0
542 rpcn y + y
543 542 2halvesd y + y 2 + y 2 = y
544 543 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 + y 2 = y
545 9 541 544 3brtr3d φ 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 + f t + i g t 0 < y