Theorem ftc1anc

Description: ftc1a holds for functions that obey the triangle inequality in the absence of ax-cc . Theorem 565Ma of Fremlin5 p. 220. (Contributed by Brendan Leahy, 11-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 )
	ftc1anc.t	|- ( ph -> A. s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ( abs ` S. s ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) ) )
Assertion	ftc1anc	|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

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		ftc1anc.t	|- ( ph -> A. s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ( abs ` S. s ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) ) )
10	1 2 3 4 5 6 7 8	ftc1lem2	|- ( ph -> G : ( A [,] B ) --> CC )
11		rphalfcl	|- ( y e. RR+ -> ( y / 2 ) e. RR+ )
12	1 2 3 4 5 6 7 8	ftc1anclem6	|- ( ( ph /\ ( y / 2 ) e. RR+ ) -> E. f e. dom S.1 E. 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 ) )
13	11 12	sylan2	|- ( ( ph /\ y e. RR+ ) -> E. f e. dom S.1 E. 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 ) )
14	13	adantrl	|- ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) -> E. f e. dom S.1 E. 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 ) )
15	11	ad2antll	|- ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) -> ( y / 2 ) e. RR+ )
16		2rp	|- 2 e. RR+
17		i1ff	|- ( f e. dom S.1 -> f : RR --> RR )
18	17	frnd	|- ( f e. dom S.1 -> ran f C_ RR )
19	18	adantr	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ran f C_ RR )
20		i1ff	|- ( g e. dom S.1 -> g : RR --> RR )
21	20	frnd	|- ( g e. dom S.1 -> ran g C_ RR )
22	21	adantl	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ran g C_ RR )
23	19 22	unssd	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) C_ RR )
24		ax-resscn	|- RR C_ CC
25	23 24	sstrdi	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) C_ CC )
26		i1f0rn	|- ( f e. dom S.1 -> 0 e. ran f )
27		elun1	|- ( 0 e. ran f -> 0 e. ( ran f u. ran g ) )
28	26 27	syl	|- ( f e. dom S.1 -> 0 e. ( ran f u. ran g ) )
29	28	adantr	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> 0 e. ( ran f u. ran g ) )
30		absf	|- abs : CC --> RR
31		ffn	|- ( abs : CC --> RR -> abs Fn CC )
32	30 31	ax-mp	|- abs Fn CC
33		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 ) ) )
34	32 33	mp3an1	|- ( ( ( ran f u. ran g ) C_ CC /\ 0 e. ( ran f u. ran g ) ) -> ( abs ` 0 ) e. ( abs " ( ran f u. ran g ) ) )
35	25 29 34	syl2anc	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs ` 0 ) e. ( abs " ( ran f u. ran g ) ) )
36	35	ne0d	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) =/= (/) )
37		imassrn	|- ( abs " ( ran f u. ran g ) ) C_ ran abs
38		frn	|- ( abs : CC --> RR -> ran abs C_ RR )
39	30 38	ax-mp	|- ran abs C_ RR
40	37 39	sstri	|- ( abs " ( ran f u. ran g ) ) C_ RR
41		ffun	|- ( abs : CC --> RR -> Fun abs )
42	30 41	ax-mp	|- Fun abs
43		i1frn	|- ( f e. dom S.1 -> ran f e. Fin )
44		i1frn	|- ( g e. dom S.1 -> ran g e. Fin )
45		unfi	|- ( ( ran f e. Fin /\ ran g e. Fin ) -> ( ran f u. ran g ) e. Fin )
46	43 44 45	syl2an	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) e. Fin )
47		imafi	|- ( ( Fun abs /\ ( ran f u. ran g ) e. Fin ) -> ( abs " ( ran f u. ran g ) ) e. Fin )
48	42 46 47	sylancr	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) e. Fin )
49		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 )
50	40 48 49	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 )
51		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 )
52	40 51	mp3an1	|- ( ( ( 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 )
53	36 50 52	syl2anc	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) e. RR )
54	53	adantr	|- ( ( ( 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 )
55		0red	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> 0 e. RR )
56	25	sselda	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> r e. CC )
57	56	abscld	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( abs ` r ) e. RR )
58	57	adantrr	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> ( abs ` r ) e. RR )
59	53	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 )
60		absgt0	|- ( r e. CC -> ( r =/= 0 <-> 0 < ( abs ` r ) ) )
61	56 60	syl	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( r =/= 0 <-> 0 < ( abs ` r ) ) )
62	61	biimpd	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( r =/= 0 -> 0 < ( abs ` r ) ) )
63	62	impr	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> 0 < ( abs ` r ) )
64	40	a1i	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) C_ RR )
65	64 36 50	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 ) )
66	65	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 ) )
67		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 ) ) )
68	32 67	mp3an1	|- ( ( ( ran f u. ran g ) C_ CC /\ r e. ( ran f u. ran g ) ) -> ( abs ` r ) e. ( abs " ( ran f u. ran g ) ) )
69	25 68	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 ) ) )
70		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 , < ) )
71	66 69 70	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 , < ) )
72	71	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 , < ) )
73	55 58 59 63 72	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 , < ) )
74	73	rexlimdvaa	|- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( E. r e. ( ran f u. ran g ) r =/= 0 -> 0 < sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) )
75	74	imp	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ E. r e. ( ran f u. ran g ) r =/= 0 ) -> 0 < sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) )
76	54 75	elrpd	|- ( ( ( 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+ )
77		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+ )
78	16 76 77	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+ )
79		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+ )
80	15 78 79	syl2an	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ E. r e. ( ran f u. ran g ) r =/= 0 ) ) -> ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) e. RR+ )
81	80	anassrs	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ E. r e. ( ran f u. ran g ) r =/= 0 ) -> ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) e. RR+ )
82	81	adantlr	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) e. RR+ )
83		ancom	|- ( ( u e. ( A [,] B ) /\ y e. RR+ ) <-> ( y e. RR+ /\ u e. ( A [,] B ) ) )
84	83	anbi2i	|- ( ( ( ( ( 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 ) /\ y e. RR+ ) ) <-> ( ( ( ( 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 ) ) ) )
85		an32	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) <-> ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) )
86	85	anbi1i	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) ) <-> ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < ( y / 2 ) ) )
87		an32	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < ( y / 2 ) ) <-> ( ( ( 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 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) )
88	86 87	bitri	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) ) <-> ( ( ( 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 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) )
89	88	anbi1i	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) <-> ( ( ( ( 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 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ E. r e. ( ran f u. ran g ) r =/= 0 ) )
90		an32	|- ( ( ( ( ( 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 ) ) /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ E. r e. ( ran f u. ran g ) r =/= 0 ) <-> ( ( ( ( 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 ) /\ y e. RR+ ) ) )
91	89 90	bitri	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) <-> ( ( ( ( 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 ) /\ y e. RR+ ) ) )
92		anass	|- ( ( ( ( ( ( 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 ) ) <-> ( ( ( ( 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 ) ) ) )
93	84 91 92	3bitr4i	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) <-> ( ( ( ( ( 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 ) ) )
94		oveq12	|- ( ( b = w /\ a = u ) -> ( b - a ) = ( w - u ) )
95	94	ancoms	|- ( ( a = u /\ b = w ) -> ( b - a ) = ( w - u ) )
96	95	fveq2d	|- ( ( a = u /\ b = w ) -> ( abs ` ( b - a ) ) = ( abs ` ( w - u ) ) )
97	96	breq1d	|- ( ( a = u /\ b = w ) -> ( ( abs ` ( b - a ) ) < ( ( 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 , < ) ) ) ) )
98		fveq2	|- ( b = w -> ( G ` b ) = ( G ` w ) )
99		fveq2	|- ( a = u -> ( G ` a ) = ( G ` u ) )
100	98 99	oveqan12rd	|- ( ( a = u /\ b = w ) -> ( ( G ` b ) - ( G ` a ) ) = ( ( G ` w ) - ( G ` u ) ) )
101	100	fveq2d	|- ( ( a = u /\ b = w ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) = ( abs ` ( ( G ` w ) - ( G ` u ) ) ) )
102	101	breq1d	|- ( ( a = u /\ b = w ) -> ( ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y <-> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
103	97 102	imbi12d	|- ( ( a = u /\ b = w ) -> ( ( ( abs ` ( b - a ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y ) <-> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) )
104		oveq12	|- ( ( b = u /\ a = w ) -> ( b - a ) = ( u - w ) )
105	104	ancoms	|- ( ( a = w /\ b = u ) -> ( b - a ) = ( u - w ) )
106	105	fveq2d	|- ( ( a = w /\ b = u ) -> ( abs ` ( b - a ) ) = ( abs ` ( u - w ) ) )
107	106	breq1d	|- ( ( a = w /\ b = u ) -> ( ( abs ` ( b - a ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) <-> ( abs ` ( u - w ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) ) )
108		fveq2	|- ( b = u -> ( G ` b ) = ( G ` u ) )
109		fveq2	|- ( a = w -> ( G ` a ) = ( G ` w ) )
110	108 109	oveqan12rd	|- ( ( a = w /\ b = u ) -> ( ( G ` b ) - ( G ` a ) ) = ( ( G ` u ) - ( G ` w ) ) )
111	110	fveq2d	|- ( ( a = w /\ b = u ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
112	111	breq1d	|- ( ( a = w /\ b = u ) -> ( ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) )
113	107 112	imbi12d	|- ( ( a = w /\ b = u ) -> ( ( ( abs ` ( b - a ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y ) <-> ( ( abs ` ( u - w ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) ) )
114		iccssre	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
115	2 3 114	syl2anc	|- ( ph -> ( A [,] B ) C_ RR )
116	115	ad4antr	|- ( ( ( ( ( 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+ ) -> ( A [,] B ) C_ RR )
117		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 )
118	115 24	sstrdi	|- ( ph -> ( A [,] B ) C_ CC )
119	118	sselda	|- ( ( ph /\ w e. ( A [,] B ) ) -> w e. CC )
120	118	sselda	|- ( ( ph /\ u e. ( A [,] B ) ) -> u e. CC )
121		abssub	|- ( ( w e. CC /\ u e. CC ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
122	119 120 121	syl2anr	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
123	122	anandis	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
124	123	breq1d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) <-> ( abs ` ( u - w ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) ) )
125	10	ffvelrnda	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( G ` w ) e. CC )
126	10	ffvelrnda	|- ( ( ph /\ u e. ( A [,] B ) ) -> ( G ` u ) e. CC )
127		abssub	|- ( ( ( G ` w ) e. CC /\ ( G ` u ) e. CC ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
128	125 126 127	syl2anr	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
129	128	anandis	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
130	129	breq1d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) )
131	124 130	imbi12d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) <-> ( ( abs ` ( u - w ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) ) )
132	117 131	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 ) ) ) -> ( ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) <-> ( ( abs ` ( u - w ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) ) )
133	2	rexrd	|- ( ph -> A e. RR* )
134	3	rexrd	|- ( ph -> B e. RR* )
135	133 134	jca	|- ( ph -> ( A e. RR* /\ B e. RR* ) )
136		df-icc	|- [,] = ( x e. RR* , y e. RR* |-> { t e. RR* | ( x <_ t /\ t <_ y ) } )
137	136	elixx3g	|- ( u e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ u e. RR* ) /\ ( A <_ u /\ u <_ B ) ) )
138	137	simprbi	|- ( u e. ( A [,] B ) -> ( A <_ u /\ u <_ B ) )
139	138	simpld	|- ( u e. ( A [,] B ) -> A <_ u )
140	136	elixx3g	|- ( w e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) /\ ( A <_ w /\ w <_ B ) ) )
141	140	simprbi	|- ( w e. ( A [,] B ) -> ( A <_ w /\ w <_ B ) )
142	141	simprd	|- ( w e. ( A [,] B ) -> w <_ B )
143	139 142	anim12i	|- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( A <_ u /\ w <_ B ) )
144		ioossioo	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ u /\ w <_ B ) ) -> ( u (,) w ) C_ ( A (,) B ) )
145	135 143 144	syl2an	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) C_ ( A (,) B ) )
146	5	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( A (,) B ) C_ D )
147	145 146	sstrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) C_ D )
148	147	sselda	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> t e. D )
149	8	ffvelrnda	|- ( ( ph /\ t e. D ) -> ( F ` t ) e. CC )
150	149	abscld	|- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. RR )
151	150	rexrd	|- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. RR* )
152	149	absge0d	|- ( ( ph /\ t e. D ) -> 0 <_ ( abs ` ( F ` t ) ) )
153		elxrge0	|- ( ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( F ` t ) ) e. RR* /\ 0 <_ ( abs ` ( F ` t ) ) ) )
154	151 152 153	sylanbrc	|- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
155	154	adantlr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
156	148 155	syldan	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
157		0e0iccpnf	|- 0 e. ( 0 [,] +oo )
158	157	a1i	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. ( u (,) w ) ) -> 0 e. ( 0 [,] +oo ) )
159	156 158	ifclda	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
160	159	adantr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. RR ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
161	160	fmpttd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
162		itg2cl	|- ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
163	161 162	syl	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
164	163	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
165	117 164	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 ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
166	165	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 ) ) , 0 ) ) ) e. RR* )
167		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 ) ) )
168	149	adantlr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( F ` t ) e. CC )
169	148 168	syldan	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( F ` t ) e. CC )
170	169	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 )
171		elioore	|- ( t e. ( u (,) w ) -> t e. RR )
172	17	ffvelrnda	|- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. RR )
173	172	recnd	|- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. CC )
174		ax-icn	|- _i e. CC
175	20	ffvelrnda	|- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. RR )
176	175	recnd	|- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. CC )
177		mulcl	|- ( ( _i e. CC /\ ( g ` t ) e. CC ) -> ( _i x. ( g ` t ) ) e. CC )
178	174 176 177	sylancr	|- ( ( g e. dom S.1 /\ t e. RR ) -> ( _i x. ( g ` t ) ) e. CC )
179		addcl	|- ( ( ( f ` t ) e. CC /\ ( _i x. ( g ` t ) ) e. CC ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
180	173 178 179	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 )
181	180	anandirs	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
182	171 181	sylan2	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
183	182	adantll	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
184	183	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 )
185	170 184	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 )
186	185	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 )
187	182	abscld	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) e. RR )
188	187	adantll	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) e. RR )
189	188	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 ) ) ) ) e. RR )
190	186 189	readdcld	|- ( ( ( ( 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 ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. RR )
191	190	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. RR* )
192	185	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 ) ) ) ) ) )
193	181	absge0d	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
194	171 193	sylan2	|- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
195	194	adantll	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
196	195	adantlr	|- ( ( ( ( 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 ) + ( _i x. ( g ` t ) ) ) ) )
197	186 189 192 196	addge0d	|- ( ( ( ( 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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
198		elxrge0	|- ( ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. ( 0 [,] +oo ) <-> ( ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. RR* /\ 0 <_ ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) )
199	191 197 198	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. ( 0 [,] +oo ) )
200	157	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 ) )
201	199 200	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) e. ( 0 [,] +oo ) )
202	201	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) e. ( 0 [,] +oo ) )
203	202	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
204		itg2cl	|- ( ( 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 ) ) : RR --> ( 0 [,] +oo ) -> ( 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 ) ) ) e. RR* )
205	203 204	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) ) e. RR* )
206	205	3adantr3	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( 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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) ) e. RR* )
207	167 206	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 ) ) -> ( 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 ) ) ) e. RR* )
208	207	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 ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) ) e. RR* )
209		rpxr	|- ( y e. RR+ -> y e. RR* )
210	209	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 e. RR* )
211	159	adantlr	|- ( ( ( 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 ) ) , 0 ) e. ( 0 [,] +oo ) )
212	211	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 ) ) , 0 ) e. ( 0 [,] +oo ) )
213	212	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 ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
214	170 184	npcand	|- ( ( ( ( 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 ) ) ) ) + ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( F ` t ) )
215	214	fveq2d	|- ( ( ( ( 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 ) ) ) ) + ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) = ( abs ` ( F ` t ) ) )
216	185 184	abstrid	|- ( ( ( ( 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 ) ) ) ) + ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) <_ ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
217	215 216	eqbrtrrd	|- ( ( ( ( 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 ) ) <_ ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
218		iftrue	|- ( t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) = ( abs ` ( F ` t ) ) )
219	218	adantl	|- ( ( ( ( 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. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) = ( abs ` ( F ` t ) ) )
220		iftrue	|- ( t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) = ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
221	220	adantl	|- ( ( ( ( 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. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) = ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
222	217 219 221	3brtr4d	|- ( ( ( ( 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. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) )
223	222	ex	|- ( ( ( 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. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) )
224		0le0	|- 0 <_ 0
225	224	a1i	|- ( -. t e. ( u (,) w ) -> 0 <_ 0 )
226		iffalse	|- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) = 0 )
227		iffalse	|- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) = 0 )
228	225 226 227	3brtr4d	|- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) )
229	223 228	pm2.61d1	|- ( ( ( 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 ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) )
230	229	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 ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) )
231		reex	|- RR e. _V
232	231	a1i	|- ( ph -> RR e. _V )
233		fvex	|- ( abs ` ( F ` t ) ) e. _V
234		c0ex	|- 0 e. _V
235	233 234	ifex	|- if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. _V
236	235	a1i	|- ( ( ph /\ t e. RR ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. _V )
237		ovex	|- ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. _V
238	237 234	ifex	|- if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) e. _V
239	238	a1i	|- ( ( ph /\ 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 ) e. _V )
240		eqidd	|- ( ph -> ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) )
241		eqidd	|- ( ph -> ( 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 ) ) = ( 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 ) ) )
242	232 236 239 240 241	ofrfval2	|- ( ph -> ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( 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 ) ) <-> A. t e. RR if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) )
243	242	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 ) ) , 0 ) ) oR <_ ( 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 ) ) <-> A. t e. RR if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) ) )
244	230 243	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 ) ) , 0 ) ) oR <_ ( 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 ) ) )
245		itg2le	|- ( ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( 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 ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( 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 ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` 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 ) ) ) )
246	213 203 244 245	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 ) ) , 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 ) ) ) )
247	246	3adantr3	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` 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 ) ) ) )
248	167 247	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 ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` 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 ) ) ) )
249	248	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 ) ) , 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 ) ) ) )
250	1 2 3 4 5 6 7 8	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 )
251	166 208 210 249 250	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 ) ) /\ 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 ) ) , 0 ) ) ) < y )
252		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 ) -> ph )
253		simpr2	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> w e. ( A [,] B ) )
254		oveq2	|- ( x = w -> ( A (,) x ) = ( A (,) w ) )
255		itgeq1	|- ( ( A (,) x ) = ( A (,) w ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) w ) ( F ` t ) _d t )
256	254 255	syl	|- ( x = w -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) w ) ( F ` t ) _d t )
257		itgex	|- S. ( A (,) w ) ( F ` t ) _d t e. _V
258	256 1 257	fvmpt	|- ( w e. ( A [,] B ) -> ( G ` w ) = S. ( A (,) w ) ( F ` t ) _d t )
259	253 258	syl	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( G ` w ) = S. ( A (,) w ) ( F ` t ) _d t )
260	2	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> A e. RR )
261	115	sselda	|- ( ( ph /\ w e. ( A [,] B ) ) -> w e. RR )
262	261	3ad2antr2	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> w e. RR )
263	115	sselda	|- ( ( ph /\ u e. ( A [,] B ) ) -> u e. RR )
264	263	rexrd	|- ( ( ph /\ u e. ( A [,] B ) ) -> u e. RR* )
265	264	3ad2antr1	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. RR* )
266		elicc1	|- ( ( A e. RR* /\ B e. RR* ) -> ( u e. ( A [,] B ) <-> ( u e. RR* /\ A <_ u /\ u <_ B ) ) )
267	133 134 266	syl2anc	|- ( ph -> ( u e. ( A [,] B ) <-> ( u e. RR* /\ A <_ u /\ u <_ B ) ) )
268	267	biimpa	|- ( ( ph /\ u e. ( A [,] B ) ) -> ( u e. RR* /\ A <_ u /\ u <_ B ) )
269	268	simp2d	|- ( ( ph /\ u e. ( A [,] B ) ) -> A <_ u )
270	269	3ad2antr1	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> A <_ u )
271		simpr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u <_ w )
272	133	adantr	|- ( ( ph /\ w e. ( A [,] B ) ) -> A e. RR* )
273	261	rexrd	|- ( ( ph /\ w e. ( A [,] B ) ) -> w e. RR* )
274		elicc1	|- ( ( A e. RR* /\ w e. RR* ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
275	272 273 274	syl2anc	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
276	275	3ad2antr2	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
277	265 270 271 276	mpbir3and	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. ( A [,] w ) )
278		iooss2	|- ( ( B e. RR* /\ w <_ B ) -> ( A (,) w ) C_ ( A (,) B ) )
279	134 142 278	syl2an	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) C_ ( A (,) B ) )
280	5	adantr	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) B ) C_ D )
281	279 280	sstrd	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) C_ D )
282	281	3ad2antr2	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( A (,) w ) C_ D )
283	282	sselda	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. ( A (,) w ) ) -> t e. D )
284	149	adantlr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. D ) -> ( F ` t ) e. CC )
285	283 284	syldan	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. ( A (,) w ) ) -> ( F ` t ) e. CC )
286		eleq1w	|- ( w = u -> ( w e. ( A [,] B ) <-> u e. ( A [,] B ) ) )
287	286	anbi2d	|- ( w = u -> ( ( ph /\ w e. ( A [,] B ) ) <-> ( ph /\ u e. ( A [,] B ) ) ) )
288		oveq2	|- ( w = u -> ( A (,) w ) = ( A (,) u ) )
289	288	mpteq1d	|- ( w = u -> ( t e. ( A (,) w ) |-> ( F ` t ) ) = ( t e. ( A (,) u ) |-> ( F ` t ) ) )
290	289	eleq1d	|- ( w = u -> ( ( t e. ( A (,) w ) |-> ( F ` t ) ) e. L^1 <-> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 ) )
291	287 290	imbi12d	|- ( w = u -> ( ( ( ph /\ w e. ( A [,] B ) ) -> ( t e. ( A (,) w ) |-> ( F ` t ) ) e. L^1 ) <-> ( ( ph /\ u e. ( A [,] B ) ) -> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 ) ) )
292		ioombl	|- ( A (,) w ) e. dom vol
293	292	a1i	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) e. dom vol )
294	149	adantlr	|- ( ( ( ph /\ w e. ( A [,] B ) ) /\ t e. D ) -> ( F ` t ) e. CC )
295	8	feqmptd	|- ( ph -> F = ( t e. D |-> ( F ` t ) ) )
296	295 7	eqeltrrd	|- ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
297	296	adantr	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
298	281 293 294 297	iblss	|- ( ( ph /\ w e. ( A [,] B ) ) -> ( t e. ( A (,) w ) |-> ( F ` t ) ) e. L^1 )
299	291 298	chvarvv	|- ( ( ph /\ u e. ( A [,] B ) ) -> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 )
300	299	3ad2antr1	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 )
301		ioombl	|- ( u (,) w ) e. dom vol
302	301	a1i	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) e. dom vol )
303		fvexd	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( F ` t ) e. _V )
304	296	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
305	147 302 303 304	iblss	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. ( u (,) w ) |-> ( F ` t ) ) e. L^1 )
306	305	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( t e. ( u (,) w ) |-> ( F ` t ) ) e. L^1 )
307	260 262 277 285 300 306	itgsplitioo	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> S. ( A (,) w ) ( F ` t ) _d t = ( S. ( A (,) u ) ( F ` t ) _d t + S. ( u (,) w ) ( F ` t ) _d t ) )
308	259 307	eqtrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( G ` w ) = ( S. ( A (,) u ) ( F ` t ) _d t + S. ( u (,) w ) ( F ` t ) _d t ) )
309		simpr1	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. ( A [,] B ) )
310		oveq2	|- ( x = u -> ( A (,) x ) = ( A (,) u ) )
311		itgeq1	|- ( ( A (,) x ) = ( A (,) u ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) u ) ( F ` t ) _d t )
312	310 311	syl	|- ( x = u -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) u ) ( F ` t ) _d t )
313		itgex	|- S. ( A (,) u ) ( F ` t ) _d t e. _V
314	312 1 313	fvmpt	|- ( u e. ( A [,] B ) -> ( G ` u ) = S. ( A (,) u ) ( F ` t ) _d t )
315	309 314	syl	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( G ` u ) = S. ( A (,) u ) ( F ` t ) _d t )
316	308 315	oveq12d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( ( G ` w ) - ( G ` u ) ) = ( ( S. ( A (,) u ) ( F ` t ) _d t + S. ( u (,) w ) ( F ` t ) _d t ) - S. ( A (,) u ) ( F ` t ) _d t ) )
317		fvexd	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ t e. ( A (,) u ) ) -> ( F ` t ) e. _V )
318	317 299	itgcl	|- ( ( ph /\ u e. ( A [,] B ) ) -> S. ( A (,) u ) ( F ` t ) _d t e. CC )
319	318	adantrr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> S. ( A (,) u ) ( F ` t ) _d t e. CC )
320		fvexd	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( F ` t ) e. _V )
321	320 305	itgcl	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> S. ( u (,) w ) ( F ` t ) _d t e. CC )
322	319 321	pncan2d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( S. ( A (,) u ) ( F ` t ) _d t + S. ( u (,) w ) ( F ` t ) _d t ) - S. ( A (,) u ) ( F ` t ) _d t ) = S. ( u (,) w ) ( F ` t ) _d t )
323	322	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( ( S. ( A (,) u ) ( F ` t ) _d t + S. ( u (,) w ) ( F ` t ) _d t ) - S. ( A (,) u ) ( F ` t ) _d t ) = S. ( u (,) w ) ( F ` t ) _d t )
324	316 323	eqtrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( ( G ` w ) - ( G ` u ) ) = S. ( u (,) w ) ( F ` t ) _d t )
325	324	fveq2d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) )
326		df-ov	|- ( u (,) w ) = ( (,) ` <. u , w >. )
327		opelxpi	|- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> <. u , w >. e. ( ( A [,] B ) X. ( A [,] B ) ) )
328		ioof	|- (,) : ( RR* X. RR* ) --> ~P RR
329		ffn	|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
330	328 329	ax-mp	|- (,) Fn ( RR* X. RR* )
331		iccssxr	|- ( A [,] B ) C_ RR*
332		xpss12	|- ( ( ( A [,] B ) C_ RR* /\ ( A [,] B ) C_ RR* ) -> ( ( A [,] B ) X. ( A [,] B ) ) C_ ( RR* X. RR* ) )
333	331 331 332	mp2an	|- ( ( A [,] B ) X. ( A [,] B ) ) C_ ( RR* X. RR* )
334		fnfvima	|- ( ( (,) Fn ( RR* X. RR* ) /\ ( ( A [,] B ) X. ( A [,] B ) ) C_ ( RR* X. RR* ) /\ <. u , w >. e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( (,) ` <. u , w >. ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
335	330 333 334	mp3an12	|- ( <. u , w >. e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` <. u , w >. ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
336	327 335	syl	|- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( (,) ` <. u , w >. ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
337	326 336	eqeltrid	|- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( u (,) w ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
338		itgeq1	|- ( s = ( u (,) w ) -> S. s ( F ` t ) _d t = S. ( u (,) w ) ( F ` t ) _d t )
339	338	fveq2d	|- ( s = ( u (,) w ) -> ( abs ` S. s ( F ` t ) _d t ) = ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) )
340		eleq2	|- ( s = ( u (,) w ) -> ( t e. s <-> t e. ( u (,) w ) ) )
341	340	ifbid	|- ( s = ( u (,) w ) -> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) = if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) )
342	341	mpteq2dv	|- ( s = ( u (,) w ) -> ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) )
343	342	fveq2d	|- ( s = ( u (,) w ) -> ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
344	339 343	breq12d	|- ( s = ( u (,) w ) -> ( ( abs ` S. s ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) ) <-> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) ) )
345	344	rspccva	|- ( ( A. s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ( abs ` S. s ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) ) ) /\ ( u (,) w ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
346	9 337 345	syl2an	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
347	346	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
348	325 347	eqbrtrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
349	348	adantlr	|- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) )
350		subcl	|- ( ( ( G ` w ) e. CC /\ ( G ` u ) e. CC ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
351	125 126 350	syl2anr	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
352	351	anandis	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
353	352	abscld	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
354	353	rexrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
355	354	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
356	355	adantlr	|- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
357	164	adantlr	|- ( ( ( ph /\ 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 ) ) , 0 ) ) ) e. RR* )
358	209	ad2antlr	|- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> y e. RR* )
359		xrlelttr	|- ( ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* /\ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* /\ y e. RR* ) -> ( ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) < y ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
360	356 357 358 359	syl3anc	|- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) < y ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
361	349 360	mpand	|- ( ( ( ph /\ 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 ) ) , 0 ) ) ) < y -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
362	252 361	sylanl1	|- ( ( ( ( ( ( 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 ) ) , 0 ) ) ) < y -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
363	362	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 ) ) , 0 ) ) ) < y -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
364	251 363	mpd	|- ( ( ( ( ( ( ( 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 ` ( ( G ` w ) - ( G ` u ) ) ) < y )
365	364	ex	|- ( ( ( ( ( ( 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 ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
366	103 113 116 132 365	wlogle	|- ( ( ( ( ( ( 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 ) ) ) -> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
367	366	anassrs	|- ( ( ( ( ( ( ( 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 ) ) -> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
368	93 367	sylanb	|- ( ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) /\ w e. ( A [,] B ) ) -> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
369	368	ralrimiva	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) -> A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
370		breq2	|- ( z = ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( ( abs ` ( w - u ) ) < z <-> ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) ) )
371	370	rspceaimv	|- ( ( ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) e. RR+ /\ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
372	82 369 371	syl2anc	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
373		ralnex	|- ( A. r e. ( ran f u. ran g ) -. r =/= 0 <-> -. E. r e. ( ran f u. ran g ) r =/= 0 )
374		nne	|- ( -. r =/= 0 <-> r = 0 )
375	374	ralbii	|- ( A. r e. ( ran f u. ran g ) -. r =/= 0 <-> A. r e. ( ran f u. ran g ) r = 0 )
376	373 375	bitr3i	|- ( -. E. r e. ( ran f u. ran g ) r =/= 0 <-> A. r e. ( ran f u. ran g ) r = 0 )
377	17	ffnd	|- ( f e. dom S.1 -> f Fn RR )
378		fnfvelrn	|- ( ( f Fn RR /\ t e. RR ) -> ( f ` t ) e. ran f )
379	377 378	sylan	|- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. ran f )
380		elun1	|- ( ( f ` t ) e. ran f -> ( f ` t ) e. ( ran f u. ran g ) )
381	379 380	syl	|- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. ( ran f u. ran g ) )
382		eqeq1	|- ( r = ( f ` t ) -> ( r = 0 <-> ( f ` t ) = 0 ) )
383	382	rspcva	|- ( ( ( f ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( f ` t ) = 0 )
384	381 383	sylan	|- ( ( ( f e. dom S.1 /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( f ` t ) = 0 )
385	384	adantllr	|- ( ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( f ` t ) = 0 )
386	20	ffnd	|- ( g e. dom S.1 -> g Fn RR )
387		fnfvelrn	|- ( ( g Fn RR /\ t e. RR ) -> ( g ` t ) e. ran g )
388	386 387	sylan	|- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. ran g )
389		elun2	|- ( ( g ` t ) e. ran g -> ( g ` t ) e. ( ran f u. ran g ) )
390	388 389	syl	|- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. ( ran f u. ran g ) )
391		eqeq1	|- ( r = ( g ` t ) -> ( r = 0 <-> ( g ` t ) = 0 ) )
392	391	rspcva	|- ( ( ( g ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( g ` t ) = 0 )
393	392	oveq2d	|- ( ( ( g ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = ( _i x. 0 ) )
394		it0e0	|- ( _i x. 0 ) = 0
395	393 394	eqtrdi	|- ( ( ( g ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = 0 )
396	390 395	sylan	|- ( ( ( g e. dom S.1 /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = 0 )
397	396	adantlll	|- ( ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = 0 )
398	385 397	oveq12d	|- ( ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) = ( 0 + 0 ) )
399	398	an32s	|- ( ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) = ( 0 + 0 ) )
400		00id	|- ( 0 + 0 ) = 0
401	399 400	eqtrdi	|- ( ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) = 0 )
402	401	adantlll	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) = 0 )
403	402	oveq2d	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( if ( t e. D , ( F ` t ) , 0 ) - 0 ) )
404		0cnd	|- ( ( ph /\ -. t e. D ) -> 0 e. CC )
405	149 404	ifclda	|- ( ph -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
406	405	subid1d	|- ( ph -> ( if ( t e. D , ( F ` t ) , 0 ) - 0 ) = if ( t e. D , ( F ` t ) , 0 ) )
407	406	ad3antrrr	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( if ( t e. D , ( F ` t ) , 0 ) - 0 ) = if ( t e. D , ( F ` t ) , 0 ) )
408	403 407	eqtrd	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = if ( t e. D , ( F ` t ) , 0 ) )
409	408	fveq2d	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) = ( abs ` if ( t e. D , ( F ` t ) , 0 ) ) )
410		fvif	|- ( abs ` if ( t e. D , ( F ` t ) , 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) )
411		abs0	|- ( abs ` 0 ) = 0
412		ifeq2	|- ( ( abs ` 0 ) = 0 -> if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
413	411 412	ax-mp	|- if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 )
414	410 413	eqtri	|- ( abs ` if ( t e. D , ( F ` t ) , 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 )
415	409 414	eqtrdi	|- ( ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) /\ t e. RR ) -> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
416	415	mpteq2dva	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) = ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
417	416	fveq2d	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( S.2 ` ( 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. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
418	417	breq1d	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < ( y / 2 ) <-> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) )
419	418	biimpd	|- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < ( y / 2 ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) )
420	419	ex	|- ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( A. r e. ( ran f u. ran g ) r = 0 -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < ( y / 2 ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) ) )
421	420	com23	|- ( ( 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 ) -> ( A. r e. ( ran f u. ran g ) r = 0 -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) ) )
422	421	imp32	|- ( ( ( 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 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) )
423	422	anasss	|- ( ( 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 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) )
424	423	adantlr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( ( 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 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) )
425		1rp	|- 1 e. RR+
426	425	ne0ii	|- RR+ =/= (/)
427	352	anassrs	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ w e. ( A [,] B ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
428	427	abscld	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
429	428	adantlrr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
430	429	adantlr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
431		rpre	|- ( y e. RR+ -> y e. RR )
432	431	rehalfcld	|- ( y e. RR+ -> ( y / 2 ) e. RR )
433	432	adantl	|- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> ( y / 2 ) e. RR )
434	433	ad3antlr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( y / 2 ) e. RR )
435	431	adantl	|- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> y e. RR )
436	435	ad3antlr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> y e. RR )
437	430	rexrd	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
438	157	a1i	|- ( ( ph /\ -. t e. D ) -> 0 e. ( 0 [,] +oo ) )
439	154 438	ifclda	|- ( ph -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
440	439	adantr	|- ( ( ph /\ t e. RR ) -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
441	440	fmpttd	|- ( ph -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
442		itg2cl	|- ( ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
443	441 442	syl	|- ( ph -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
444	443	ad3antrrr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
445	434	rexrd	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( y / 2 ) e. RR* )
446	109 108	oveqan12rd	|- ( ( b = u /\ a = w ) -> ( ( G ` a ) - ( G ` b ) ) = ( ( G ` w ) - ( G ` u ) ) )
447	446	fveq2d	|- ( ( b = u /\ a = w ) -> ( abs ` ( ( G ` a ) - ( G ` b ) ) ) = ( abs ` ( ( G ` w ) - ( G ` u ) ) ) )
448	447	breq1d	|- ( ( b = u /\ a = w ) -> ( ( abs ` ( ( G ` a ) - ( G ` b ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) <-> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) ) )
449	99 98	oveqan12rd	|- ( ( b = w /\ a = u ) -> ( ( G ` a ) - ( G ` b ) ) = ( ( G ` u ) - ( G ` w ) ) )
450	449	fveq2d	|- ( ( b = w /\ a = u ) -> ( abs ` ( ( G ` a ) - ( G ` b ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
451	450	breq1d	|- ( ( b = w /\ a = u ) -> ( ( abs ` ( ( G ` a ) - ( G ` b ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) ) )
452	129	breq1d	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) ) )
453	321	abscld	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) e. RR )
454	453	rexrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) e. RR* )
455	443	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
456	441	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
457		breq2	|- ( ( abs ` ( F ` t ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) -> ( if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) <-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
458		breq2	|- ( 0 = if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) -> ( if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ 0 <-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
459	150	leidd	|- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) <_ ( abs ` ( F ` t ) ) )
460		breq1	|- ( ( abs ` ( F ` t ) ) = if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) -> ( ( abs ` ( F ` t ) ) <_ ( abs ` ( F ` t ) ) <-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) ) )
461		breq1	|- ( 0 = if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) -> ( 0 <_ ( abs ` ( F ` t ) ) <-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) ) )
462	460 461	ifboth	|- ( ( ( abs ` ( F ` t ) ) <_ ( abs ` ( F ` t ) ) /\ 0 <_ ( abs ` ( F ` t ) ) ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
463	459 152 462	syl2anc	|- ( ( ph /\ t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
464	463	adantlr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
465	147	ssneld	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( -. t e. D -> -. t e. ( u (,) w ) ) )
466	465	imp	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. D ) -> -. t e. ( u (,) w ) )
467	226 224	eqbrtrdi	|- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ 0 )
468	466 467	syl	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ 0 )
469	457 458 464 468	ifbothda	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
470	469	ralrimivw	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> A. t e. RR if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
471	233 234	ifex	|- if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. _V
472	471	a1i	|- ( ( ph /\ t e. RR ) -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. _V )
473		eqidd	|- ( ph -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
474	232 236 472 240 473	ofrfval2	|- ( ph -> ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) <-> A. t e. RR if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
475	474	adantr	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) <-> A. t e. RR if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
476	470 475	mpbird	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
477		itg2le	|- ( ( ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) oR <_ ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
478	161 456 476 477	syl3anc	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
479	454 163 455 346 478	xrletrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
480	479	3adantr3	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
481	325 480	eqbrtrd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
482	448 451 115 452 481	wlogle	|- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
483	482	anassrs	|- ( ( ( ph /\ u e. ( A [,] B ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
484	483	adantlrr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
485	484	adantlr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) <_ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) )
486		simplr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) )
487	437 444 445 485 486	xrlelttrd	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < ( y / 2 ) )
488		rphalflt	|- ( y e. RR+ -> ( y / 2 ) < y )
489	488	adantl	|- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> ( y / 2 ) < y )
490	489	ad3antlr	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( y / 2 ) < y )
491	430 434 436 487 490	lttrd	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y )
492	491	a1d	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) /\ w e. ( A [,] B ) ) -> ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
493	492	ralrimiva	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) -> A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
494	493	ralrimivw	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) -> A. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
495		r19.2z	|- ( ( RR+ =/= (/) /\ A. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
496	426 494 495	sylancr	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) < ( y / 2 ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
497	424 496	syldan	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( ( 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 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
498	497	anassrs	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) /\ A. r e. ( ran f u. ran g ) r = 0 ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
499	498	anassrs	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
500	376 499	sylan2b	|- ( ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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 ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
501	372 500	pm2.61dan	|- ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
502	501	ex	|- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ ( 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. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) )
503	502	rexlimdvva	|- ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) -> ( E. f e. dom S.1 E. 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. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) )
504	14 503	mpd	|- ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
505	504	ralrimivva	|- ( ph -> A. u e. ( A [,] B ) A. y e. RR+ E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
506		ssid	|- CC C_ CC
507		elcncf2	|- ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( G e. ( ( A [,] B ) -cn-> CC ) <-> ( G : ( A [,] B ) --> CC /\ A. u e. ( A [,] B ) A. y e. RR+ E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) ) )
508	118 506 507	sylancl	|- ( ph -> ( G e. ( ( A [,] B ) -cn-> CC ) <-> ( G : ( A [,] B ) --> CC /\ A. u e. ( A [,] B ) A. y e. RR+ E. z e. RR+ A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) ) )
509	10 505 508	mpbir2and	|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )