Theorem ftc1anclem8

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