Theorem ftc1anclem7

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 13-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	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 ) ) )

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