Metamath Proof Explorer

Theorem ftc1anclem5

Description: Lemma for ftc1anc , the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018)

Ref Expression
Hypotheses ftc1anc.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1anc.a 
|- ( ph -> A e. RR )
ftc1anc.b 
|- ( ph -> B e. RR )
ftc1anc.le 
|- ( ph -> A <_ B )
ftc1anc.s 
|- ( ph -> ( A (,) B ) C_ D )
ftc1anc.d 
|- ( ph -> D C_ RR )
ftc1anc.i 
|- ( ph -> F e. L^1 )
ftc1anc.f 
|- ( ph -> F : D --> CC )
Assertion ftc1anclem5 
|- ( ( ph /\ Y e. RR+ ) -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y )

Proof

Step Hyp Ref Expression
1 ftc1anc.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1anc.a 
 |-  ( ph -> A e. RR )
3 ftc1anc.b 
 |-  ( ph -> B e. RR )
4 ftc1anc.le 
 |-  ( ph -> A <_ B )
5 ftc1anc.s 
 |-  ( ph -> ( A (,) B ) C_ D )
6 ftc1anc.d 
 |-  ( ph -> D C_ RR )
7 ftc1anc.i 
 |-  ( ph -> F e. L^1 )
8 ftc1anc.f 
 |-  ( ph -> F : D --> CC )
9 iftrue 
 |-  ( t e. RR -> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
10 9 mpteq2ia 
 |-  ( t e. RR |-> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) ) = ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
11 10 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
12 8 ffvelcdmda 
 |-  ( ( ph /\ t e. D ) -> ( F ` t ) e. CC )
13 0cnd 
 |-  ( ( ph /\ -. t e. D ) -> 0 e. CC )
14 12 13 ifclda 
 |-  ( ph -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
15 14 recld 
 |-  ( ph -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
16 15 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
17 rembl 
 |-  RR e. dom vol
18 17 a1i 
 |-  ( ph -> RR e. dom vol )
19 15 adantr 
 |-  ( ( ph /\ t e. D ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
20 eldifn 
 |-  ( t e. ( RR \ D ) -> -. t e. D )
21 20 adantl 
 |-  ( ( ph /\ t e. ( RR \ D ) ) -> -. t e. D )
22 iffalse 
 |-  ( -. t e. D -> if ( t e. D , ( F ` t ) , 0 ) = 0 )
23 22 fveq2d 
 |-  ( -. t e. D -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) = ( Re ` 0 ) )
24 re0 
 |-  ( Re ` 0 ) = 0
25 23 24 eqtrdi 
 |-  ( -. t e. D -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) = 0 )
26 21 25 syl 
 |-  ( ( ph /\ t e. ( RR \ D ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) = 0 )
27 iftrue 
 |-  ( t e. D -> if ( t e. D , ( F ` t ) , 0 ) = ( F ` t ) )
28 27 fveq2d 
 |-  ( t e. D -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) = ( Re ` ( F ` t ) ) )
29 28 mpteq2ia 
 |-  ( t e. D |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = ( t e. D |-> ( Re ` ( F ` t ) ) )
30 8 feqmptd 
 |-  ( ph -> F = ( t e. D |-> ( F ` t ) ) )
31 30 7 eqeltrrd 
 |-  ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
32 12 iblcn 
 |-  ( ph -> ( ( t e. D |-> ( F ` t ) ) e. L^1 <-> ( ( t e. D |-> ( Re ` ( F ` t ) ) ) e. L^1 /\ ( t e. D |-> ( Im ` ( F ` t ) ) ) e. L^1 ) ) )
33 31 32 mpbid 
 |-  ( ph -> ( ( t e. D |-> ( Re ` ( F ` t ) ) ) e. L^1 /\ ( t e. D |-> ( Im ` ( F ` t ) ) ) e. L^1 ) )
34 33 simpld 
 |-  ( ph -> ( t e. D |-> ( Re ` ( F ` t ) ) ) e. L^1 )
35 29 34 eqeltrid 
 |-  ( ph -> ( t e. D |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. L^1 )
36 6 18 19 26 35 iblss2 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. L^1 )
37 15 recnd 
 |-  ( ph -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC )
38 37 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC )
39 eqidd 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
40 absf 
 |-  abs : CC --> RR
41 40 a1i 
 |-  ( ph -> abs : CC --> RR )
42 41 feqmptd 
 |-  ( ph -> abs = ( x e. CC |-> ( abs ` x ) ) )
43 fveq2 
 |-  ( x = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( abs ` x ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
44 38 39 42 43 fmptco 
 |-  ( ph -> ( abs o. ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) = ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
45 16 fmpttd 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) : RR --> RR )
46 iblmbf 
 |-  ( F e. L^1 -> F e. MblFn )
47 7 46 syl 
 |-  ( ph -> F e. MblFn )
48 30 47 eqeltrrd 
 |-  ( ph -> ( t e. D |-> ( F ` t ) ) e. MblFn )
49 12 ismbfcn2 
 |-  ( ph -> ( ( t e. D |-> ( F ` t ) ) e. MblFn <-> ( ( t e. D |-> ( Re ` ( F ` t ) ) ) e. MblFn /\ ( t e. D |-> ( Im ` ( F ` t ) ) ) e. MblFn ) ) )
50 48 49 mpbid 
 |-  ( ph -> ( ( t e. D |-> ( Re ` ( F ` t ) ) ) e. MblFn /\ ( t e. D |-> ( Im ` ( F ` t ) ) ) e. MblFn ) )
51 50 simpld 
 |-  ( ph -> ( t e. D |-> ( Re ` ( F ` t ) ) ) e. MblFn )
52 29 51 eqeltrid 
 |-  ( ph -> ( t e. D |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn )
53 6 18 19 26 52 mbfss 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn )
54 ftc1anclem1 
 |-  ( ( ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) : RR --> RR /\ ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn ) -> ( abs o. ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. MblFn )
55 45 53 54 syl2anc 
 |-  ( ph -> ( abs o. ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. MblFn )
56 44 55 eqeltrrd 
 |-  ( ph -> ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. MblFn )
57 16 36 56 iblabsnc 
 |-  ( ph -> ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. L^1 )
58 37 abscld 
 |-  ( ph -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. RR )
59 58 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. RR )
60 37 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
61 60 adantr 
 |-  ( ( ph /\ t e. RR ) -> 0 <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
62 59 61 iblpos 
 |-  ( ph -> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. L^1 <-> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) ) ) e. RR ) ) )
63 57 62 mpbid 
 |-  ( ph -> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) ) ) e. RR ) )
64 63 simprd 
 |-  ( ph -> ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) , 0 ) ) ) e. RR )
65 11 64 eqeltrrid 
 |-  ( ph -> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) e. RR )
66 ltsubrp 
 |-  ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) e. RR /\ Y e. RR+ ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) )
67 65 66 sylan 
 |-  ( ( ph /\ Y e. RR+ ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) )
68 rpre 
 |-  ( Y e. RR+ -> Y e. RR )
69 resubcl 
 |-  ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) e. RR /\ Y e. RR ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR )
70 65 68 69 syl2an 
 |-  ( ( ph /\ Y e. RR+ ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR )
71 65 adantr 
 |-  ( ( ph /\ Y e. RR+ ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) e. RR )
72 70 71 ltnled 
 |-  ( ( ph /\ Y e. RR+ ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) <-> -. ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
73 67 72 mpbid 
 |-  ( ( ph /\ Y e. RR+ ) -> -. ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) )
74 58 rexrd 
 |-  ( ph -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. RR* )
75 elxrge0 
 |-  ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. RR* /\ 0 <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
76 74 60 75 sylanbrc 
 |-  ( ph -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. ( 0 [,] +oo ) )
77 76 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. ( 0 [,] +oo ) )
78 77 fmpttd 
 |-  ( ph -> ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
79 78 adantr 
 |-  ( ( ph /\ Y e. RR+ ) -> ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
80 70 rexrd 
 |-  ( ( ph /\ Y e. RR+ ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR* )
81 itg2leub 
 |-  ( ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR* ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) <-> A. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) ) )
82 79 80 81 syl2anc 
 |-  ( ( ph /\ Y e. RR+ ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) <-> A. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) ) )
83 73 82 mtbid 
 |-  ( ( ph /\ Y e. RR+ ) -> -. A. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
84 rexanali 
 |-  ( E. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) <-> -. A. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
85 83 84 sylibr 
 |-  ( ( ph /\ Y e. RR+ ) -> E. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
86 70 ad2antrr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR )
87 itg1cl 
 |-  ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
88 87 ad2antlr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( S.1 ` g ) e. RR )
89 eqid 
 |-  ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
90 89 i1fpos 
 |-  ( g e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 )
91 0re 
 |-  0 e. RR
92 i1ff 
 |-  ( g e. dom S.1 -> g : RR --> RR )
93 92 ffvelcdmda 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. RR )
94 max1 
 |-  ( ( 0 e. RR /\ ( g ` t ) e. RR ) -> 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
95 91 93 94 sylancr 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
96 95 ralrimiva 
 |-  ( g e. dom S.1 -> A. t e. RR 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
97 ax-resscn 
 |-  RR C_ CC
98 97 a1i 
 |-  ( g e. dom S.1 -> RR C_ CC )
99 fvex 
 |-  ( g ` t ) e. _V
100 c0ex 
 |-  0 e. _V
101 99 100 ifex 
 |-  if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. _V
102 101 89 fnmpti 
 |-  ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) Fn RR
103 102 a1i 
 |-  ( g e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) Fn RR )
104 98 103 0pledm 
 |-  ( g e. dom S.1 -> ( 0p oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> ( RR X. { 0 } ) oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
105 reex 
 |-  RR e. _V
106 105 a1i 
 |-  ( g e. dom S.1 -> RR e. _V )
107 100 a1i 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> 0 e. _V )
108 ifcl 
 |-  ( ( ( g ` t ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR )
109 93 91 108 sylancl 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR )
110 fconstmpt 
 |-  ( RR X. { 0 } ) = ( t e. RR |-> 0 )
111 110 a1i 
 |-  ( g e. dom S.1 -> ( RR X. { 0 } ) = ( t e. RR |-> 0 ) )
112 eqidd 
 |-  ( g e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
113 106 107 109 111 112 ofrfval2 
 |-  ( g e. dom S.1 -> ( ( RR X. { 0 } ) oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> A. t e. RR 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
114 104 113 bitrd 
 |-  ( g e. dom S.1 -> ( 0p oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> A. t e. RR 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
115 96 114 mpbird 
 |-  ( g e. dom S.1 -> 0p oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
116 itg2itg1 
 |-  ( ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 /\ 0p oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
117 90 115 116 syl2anc 
 |-  ( g e. dom S.1 -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
118 itg1cl 
 |-  ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
119 90 118 syl 
 |-  ( g e. dom S.1 -> ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
120 117 119 eqeltrd 
 |-  ( g e. dom S.1 -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
121 120 ad2antlr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
122 ltnle 
 |-  ( ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) e. RR /\ ( S.1 ` g ) e. RR ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.1 ` g ) <-> -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
123 70 87 122 syl2an 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.1 ` g ) <-> -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) )
124 123 biimpar 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.1 ` g ) )
125 max2 
 |-  ( ( 0 e. RR /\ ( g ` t ) e. RR ) -> ( g ` t ) <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
126 91 93 125 sylancr 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
127 126 ralrimiva 
 |-  ( g e. dom S.1 -> A. t e. RR ( g ` t ) <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
128 92 feqmptd 
 |-  ( g e. dom S.1 -> g = ( t e. RR |-> ( g ` t ) ) )
129 106 93 109 128 112 ofrfval2 
 |-  ( g e. dom S.1 -> ( g oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> A. t e. RR ( g ` t ) <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
130 127 129 mpbird 
 |-  ( g e. dom S.1 -> g oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
131 itg1le 
 |-  ( ( g e. dom S.1 /\ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 /\ g oR <_ ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) -> ( S.1 ` g ) <_ ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
132 90 130 131 mpd3an23 
 |-  ( g e. dom S.1 -> ( S.1 ` g ) <_ ( S.1 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
133 132 117 breqtrrd 
 |-  ( g e. dom S.1 -> ( S.1 ` g ) <_ ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
134 133 ad2antlr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( S.1 ` g ) <_ ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
135 86 88 121 124 134 ltletrd 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
136 135 adantrl 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
137 i1fmbf 
 |-  ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. MblFn )
138 90 137 syl 
 |-  ( g e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. MblFn )
139 138 adantl 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. MblFn )
140 elrege0 
 |-  ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR /\ 0 <_ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
141 109 95 140 sylanbrc 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. ( 0 [,) +oo ) )
142 141 fmpttd 
 |-  ( g e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
143 142 adantl 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
144 120 adantl 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
145 109 recnd 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC )
146 145 negcld 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC )
147 145 146 ifcld 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. CC )
148 subcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. CC ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. CC )
149 37 147 148 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. CC )
150 149 anassrs 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. CC )
151 150 abscld 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) e. RR )
152 150 absge0d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
153 elrege0 
 |-  ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) e. RR /\ 0 <_ ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) )
154 151 152 153 sylanbrc 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) e. ( 0 [,) +oo ) )
155 154 fmpttd 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) : RR --> ( 0 [,) +oo ) )
156 eleq1w 
 |-  ( x = t -> ( x e. D <-> t e. D ) )
157 fveq2 
 |-  ( x = t -> ( F ` x ) = ( F ` t ) )
158 156 157 ifbieq1d 
 |-  ( x = t -> if ( x e. D , ( F ` x ) , 0 ) = if ( t e. D , ( F ` t ) , 0 ) )
159 158 fveq2d 
 |-  ( x = t -> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
160 eqid 
 |-  ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) = ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) )
161 fvex 
 |-  ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. _V
162 159 160 161 fvmpt 
 |-  ( t e. RR -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
163 159 breq2d 
 |-  ( x = t -> ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) <-> 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
164 fveq2 
 |-  ( x = t -> ( g ` x ) = ( g ` t ) )
165 164 breq2d 
 |-  ( x = t -> ( 0 <_ ( g ` x ) <-> 0 <_ ( g ` t ) ) )
166 165 164 ifbieq1d 
 |-  ( x = t -> if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
167 166 negeqd 
 |-  ( x = t -> -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) = -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
168 163 166 167 ifbieq12d 
 |-  ( x = t -> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) = if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
169 eqid 
 |-  ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
170 negex 
 |-  -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. _V
171 101 170 ifex 
 |-  if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. _V
172 168 169 171 fvmpt 
 |-  ( t e. RR -> ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) = if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
173 162 172 oveq12d 
 |-  ( t e. RR -> ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
174 173 fveq2d 
 |-  ( t e. RR -> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
175 174 mpteq2ia 
 |-  ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
176 175 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) )
177 105 a1i 
 |-  ( ph -> RR e. _V )
178 fvex 
 |-  ( g ` x ) e. _V
179 178 100 ifex 
 |-  if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) e. _V
180 179 100 ifex 
 |-  if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) e. _V
181 180 a1i 
 |-  ( ( ph /\ x e. RR ) -> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) e. _V )
182 ovex 
 |-  ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) e. _V
183 100 182 ifex 
 |-  if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. _V
184 183 a1i 
 |-  ( ( ph /\ x e. RR ) -> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. _V )
185 ffn 
 |-  ( F : D --> CC -> F Fn D )
186 frn 
 |-  ( F : D --> CC -> ran F C_ CC )
187 ref 
 |-  Re : CC --> RR
188 ffn 
 |-  ( Re : CC --> RR -> Re Fn CC )
189 187 188 ax-mp 
 |-  Re Fn CC
190 fnco 
 |-  ( ( Re Fn CC /\ F Fn D /\ ran F C_ CC ) -> ( Re o. F ) Fn D )
191 189 190 mp3an1 
 |-  ( ( F Fn D /\ ran F C_ CC ) -> ( Re o. F ) Fn D )
192 185 186 191 syl2anc 
 |-  ( F : D --> CC -> ( Re o. F ) Fn D )
193 elpreima 
 |-  ( ( Re o. F ) Fn D -> ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) <-> ( x e. D /\ ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) ) ) )
194 8 192 193 3syl 
 |-  ( ph -> ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) <-> ( x e. D /\ ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) ) ) )
195 fco 
 |-  ( ( Re : CC --> RR /\ F : D --> CC ) -> ( Re o. F ) : D --> RR )
196 187 8 195 sylancr 
 |-  ( ph -> ( Re o. F ) : D --> RR )
197 196 ffvelcdmda 
 |-  ( ( ph /\ x e. D ) -> ( ( Re o. F ) ` x ) e. RR )
198 197 biantrurd 
 |-  ( ( ph /\ x e. D ) -> ( 0 <_ ( ( Re o. F ) ` x ) <-> ( ( ( Re o. F ) ` x ) e. RR /\ 0 <_ ( ( Re o. F ) ` x ) ) ) )
199 elrege0 
 |-  ( ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( Re o. F ) ` x ) e. RR /\ 0 <_ ( ( Re o. F ) ` x ) ) )
200 198 199 bitr4di 
 |-  ( ( ph /\ x e. D ) -> ( 0 <_ ( ( Re o. F ) ` x ) <-> ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) ) )
201 fvco3 
 |-  ( ( F : D --> CC /\ x e. D ) -> ( ( Re o. F ) ` x ) = ( Re ` ( F ` x ) ) )
202 8 201 sylan 
 |-  ( ( ph /\ x e. D ) -> ( ( Re o. F ) ` x ) = ( Re ` ( F ` x ) ) )
203 202 breq2d 
 |-  ( ( ph /\ x e. D ) -> ( 0 <_ ( ( Re o. F ) ` x ) <-> 0 <_ ( Re ` ( F ` x ) ) ) )
204 200 203 bitr3d 
 |-  ( ( ph /\ x e. D ) -> ( ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) <-> 0 <_ ( Re ` ( F ` x ) ) ) )
205 204 pm5.32da 
 |-  ( ph -> ( ( x e. D /\ ( ( Re o. F ) ` x ) e. ( 0 [,) +oo ) ) <-> ( x e. D /\ 0 <_ ( Re ` ( F ` x ) ) ) ) )
206 194 205 bitrd 
 |-  ( ph -> ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) <-> ( x e. D /\ 0 <_ ( Re ` ( F ` x ) ) ) ) )
207 206 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) <-> ( x e. D /\ 0 <_ ( Re ` ( F ` x ) ) ) ) )
208 eldif 
 |-  ( x e. ( RR \ D ) <-> ( x e. RR /\ -. x e. D ) )
209 208 baibr 
 |-  ( x e. RR -> ( -. x e. D <-> x e. ( RR \ D ) ) )
210 0le0 
 |-  0 <_ 0
211 210 24 breqtrri 
 |-  0 <_ ( Re ` 0 )
212 211 biantru 
 |-  ( -. x e. D <-> ( -. x e. D /\ 0 <_ ( Re ` 0 ) ) )
213 209 212 bitr3di 
 |-  ( x e. RR -> ( x e. ( RR \ D ) <-> ( -. x e. D /\ 0 <_ ( Re ` 0 ) ) ) )
214 213 adantl 
 |-  ( ( ph /\ x e. RR ) -> ( x e. ( RR \ D ) <-> ( -. x e. D /\ 0 <_ ( Re ` 0 ) ) ) )
215 207 214 orbi12d 
 |-  ( ( ph /\ x e. RR ) -> ( ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) \/ x e. ( RR \ D ) ) <-> ( ( x e. D /\ 0 <_ ( Re ` ( F ` x ) ) ) \/ ( -. x e. D /\ 0 <_ ( Re ` 0 ) ) ) ) )
216 elun 
 |-  ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) <-> ( x e. ( `' ( Re o. F ) " ( 0 [,) +oo ) ) \/ x e. ( RR \ D ) ) )
217 fveq2 
 |-  ( if ( x e. D , ( F ` x ) , 0 ) = ( F ` x ) -> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) = ( Re ` ( F ` x ) ) )
218 217 breq2d 
 |-  ( if ( x e. D , ( F ` x ) , 0 ) = ( F ` x ) -> ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) <-> 0 <_ ( Re ` ( F ` x ) ) ) )
219 fveq2 
 |-  ( if ( x e. D , ( F ` x ) , 0 ) = 0 -> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) = ( Re ` 0 ) )
220 219 breq2d 
 |-  ( if ( x e. D , ( F ` x ) , 0 ) = 0 -> ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) <-> 0 <_ ( Re ` 0 ) ) )
221 218 220 elimif 
 |-  ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) <-> ( ( x e. D /\ 0 <_ ( Re ` ( F ` x ) ) ) \/ ( -. x e. D /\ 0 <_ ( Re ` 0 ) ) ) )
222 215 216 221 3bitr4g 
 |-  ( ( ph /\ x e. RR ) -> ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) <-> 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) )
223 222 ifbid 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) )
224 223 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) )
225 222 ifbid 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) = if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) )
226 225 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) )
227 177 181 184 224 226 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) oF + ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) = ( x e. RR |-> ( if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) + if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) )
228 ovif12 
 |-  ( if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) + if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) = if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , ( if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) + 0 ) , ( 0 + ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) )
229 92 ffvelcdmda 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( g ` x ) e. RR )
230 229 recnd 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( g ` x ) e. CC )
231 0cn 
 |-  0 e. CC
232 ifcl 
 |-  ( ( ( g ` x ) e. CC /\ 0 e. CC ) -> if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) e. CC )
233 230 231 232 sylancl 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) e. CC )
234 233 addridd 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) + 0 ) = if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
235 233 mulm1d 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) = -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
236 235 oveq2d 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( 0 + ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) = ( 0 + -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
237 233 negcld 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) e. CC )
238 237 addlidd 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( 0 + -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) = -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
239 236 238 eqtrd 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( 0 + ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) = -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
240 234 239 ifeq12d 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , ( if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) + 0 ) , ( 0 + ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) = if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
241 228 240 eqtrid 
 |-  ( ( g e. dom S.1 /\ x e. RR ) -> ( if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) + if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) = if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
242 241 mpteq2dva 
 |-  ( g e. dom S.1 -> ( x e. RR |-> ( if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) + if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) )
243 227 242 sylan9eq 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) oF + ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) )
244 0xr 
 |-  0 e. RR*
245 pnfxr 
 |-  +oo e. RR*
246 0ltpnf 
 |-  0 < +oo
247 snunioo 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
248 244 245 246 247 mp3an 
 |-  ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
249 248 imaeq2i 
 |-  ( `' ( Re o. F ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( Re o. F ) " ( 0 [,) +oo ) )
250 imaundi 
 |-  ( `' ( Re o. F ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( Re o. F ) " { 0 } ) u. ( `' ( Re o. F ) " ( 0 (,) +oo ) ) )
251 249 250 eqtr3i 
 |-  ( `' ( Re o. F ) " ( 0 [,) +oo ) ) = ( ( `' ( Re o. F ) " { 0 } ) u. ( `' ( Re o. F ) " ( 0 (,) +oo ) ) )
252 ismbfcn 
 |-  ( F : D --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
253 8 252 syl 
 |-  ( ph -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
254 47 253 mpbid 
 |-  ( ph -> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) )
255 254 simpld 
 |-  ( ph -> ( Re o. F ) e. MblFn )
256 mbfimasn 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : D --> RR /\ 0 e. RR ) -> ( `' ( Re o. F ) " { 0 } ) e. dom vol )
257 91 256 mp3an3 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : D --> RR ) -> ( `' ( Re o. F ) " { 0 } ) e. dom vol )
258 mbfima 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : D --> RR ) -> ( `' ( Re o. F ) " ( 0 (,) +oo ) ) e. dom vol )
259 unmbl 
 |-  ( ( ( `' ( Re o. F ) " { 0 } ) e. dom vol /\ ( `' ( Re o. F ) " ( 0 (,) +oo ) ) e. dom vol ) -> ( ( `' ( Re o. F ) " { 0 } ) u. ( `' ( Re o. F ) " ( 0 (,) +oo ) ) ) e. dom vol )
260 257 258 259 syl2anc 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : D --> RR ) -> ( ( `' ( Re o. F ) " { 0 } ) u. ( `' ( Re o. F ) " ( 0 (,) +oo ) ) ) e. dom vol )
261 255 196 260 syl2anc 
 |-  ( ph -> ( ( `' ( Re o. F ) " { 0 } ) u. ( `' ( Re o. F ) " ( 0 (,) +oo ) ) ) e. dom vol )
262 251 261 eqeltrid 
 |-  ( ph -> ( `' ( Re o. F ) " ( 0 [,) +oo ) ) e. dom vol )
263 8 fdmd 
 |-  ( ph -> dom F = D )
264 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
265 47 264 syl 
 |-  ( ph -> dom F e. dom vol )
266 263 265 eqeltrrd 
 |-  ( ph -> D e. dom vol )
267 difmbl 
 |-  ( ( RR e. dom vol /\ D e. dom vol ) -> ( RR \ D ) e. dom vol )
268 17 266 267 sylancr 
 |-  ( ph -> ( RR \ D ) e. dom vol )
269 unmbl 
 |-  ( ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) e. dom vol /\ ( RR \ D ) e. dom vol ) -> ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol )
270 262 268 269 syl2anc 
 |-  ( ph -> ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol )
271 fveq2 
 |-  ( t = x -> ( g ` t ) = ( g ` x ) )
272 271 breq2d 
 |-  ( t = x -> ( 0 <_ ( g ` t ) <-> 0 <_ ( g ` x ) ) )
273 272 271 ifbieq1d 
 |-  ( t = x -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) = if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
274 273 89 179 fvmpt 
 |-  ( x e. RR -> ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ` x ) = if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
275 274 eqcomd 
 |-  ( x e. RR -> if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) = ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ` x ) )
276 275 ifeq1d 
 |-  ( x e. RR -> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) = if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ` x ) , 0 ) )
277 276 mpteq2ia 
 |-  ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ` x ) , 0 ) )
278 277 i1fres 
 |-  ( ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 /\ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) e. dom S.1 )
279 id 
 |-  ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 )
280 neg1rr 
 |-  -u 1 e. RR
281 280 a1i 
 |-  ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 -> -u 1 e. RR )
282 279 281 i1fmulc 
 |-  ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. dom S.1 )
283 cmmbl 
 |-  ( ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol -> ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) e. dom vol )
284 ifnot 
 |-  if ( -. x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) , 0 ) = if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
285 eldif 
 |-  ( x e. ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) <-> ( x e. RR /\ -. x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) )
286 285 baibr 
 |-  ( x e. RR -> ( -. x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) <-> x e. ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) ) )
287 tru 
 |-  T.
288 negex 
 |-  -u 1 e. _V
289 288 fconst 
 |-  ( RR X. { -u 1 } ) : RR --> { -u 1 }
290 ffn 
 |-  ( ( RR X. { -u 1 } ) : RR --> { -u 1 } -> ( RR X. { -u 1 } ) Fn RR )
291 289 290 mp1i 
 |-  ( T. -> ( RR X. { -u 1 } ) Fn RR )
292 102 a1i 
 |-  ( T. -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) Fn RR )
293 105 a1i 
 |-  ( T. -> RR e. _V )
294 inidm 
 |-  ( RR i^i RR ) = RR
295 288 fvconst2 
 |-  ( x e. RR -> ( ( RR X. { -u 1 } ) ` x ) = -u 1 )
296 295 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( ( RR X. { -u 1 } ) ` x ) = -u 1 )
297 274 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ` x ) = if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) )
298 291 292 293 293 294 296 297 ofval 
 |-  ( ( T. /\ x e. RR ) -> ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) = ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
299 287 298 mpan 
 |-  ( x e. RR -> ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) = ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) )
300 299 eqcomd 
 |-  ( x e. RR -> ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) = ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) )
301 286 300 ifbieq1d 
 |-  ( x e. RR -> if ( -. x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) , 0 ) = if ( x e. ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) , ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) , 0 ) )
302 284 301 eqtr3id 
 |-  ( x e. RR -> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) = if ( x e. ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) , ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) , 0 ) )
303 302 mpteq2ia 
 |-  ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) = ( x e. RR |-> if ( x e. ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) , ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ` x ) , 0 ) )
304 303 i1fres 
 |-  ( ( ( ( RR X. { -u 1 } ) oF x. ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. dom S.1 /\ ( RR \ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) e. dom S.1 )
305 282 283 304 syl2an 
 |-  ( ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 /\ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) e. dom S.1 )
306 278 305 i1fadd 
 |-  ( ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. dom S.1 /\ ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) e. dom vol ) -> ( ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) oF + ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) e. dom S.1 )
307 90 270 306 syl2anr 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , 0 ) ) oF + ( x e. RR |-> if ( x e. ( ( `' ( Re o. F ) " ( 0 [,) +oo ) ) u. ( RR \ D ) ) , 0 , ( -u 1 x. if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ) ) e. dom S.1 )
308 243 307 eqeltrrd 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. dom S.1 )
309 159 cbvmptv 
 |-  ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) = ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
310 309 36 eqeltrid 
 |-  ( ph -> ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 )
311 16 309 fmptd 
 |-  ( ph -> ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR )
312 310 311 jca 
 |-  ( ph -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) )
313 312 adantr 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) )
314 ftc1anclem4 
 |-  ( ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. dom S.1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) ) ) e. RR )
315 314 3expb 
 |-  ( ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. dom S.1 /\ ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) ) ) e. RR )
316 308 313 315 syl2anc 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) ) ) ) ) e. RR )
317 176 316 eqeltrrid 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) e. RR )
318 139 143 144 155 317 itg2addnc 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) oF + ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) )
319 105 a1i 
 |-  ( ( ph /\ g e. dom S.1 ) -> RR e. _V )
320 101 a1i 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. _V )
321 eqidd 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
322 eqidd 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) )
323 319 320 151 321 322 offval2 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) oF + ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) = ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) )
324 323 fveq2d 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) oF + ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) )
325 318 324 eqtr3d 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) )
326 325 adantr 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) )
327 nfv 
 |-  F/ t ( ph /\ g e. dom S.1 )
328 nfcv 
 |-  F/_ t g
329 nfcv 
 |-  F/_ t oR <_
330 nfmpt1 
 |-  F/_ t ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
331 328 329 330 nfbr 
 |-  F/ t g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
332 327 331 nfan 
 |-  F/ t ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
333 anass 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) <-> ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) )
334 92 ffnd 
 |-  ( g e. dom S.1 -> g Fn RR )
335 fvex 
 |-  ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. _V
336 eqid 
 |-  ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) = ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
337 335 336 fnmpti 
 |-  ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) Fn RR
338 337 a1i 
 |-  ( g e. dom S.1 -> ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) Fn RR )
339 eqidd 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) = ( g ` t ) )
340 336 fvmpt2 
 |-  ( ( t e. RR /\ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. _V ) -> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ` t ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
341 335 340 mpan2 
 |-  ( t e. RR -> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ` t ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
342 341 adantl 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ` t ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
343 334 338 106 106 294 339 342 ofrval 
 |-  ( ( g e. dom S.1 /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ t e. RR ) -> ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
344 343 3com23 
 |-  ( ( g e. dom S.1 /\ t e. RR /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
345 344 3expa 
 |-  ( ( ( g e. dom S.1 /\ t e. RR ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
346 345 adantll 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
347 resubcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
348 15 109 347 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
349 348 ad2antrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
350 absid 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
351 15 350 sylan 
 |-  ( ( ph /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
352 351 breq2d 
 |-  ( ( ph /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) <-> ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
353 352 biimpa 
 |-  ( ( ( ph /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
354 353 an32s 
 |-  ( ( ( ph /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
355 354 adantllr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
356 breq1 
 |-  ( ( g ` t ) = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> ( ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
357 breq1 
 |-  ( 0 = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
358 356 357 ifboth 
 |-  ( ( ( g ` t ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
359 355 358 sylancom 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
360 subge0 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR ) -> ( 0 <_ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
361 15 109 360 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( 0 <_ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
362 361 ad2antrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( 0 <_ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
363 359 362 mpbird 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> 0 <_ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
364 349 363 absidd 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
365 iftrue 
 |-  ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
366 365 oveq2d 
 |-  ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
367 366 fveq2d 
 |-  ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
368 367 adantl 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
369 15 ad2antrr 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
370 350 oveq1d 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
371 369 370 sylan 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
372 364 368 371 3eqtr4d 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
373 109 renegcld 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR )
374 resubcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
375 15 373 374 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
376 375 ad2antrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) e. RR )
377 93 ad3antlr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( g ` t ) e. RR )
378 15 ad3antrrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
379 15 adantr 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
380 ltnle 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ 0 e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 <-> -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
381 91 380 mpan2 
 |-  ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 <-> -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
382 ltle 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ 0 e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) )
383 91 382 mpan2 
 |-  ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) )
384 381 383 sylbird 
 |-  ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR -> ( -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) )
385 384 imp 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 )
386 absnid 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
387 385 386 syldan 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
388 387 breq2d 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) <-> ( g ` t ) <_ -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
389 388 biimpa 
 |-  ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( g ` t ) <_ -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
390 389 an32s 
 |-  ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( g ` t ) <_ -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
391 379 390 sylanl1 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( g ` t ) <_ -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
392 377 378 391 lenegcon2d 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u ( g ` t ) )
393 simpll 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ph )
394 91 a1i 
 |-  ( ph -> 0 e. RR )
395 15 394 ltnled 
 |-  ( ph -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 <-> -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
396 15 91 382 sylancl 
 |-  ( ph -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < 0 -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) )
397 395 396 sylbird 
 |-  ( ph -> ( -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) )
398 397 imp 
 |-  ( ( ph /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 )
399 393 398 sylan 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 )
400 negeq 
 |-  ( ( g ` t ) = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> -u ( g ` t ) = -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
401 400 breq2d 
 |-  ( ( g ` t ) = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u ( g ` t ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
402 neg0 
 |-  -u 0 = 0
403 negeq 
 |-  ( 0 = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> -u 0 = -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
404 402 403 eqtr3id 
 |-  ( 0 = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> 0 = -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
405 404 breq2d 
 |-  ( 0 = if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
406 401 405 ifboth 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u ( g ` t ) /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
407 392 399 406 syl2anc 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
408 suble0 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <_ 0 <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
409 15 373 408 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <_ 0 <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
410 409 ad2antrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <_ 0 <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
411 407 410 mpbird 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) <_ 0 )
412 376 411 absnidd 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
413 subneg 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
414 413 negeqd 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC ) -> -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
415 negdi2 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC ) -> -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
416 414 415 eqtrd 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC ) -> -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
417 37 145 416 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
418 417 ad2antrr 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> -u ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
419 412 418 eqtrd 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
420 iffalse 
 |-  ( -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) )
421 420 oveq2d 
 |-  ( -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
422 421 fveq2d 
 |-  ( -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
423 422 adantl 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
424 15 386 sylan 
 |-  ( ( ph /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <_ 0 ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
425 398 424 syldan 
 |-  ( ( ph /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
426 425 oveq1d 
 |-  ( ( ph /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
427 393 426 sylan 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) = ( -u ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
428 419 423 427 3eqtr4d 
 |-  ( ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
429 372 428 pm2.61dan 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) = ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
430 429 oveq2d 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
431 58 recnd 
 |-  ( ph -> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC )
432 pncan3 
 |-  ( ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) e. CC /\ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
433 145 431 432 syl2anr 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
434 433 adantr 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) - if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
435 430 434 eqtrd 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ ( g ` t ) <_ ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
436 346 435 syldan 
 |-  ( ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
437 333 436 sylanb 
 |-  ( ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
438 437 an32s 
 |-  ( ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) /\ t e. RR ) -> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) = ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) )
439 332 438 mpteq2da 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) = ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
440 439 fveq2d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( S.2 ` ( t e. RR |-> ( if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) + ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) )
441 326 440 eqtrd 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) )
442 441 breq1d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
443 442 adantllr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
444 317 adantlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) e. RR )
445 68 ad2antlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> Y e. RR )
446 120 adantl 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR )
447 444 445 446 ltadd2d 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y <-> ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
448 447 adantr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y <-> ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
449 ltsubadd 
 |-  ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) e. RR /\ Y e. RR /\ ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) e. RR ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
450 65 68 120 449 syl3an 
 |-  ( ( ph /\ Y e. RR+ /\ g e. dom S.1 ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
451 450 3expa 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
452 451 adantr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) < ( ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) + Y ) ) )
453 443 448 452 3bitr4d 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y <-> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
454 453 adantrr 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y <-> ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) < ( S.2 ` ( t e. RR |-> if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
455 136 454 mpbird 
 |-  ( ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) /\ ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y )
456 455 ex 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ g e. dom S.1 ) -> ( ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y ) )
457 456 reximdva 
 |-  ( ( ph /\ Y e. RR+ ) -> ( E. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y ) )
458 fveq1 
 |-  ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) -> ( f ` t ) = ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) ` t ) )
459 458 172 sylan9eq 
 |-  ( ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) /\ t e. RR ) -> ( f ` t ) = if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) )
460 459 oveq2d 
 |-  ( ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) /\ t e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) )
461 460 fveq2d 
 |-  ( ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) )
462 461 mpteq2dva 
 |-  ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) )
463 462 fveq2d 
 |-  ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) )
464 463 breq1d 
 |-  ( f = ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y <-> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y ) )
465 464 rspcev 
 |-  ( ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. dom S.1 /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y ) -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y )
466 465 ex 
 |-  ( ( x e. RR |-> if ( 0 <_ ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) , if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) , -u if ( 0 <_ ( g ` x ) , ( g ` x ) , 0 ) ) ) e. dom S.1 -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y ) )
467 308 466 syl 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y ) )
468 467 rexlimdva 
 |-  ( ph -> ( E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y ) )
469 468 adantr 
 |-  ( ( ph /\ Y e. RR+ ) -> ( E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - if ( 0 <_ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) , if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) , -u if ( 0 <_ ( g ` t ) , ( g ` t ) , 0 ) ) ) ) ) ) < Y -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y ) )
470 457 469 syld 
 |-  ( ( ph /\ Y e. RR+ ) -> ( E. g e. dom S.1 ( g oR <_ ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) /\ -. ( S.1 ` g ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) ) - Y ) ) -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y ) )
471 85 470 mpd 
 |-  ( ( ph /\ Y e. RR+ ) -> E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < Y )