Theorem ftc1anc 33493

Description: ftc1a 23800 holds for functions that obey the triangle inequality in the absence of ax-cc 9257. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)

Hypotheses

Ref	Expression
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

Ref	Expression
ftc1anc	|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Distinct variable groups:   t, s, x, A   B, s, t, x   D, s, t, x   F, s, t, x   ph, s, t, x   G, s

Allowed substitution hints:   G( x, t)

Proof of Theorem ftc1anc

Dummy variables a b f g r u w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ftc1anc.g	. . 3 |- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2		ftc1anc.a	. . 3 |- ( ph -> A e. RR )
3		ftc1anc.b	. . 3 |- ( ph -> B e. RR )
4		ftc1anc.le	. . 3 |- ( ph -> A <_ B )
5		ftc1anc.s	. . 3 |- ( ph -> ( A (,) B ) C_ D )
6		ftc1anc.d	. . 3 |- ( ph -> D C_ RR )
7		ftc1anc.i	. . 3 |- ( ph -> F e. L^1 )
8		ftc1anc.f	. . 3 |- ( ph -> F : D --> CC )
9	1, 2, 3, 4, 5, 6, 7, 8	ftc1lem2 23799	. 2 |- ( ph -> G : ( A [,] B ) --> CC )
10		rphalfcl 11858	. . . . . 6 |- ( y e. RR+ -> ( y / 2 ) e. RR+ )
11	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem6 33490	. . . . . 6 |- ( ( 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 ) )
12	10, 11	sylan2 491	. . . . 5 |- ( ( 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 ) )
13	12	adantrl 752	. . . 4 |- ( ( 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 ) )
14	10	ad2antll 765	. . . . . . . . . . 11 |- ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) -> ( y / 2 ) e. RR+ )
15		2rp 11837	. . . . . . . . . . . 12 |- 2 e. RR+
16		i1ff 23443	. . . . . . . . . . . . . . . . . . . . 21 |- ( f e. dom S.1 -> f : RR --> RR )
17		frn 6053	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : RR --> RR -> ran f C_ RR )
18	16, 17	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. dom S.1 -> ran f C_ RR )
19	18	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ran f C_ RR )
20		i1ff 23443	. . . . . . . . . . . . . . . . . . . . 21 |- ( g e. dom S.1 -> g : RR --> RR )
21		frn 6053	. . . . . . . . . . . . . . . . . . . . 21 |- ( g : RR --> RR -> ran g C_ RR )
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( g e. dom S.1 -> ran g C_ RR )
23	22	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ran g C_ RR )
24	19, 23	unssd 3789	. . . . . . . . . . . . . . . . . 18 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) C_ RR )
25		ax-resscn 9993	. . . . . . . . . . . . . . . . . 18 |- RR C_ CC
26	24, 25	syl6ss 3615	. . . . . . . . . . . . . . . . 17 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) C_ CC )
27		i1f0rn 23449	. . . . . . . . . . . . . . . . . . 19 |- ( f e. dom S.1 -> 0 e. ran f )
28		elun1 3780	. . . . . . . . . . . . . . . . . . 19 |- ( 0 e. ran f -> 0 e. ( ran f u. ran g ) )
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( f e. dom S.1 -> 0 e. ( ran f u. ran g ) )
30	29	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> 0 e. ( ran f u. ran g ) )
31		absf 14077	. . . . . . . . . . . . . . . . . . 19 |- abs : CC --> RR
32		ffn 6045	. . . . . . . . . . . . . . . . . . 19 |- ( abs : CC --> RR -> abs Fn CC )
33	31, 32	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- abs Fn CC
34		fnfvima 6496	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) )
35	33, 34	mp3an1 1411	. . . . . . . . . . . . . . . . 17 |- ( ( ( ran f u. ran g ) C_ CC /\ 0 e. ( ran f u. ran g ) ) -> ( abs ` 0 ) e. ( abs " ( ran f u. ran g ) ) )
36	26, 30, 35	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs ` 0 ) e. ( abs " ( ran f u. ran g ) ) )
37		ne0i 3921	. . . . . . . . . . . . . . . 16 |- ( ( abs ` 0 ) e. ( abs " ( ran f u. ran g ) ) -> ( abs " ( ran f u. ran g ) ) =/= (/) )
38	36, 37	syl 17	. . . . . . . . . . . . . . 15 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) =/= (/) )
39		imassrn 5477	. . . . . . . . . . . . . . . . 17 |- ( abs " ( ran f u. ran g ) ) C_ ran abs
40		frn 6053	. . . . . . . . . . . . . . . . . 18 |- ( abs : CC --> RR -> ran abs C_ RR )
41	31, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ran abs C_ RR
42	39, 41	sstri 3612	. . . . . . . . . . . . . . . 16 |- ( abs " ( ran f u. ran g ) ) C_ RR
43		ffun 6048	. . . . . . . . . . . . . . . . . 18 |- ( abs : CC --> RR -> Fun abs )
44	31, 43	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- Fun abs
45		i1frn 23444	. . . . . . . . . . . . . . . . . 18 |- ( f e. dom S.1 -> ran f e. Fin )
46		i1frn 23444	. . . . . . . . . . . . . . . . . 18 |- ( g e. dom S.1 -> ran g e. Fin )
47		unfi 8227	. . . . . . . . . . . . . . . . . 18 |- ( ( ran f e. Fin /\ ran g e. Fin ) -> ( ran f u. ran g ) e. Fin )
48	45, 46, 47	syl2an 494	. . . . . . . . . . . . . . . . 17 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( ran f u. ran g ) e. Fin )
49		imafi 8259	. . . . . . . . . . . . . . . . 17 |- ( ( Fun abs /\ ( ran f u. ran g ) e. Fin ) -> ( abs " ( ran f u. ran g ) ) e. Fin )
50	44, 48, 49	sylancr 695	. . . . . . . . . . . . . . . 16 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) e. Fin )
51		fimaxre2 10969	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
52	42, 50, 51	sylancr 695	. . . . . . . . . . . . . . 15 |- ( ( 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 )
53		suprcl 10983	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
54	42, 53	mp3an1 1411	. . . . . . . . . . . . . . 15 |- ( ( ( 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 )
55	38, 52, 54	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) e. RR )
56	55	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( 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 )
57		0red 10041	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> 0 e. RR )
58	26	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> r e. CC )
59	58	abscld 14175	. . . . . . . . . . . . . . . . 17 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( abs ` r ) e. RR )
60	59	adantrr 753	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> ( abs ` r ) e. RR )
61	55	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
62		absgt0 14064	. . . . . . . . . . . . . . . . . . 19 |- ( r e. CC -> ( r =/= 0 <-> 0 < ( abs ` r ) ) )
63	58, 62	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( r =/= 0 <-> 0 < ( abs ` r ) ) )
64	63	biimpd 219	. . . . . . . . . . . . . . . . 17 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ r e. ( ran f u. ran g ) ) -> ( r =/= 0 -> 0 < ( abs ` r ) ) )
65	64	impr 649	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ ( r e. ( ran f u. ran g ) /\ r =/= 0 ) ) -> 0 < ( abs ` r ) )
66	42	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. dom S.1 /\ g e. dom S.1 ) -> ( abs " ( ran f u. ran g ) ) C_ RR )
67	66, 38, 52	3jca 1242	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) )
68	67	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
69		fnfvima 6496	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) )
70	33, 69	mp3an1 1411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ran f u. ran g ) C_ CC /\ r e. ( ran f u. ran g ) ) -> ( abs ` r ) e. ( abs " ( ran f u. ran g ) ) )
71	26, 70	sylan 488	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
72		suprub 10984	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 , < ) )
73	68, 71, 72	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 , < ) )
74	73	adantrr 753	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 , < ) )
75	57, 60, 61, 65, 74	ltletrd 10197	. . . . . . . . . . . . . . 15 |- ( ( ( 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 , < ) )
76	75	rexlimdvaa 3032	. . . . . . . . . . . . . 14 |- ( ( 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 , < ) ) )
77	76	imp 445	. . . . . . . . . . . . 13 |- ( ( ( 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 , < ) )
78	56, 77	elrpd 11869	. . . . . . . . . . . 12 |- ( ( ( 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+ )
79		rpmulcl 11855	. . . . . . . . . . . 12 |- ( ( 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+ )
80	15, 78, 79	sylancr 695	. . . . . . . . . . 11 |- ( ( ( 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+ )
81		rpdivcl 11856	. . . . . . . . . . 11 |- ( ( ( 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+ )
82	14, 80, 81	syl2an 494	. . . . . . . . . 10 |- ( ( ( 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+ )
83	82	anassrs 680	. . . . . . . . 9 |- ( ( ( ( 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+ )
84	83	adantlr 751	. . . . . . . 8 |- ( ( ( ( ( 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+ )
85		ancom 466	. . . . . . . . . . . 12 |- ( ( u e. ( A [,] B ) /\ y e. RR+ ) <-> ( y e. RR+ /\ u e. ( A [,] B ) ) )
86	85	anbi2i 730	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) )
87		an32 839	. . . . . . . . . . . . . . 15 |- ( ( ( 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+ ) ) )
88	87	anbi1i 731	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
89		an32 839	. . . . . . . . . . . . . 14 |- ( ( ( ( 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+ ) ) )
90	88, 89	bitri 264	. . . . . . . . . . . . 13 |- ( ( ( ( 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+ ) ) )
91	90	anbi1i 731	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
92		an32 839	. . . . . . . . . . . 12 |- ( ( ( ( ( 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+ ) ) )
93	91, 92	bitri 264	. . . . . . . . . . 11 |- ( ( ( ( ( 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+ ) ) )
94		anass 681	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) ) )
95	86, 93, 94	3bitr4i 292	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) )
96		oveq12 6659	. . . . . . . . . . . . . . . 16 |- ( ( b = w /\ a = u ) -> ( b - a ) = ( w - u ) )
97	96	ancoms 469	. . . . . . . . . . . . . . 15 |- ( ( a = u /\ b = w ) -> ( b - a ) = ( w - u ) )
98	97	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( a = u /\ b = w ) -> ( abs ` ( b - a ) ) = ( abs ` ( w - u ) ) )
99	98	breq1d 4663	. . . . . . . . . . . . 13 |- ( ( 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 , < ) ) ) ) )
100		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( G ` b ) = ( G ` w ) )
101		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( a = u -> ( G ` a ) = ( G ` u ) )
102	100, 101	oveqan12rd 6670	. . . . . . . . . . . . . . 15 |- ( ( a = u /\ b = w ) -> ( ( G ` b ) - ( G ` a ) ) = ( ( G ` w ) - ( G ` u ) ) )
103	102	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( a = u /\ b = w ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) = ( abs ` ( ( G ` w ) - ( G ` u ) ) ) )
104	103	breq1d 4663	. . . . . . . . . . . . 13 |- ( ( a = u /\ b = w ) -> ( ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y <-> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) )
105	99, 104	imbi12d 334	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
106		oveq12 6659	. . . . . . . . . . . . . . . 16 |- ( ( b = u /\ a = w ) -> ( b - a ) = ( u - w ) )
107	106	ancoms 469	. . . . . . . . . . . . . . 15 |- ( ( a = w /\ b = u ) -> ( b - a ) = ( u - w ) )
108	107	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( a = w /\ b = u ) -> ( abs ` ( b - a ) ) = ( abs ` ( u - w ) ) )
109	108	breq1d 4663	. . . . . . . . . . . . 13 |- ( ( 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 , < ) ) ) ) )
110		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( b = u -> ( G ` b ) = ( G ` u ) )
111		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( a = w -> ( G ` a ) = ( G ` w ) )
112	110, 111	oveqan12rd 6670	. . . . . . . . . . . . . . 15 |- ( ( a = w /\ b = u ) -> ( ( G ` b ) - ( G ` a ) ) = ( ( G ` u ) - ( G ` w ) ) )
113	112	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( a = w /\ b = u ) -> ( abs ` ( ( G ` b ) - ( G ` a ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
114	113	breq1d 4663	. . . . . . . . . . . . 13 |- ( ( a = w /\ b = u ) -> ( ( abs ` ( ( G ` b ) - ( G ` a ) ) ) < y <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) )
115	109, 114	imbi12d 334	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
116		iccssre 12255	. . . . . . . . . . . . . 14 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
117	2, 3, 116	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( A [,] B ) C_ RR )
118	117	ad4antr 768	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
119		simp-4l 806	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 )
120	117, 25	syl6ss 3615	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A [,] B ) C_ CC )
121	120	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( A [,] B ) ) -> w e. CC )
122	120	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( A [,] B ) ) -> u e. CC )
123		abssub 14066	. . . . . . . . . . . . . . . . 17 |- ( ( w e. CC /\ u e. CC ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
124	121, 122, 123	syl2anr 495	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
125	124	anandis 873	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( w - u ) ) = ( abs ` ( u - w ) ) )
126	125	breq1d 4663	. . . . . . . . . . . . . 14 |- ( ( 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 , < ) ) ) ) )
127	9	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( G ` w ) e. CC )
128	9	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( A [,] B ) ) -> ( G ` u ) e. CC )
129		abssub 14066	. . . . . . . . . . . . . . . . 17 |- ( ( ( G ` w ) e. CC /\ ( G ` u ) e. CC ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
130	127, 128, 129	syl2anr 495	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
131	130	anandis 873	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
132	131	breq1d 4663	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y <-> ( abs ` ( ( G ` u ) - ( G ` w ) ) ) < y ) )
133	126, 132	imbi12d 334	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
134	119, 133	sylan 488	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) )
135	2	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> A e. RR* )
136	3	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> B e. RR* )
137	135, 136	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( A e. RR* /\ B e. RR* ) )
138		df-icc 12182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- [,] = ( x e. RR* , y e. RR* |-> { t e. RR* | ( x <_ t /\ t <_ y ) } )
139	138	elixx3g 12188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( u e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ u e. RR* ) /\ ( A <_ u /\ u <_ B ) ) )
140	139	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( u e. ( A [,] B ) -> ( A <_ u /\ u <_ B ) )
141	140	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( u e. ( A [,] B ) -> A <_ u )
142	138	elixx3g 12188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( w e. ( A [,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) /\ ( A <_ w /\ w <_ B ) ) )
143	142	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w e. ( A [,] B ) -> ( A <_ w /\ w <_ B ) )
144	143	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. ( A [,] B ) -> w <_ B )
145	141, 144	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( A <_ u /\ w <_ B ) )
146		ioossioo 12265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ u /\ w <_ B ) ) -> ( u (,) w ) C_ ( A (,) B ) )
147	137, 145, 146	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) C_ ( A (,) B ) )
148	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( A (,) B ) C_ D )
149	147, 148	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) C_ D )
150	149	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> t e. D )
151	8	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ t e. D ) -> ( F ` t ) e. CC )
152	151	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. RR )
153	152	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. RR* )
154	151	absge0d 14183	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. D ) -> 0 <_ ( abs ` ( F ` t ) ) )
155		elxrge0 12281	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( F ` t ) ) e. RR* /\ 0 <_ ( abs ` ( F ` t ) ) ) )
156	153, 154, 155	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
157	156	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
158	150, 157	syldan 487	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( abs ` ( F ` t ) ) e. ( 0 [,] +oo ) )
159		0e0iccpnf 12283	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. ( 0 [,] +oo )
160	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. ( u (,) w ) ) -> 0 e. ( 0 [,] +oo ) )
161	158, 160	ifclda 4120	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
162	161	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. RR ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
163		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) )
164	162, 163	fmptd 6385	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. RR |-> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
165		itg2cl 23499	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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* )
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( 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* )
167	166	3adantr3 1222	. . . . . . . . . . . . . . . . 17 |- ( ( 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* )
168	119, 167	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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* )
169	168	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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* )
170		simplll 798	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) )
171	151	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( F ` t ) e. CC )
172	150, 171	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( F ` t ) e. CC )
173	172	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 )
174		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( t e. ( u (,) w ) -> t e. RR )
175	16	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. RR )
176	175	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. CC )
177		ax-icn 9995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- _i e. CC
178	20	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. RR )
179	178	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. CC )
180		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( _i e. CC /\ ( g ` t ) e. CC ) -> ( _i x. ( g ` t ) ) e. CC )
181	177, 179, 180	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( g e. dom S.1 /\ t e. RR ) -> ( _i x. ( g ` t ) ) e. CC )
182		addcl 10018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( f ` t ) e. CC /\ ( _i x. ( g ` t ) ) e. CC ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
183	176, 181, 182	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( f e. dom S.1 /\ t e. RR ) /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
184	183	anandirs 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
185	174, 184	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
186	185	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> ( ( f ` t ) + ( _i x. ( g ` t ) ) ) e. CC )
187	186	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 )
188	173, 187	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 )
189	188	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 )
190	185	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) e. RR )
191	190	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) e. RR )
192	191	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 )
193	189, 192	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 )
194	193	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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* )
195	188	absge0d 14183	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) ) )
196	184	absge0d 14183	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
197	174, 196	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. ( u (,) w ) ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
198	197	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. ( u (,) w ) ) -> 0 <_ ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
199	198	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) )
200	189, 192, 195, 199	addge0d 10603	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) ) ) ) )
201		elxrge0 12281	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) ) ) ) ) )
202	194, 200, 201	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) )
203	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) )
204	202, 203	ifclda 4120	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) )
205	204	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
206		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) )
207	205, 206	fmptd 6385	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
208		itg2cl 23499	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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* )
209	207, 208	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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* )
210	209	3adantr3 1222	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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* )
211	170, 210	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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* )
212	211	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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* )
213		rpxr 11840	. . . . . . . . . . . . . . . 16 |- ( y e. RR+ -> y e. RR* )
214	213	ad3antlr 767	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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* )
215	161	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) )
216	215	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
217	216, 163	fmptd 6385	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
218	173, 187	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) )
219	218	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) )
220	188, 187	abstrid 14195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) ) ) ) )
221	219, 220	eqbrtrrd 4677	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) ) )
222		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) = ( abs ` ( F ` t ) ) )
223	222	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) )
224		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 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 ) ) ) ) ) )
225	224	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) ) )
226	221, 223, 225	3brtr4d 4685	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) )
227	226	ex 450	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 ) ) )
228		0le0 11110	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 0
229	228	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. t e. ( u (,) w ) -> 0 <_ 0 )
230		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) = 0 )
231		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. 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 )
232	229, 230, 231	3brtr4d 4685	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. 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 ) )
233	227, 232	pm2.61d1 171	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) )
234	233	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) )
235		reex 10027	. . . . . . . . . . . . . . . . . . . . . . 23 |- RR e. _V
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> RR e. _V )
237		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( abs ` ( F ` t ) ) e. _V
238		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. _V
239	237, 238	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . 23 |- if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. _V
240	239	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ t e. RR ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) e. _V )
241		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) e. _V
242	241, 238	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . 23 |- if ( t e. ( u (,) w ) , ( ( abs ` ( ( F ` t ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) + ( abs ` ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) , 0 ) e. _V
243	242	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
244		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
245		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
246	236, 240, 243, 244, 245	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
247	246	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) )
248	234, 247	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
249		itg2le 23506	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) )
250	217, 207, 248, 249	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
251	250	3adantr3 1222	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
252	170, 251	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) ) ) )
253	252	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) ) )
254	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem8 33492	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 )
255	169, 212, 214, 253, 254	xrlelttrd 11991	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 )
256		simplll 798	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
257		simpr2 1068	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> w e. ( A [,] B ) )
258		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = w -> ( A (,) x ) = ( A (,) w ) )
259		itgeq1 23539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A (,) x ) = ( A (,) w ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) w ) ( F ` t ) _d t )
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = w -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) w ) ( F ` t ) _d t )
261		itgex 23537	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- S. ( A (,) w ) ( F ` t ) _d t e. _V
262	260, 1, 261	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( w e. ( A [,] B ) -> ( G ` w ) = S. ( A (,) w ) ( F ` t ) _d t )
263	257, 262	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( G ` w ) = S. ( A (,) w ) ( F ` t ) _d t )
264	2	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> A e. RR )
265	117	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. ( A [,] B ) ) -> w e. RR )
266	265	3ad2antr2 1227	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> w e. RR )
267	117	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( A [,] B ) ) -> u e. RR )
268	267	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( A [,] B ) ) -> u e. RR* )
269	268	3ad2antr1 1226	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. RR* )
270		elicc1 12219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A e. RR* /\ B e. RR* ) -> ( u e. ( A [,] B ) <-> ( u e. RR* /\ A <_ u /\ u <_ B ) ) )
271	135, 136, 270	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( u e. ( A [,] B ) <-> ( u e. RR* /\ A <_ u /\ u <_ B ) ) )
272	271	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( A [,] B ) ) -> ( u e. RR* /\ A <_ u /\ u <_ B ) )
273	272	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( A [,] B ) ) -> A <_ u )
274	273	3ad2antr1 1226	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> A <_ u )
275		simpr3 1069	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u <_ w )
276	135	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. ( A [,] B ) ) -> A e. RR* )
277	265	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. ( A [,] B ) ) -> w e. RR* )
278		elicc1 12219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A e. RR* /\ w e. RR* ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
279	276, 277, 278	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
280	279	3ad2antr2 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( u e. ( A [,] w ) <-> ( u e. RR* /\ A <_ u /\ u <_ w ) ) )
281	269, 274, 275, 280	mpbir3and 1245	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. ( A [,] w ) )
282		iooss2 12211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( B e. RR* /\ w <_ B ) -> ( A (,) w ) C_ ( A (,) B ) )
283	136, 144, 282	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) C_ ( A (,) B ) )
284	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) B ) C_ D )
285	283, 284	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) C_ D )
286	285	3ad2antr2 1227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( A (,) w ) C_ D )
287	286	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. ( A (,) w ) ) -> t e. D )
288	151	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. D ) -> ( F ` t ) e. CC )
289	287, 288	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) /\ t e. ( A (,) w ) ) -> ( F ` t ) e. CC )
290		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w = u -> ( w e. ( A [,] B ) <-> u e. ( A [,] B ) ) )
291	290	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w = u -> ( ( ph /\ w e. ( A [,] B ) ) <-> ( ph /\ u e. ( A [,] B ) ) ) )
292		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( w = u -> ( A (,) w ) = ( A (,) u ) )
293	292	mpteq1d 4738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w = u -> ( t e. ( A (,) w ) |-> ( F ` t ) ) = ( t e. ( A (,) u ) |-> ( F ` t ) ) )
294	293	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w = u -> ( ( t e. ( A (,) w ) |-> ( F ` t ) ) e. L^1 <-> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 ) )
295	291, 294	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 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 ) ) )
296		ioombl 23333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( A (,) w ) e. dom vol
297	296	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( A (,) w ) e. dom vol )
298	151	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ w e. ( A [,] B ) ) /\ t e. D ) -> ( F ` t ) e. CC )
299	8	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> F = ( t e. D |-> ( F ` t ) ) )
300	299, 7	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
301	300	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
302	285, 297, 298, 301	iblss 23571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ( A [,] B ) ) -> ( t e. ( A (,) w ) |-> ( F ` t ) ) e. L^1 )
303	295, 302	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( A [,] B ) ) -> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 )
304	303	3ad2antr1 1226	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( t e. ( A (,) u ) |-> ( F ` t ) ) e. L^1 )
305		ioombl 23333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( u (,) w ) e. dom vol
306	305	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( u (,) w ) e. dom vol )
307		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> ( F ` t ) e. _V )
308	300	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
309	149, 306, 307, 308	iblss 23571	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. ( u (,) w ) |-> ( F ` t ) ) e. L^1 )
310	309	3adantr3 1222	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( t e. ( u (,) w ) |-> ( F ` t ) ) e. L^1 )
311	264, 266, 281, 289, 304, 310	itgsplitioo 23604	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) )
312	263, 311	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) )
313		simpr1 1067	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> u e. ( A [,] B ) )
314		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = u -> ( A (,) x ) = ( A (,) u ) )
315		itgeq1 23539	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A (,) x ) = ( A (,) u ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) u ) ( F ` t ) _d t )
316	314, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = u -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) u ) ( F ` t ) _d t )
317		itgex 23537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- S. ( A (,) u ) ( F ` t ) _d t e. _V
318	316, 1, 317	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u e. ( A [,] B ) -> ( G ` u ) = S. ( A (,) u ) ( F ` t ) _d t )
319	313, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( G ` u ) = S. ( A (,) u ) ( F ` t ) _d t )
320	312, 319	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) )
321		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ t e. ( A (,) u ) ) -> ( F ` t ) e. _V )
322	321, 303	itgcl 23550	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ u e. ( A [,] B ) ) -> S. ( A (,) u ) ( F ` t ) _d t e. CC )
323	322	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> S. ( A (,) u ) ( F ` t ) _d t e. CC )
324		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. ( u (,) w ) ) -> ( F ` t ) e. _V )
325	324, 309	itgcl 23550	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> S. ( u (,) w ) ( F ` t ) _d t e. CC )
326	323, 325	pncan2d 10394	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
327	326	3adantr3 1222	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 )
328	320, 327	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( ( G ` w ) - ( G ` u ) ) = S. ( u (,) w ) ( F ` t ) _d t )
329	328	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) = ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) )
330		ftc1anc.t	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) ) )
331		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u (,) w ) = ( (,) ` <. u , w >. )
332		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> <. u , w >. e. ( ( A [,] B ) X. ( A [,] B ) ) )
333		ioof 12271	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (,) : ( RR* X. RR* ) --> ~P RR
334		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
335	333, 334	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (,) Fn ( RR* X. RR* )
336		iccssxr 12256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A [,] B ) C_ RR*
337		xpss12 5225	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A [,] B ) C_ RR* /\ ( A [,] B ) C_ RR* ) -> ( ( A [,] B ) X. ( A [,] B ) ) C_ ( RR* X. RR* ) )
338	336, 336, 337	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A [,] B ) X. ( A [,] B ) ) C_ ( RR* X. RR* )
339		fnfvima 6496	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( (,) 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 ) ) ) )
340	335, 338, 339	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. u , w >. e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` <. u , w >. ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
341	332, 340	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( (,) ` <. u , w >. ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
342	331, 341	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) -> ( u (,) w ) e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) )
343		itgeq1 23539	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s = ( u (,) w ) -> S. s ( F ` t ) _d t = S. ( u (,) w ) ( F ` t ) _d t )
344	343	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s = ( u (,) w ) -> ( abs ` S. s ( F ` t ) _d t ) = ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) )
345		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = ( u (,) w ) -> ( t e. s <-> t e. ( u (,) w ) ) )
346	345	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s = ( u (,) w ) -> if ( t e. s , ( abs ` ( F ` t ) ) , 0 ) = if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) )
347	346	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) )
348	347	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) ) )
349	344, 348	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) ) ) )
350	349	rspccva 3308	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) )
351	330, 342, 350	syl2an 494	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) ) )
352	351	3adantr3 1222	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) )
353	329, 352	eqbrtrd 4675	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
354	353	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
355		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( G ` w ) e. CC /\ ( G ` u ) e. CC ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
356	127, 128, 355	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ ( ph /\ w e. ( A [,] B ) ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
357	356	anandis 873	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
358	357	abscld 14175	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
359	358	rexrd 10089	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
360	359	3adantr3 1222	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
361	360	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR* )
362	167	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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* )
363	213	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ y e. RR+ ) /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) /\ u <_ w ) ) -> y e. RR* )
364		xrlelttr 11987	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
365	361, 362, 363, 364	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
366	354, 365	mpand 711	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
367	256, 366	sylanl1 682	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 ) )
368	367	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 ) )
369	255, 368	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 )
370	369	ex 450	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
371	105, 115, 118, 134, 370	wlogle 10561	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) )
372	371	anassrs 680	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) )
373	95, 372	sylanb 489	. . . . . . . . 9 |- ( ( ( ( ( ( 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 ) )
374	373	ralrimiva 2966	. . . . . . . 8 |- ( ( ( ( ( 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 ) )
375		breq2 4657	. . . . . . . . . . 11 |- ( 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 , < ) ) ) ) )
376	375	imbi1d 331	. . . . . . . . . 10 |- ( z = ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) <-> ( ( abs ` ( w - u ) ) < ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) ) )
377	376	ralbidv 2986	. . . . . . . . 9 |- ( z = ( ( y / 2 ) / ( 2 x. sup ( ( abs " ( ran f u. ran g ) ) , RR , < ) ) ) -> ( A. w e. ( A [,] B ) ( ( abs ` ( w - u ) ) < z -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) < y ) <-> 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 ) ) )
378	377	rspcev 3309	. . . . . . . 8 |- ( ( ( ( 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 ) )
379	84, 374, 378	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( 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 ) )
380		ralnex 2992	. . . . . . . . 9 |- ( A. r e. ( ran f u. ran g ) -. r =/= 0 <-> -. E. r e. ( ran f u. ran g ) r =/= 0 )
381		nne 2798	. . . . . . . . . 10 |- ( -. r =/= 0 <-> r = 0 )
382	381	ralbii 2980	. . . . . . . . 9 |- ( A. r e. ( ran f u. ran g ) -. r =/= 0 <-> A. r e. ( ran f u. ran g ) r = 0 )
383	380, 382	bitr3i 266	. . . . . . . 8 |- ( -. E. r e. ( ran f u. ran g ) r =/= 0 <-> A. r e. ( ran f u. ran g ) r = 0 )
384		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( f : RR --> RR -> f Fn RR )
385	16, 384	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( f e. dom S.1 -> f Fn RR )
386		fnfvelrn 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( f Fn RR /\ t e. RR ) -> ( f ` t ) e. ran f )
387	385, 386	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. ran f )
388		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( f ` t ) e. ran f -> ( f ` t ) e. ( ran f u. ran g ) )
389	387, 388	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. ( ran f u. ran g ) )
390		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( r = ( f ` t ) -> ( r = 0 <-> ( f ` t ) = 0 ) )
391	390	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( f ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( f ` t ) = 0 )
392	389, 391	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( f e. dom S.1 /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( f ` t ) = 0 )
393	392	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 )
394		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( g : RR --> RR -> g Fn RR )
395	20, 394	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( g e. dom S.1 -> g Fn RR )
396		fnfvelrn 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( g Fn RR /\ t e. RR ) -> ( g ` t ) e. ran g )
397	395, 396	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. ran g )
398		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( g ` t ) e. ran g -> ( g ` t ) e. ( ran f u. ran g ) )
399	397, 398	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. ( ran f u. ran g ) )
400		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( r = ( g ` t ) -> ( r = 0 <-> ( g ` t ) = 0 ) )
401	400	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( g ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( g ` t ) = 0 )
402	401	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( 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 ) )
403		it0e0 11254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( _i x. 0 ) = 0
404	402, 403	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( g ` t ) e. ( ran f u. ran g ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = 0 )
405	399, 404	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( g e. dom S.1 /\ t e. RR ) /\ A. r e. ( ran f u. ran g ) r = 0 ) -> ( _i x. ( g ` t ) ) = 0 )
406	405	adantlll 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 )
407	393, 406	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 ) )
408	407	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) )
409		00id 10211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 0 + 0 ) = 0
410	408, 409	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 )
411	410	adantlll 754	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 )
412	411	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) )
413		0cnd 10033	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ -. t e. D ) -> 0 e. CC )
414	151, 413	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
415	414	subid1d 10381	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( if ( t e. D , ( F ` t ) , 0 ) - 0 ) = if ( t e. D , ( F ` t ) , 0 ) )
416	415	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) )
417	412, 416	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) )
418	417	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) )
419		fvif 6204	. . . . . . . . . . . . . . . . . . . . . 22 |- ( abs ` if ( t e. D , ( F ` t ) , 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) )
420		abs0 14025	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( abs ` 0 ) = 0
421		ifeq2 4091	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( abs ` 0 ) = 0 -> if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
422	420, 421	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- if ( t e. D , ( abs ` ( F ` t ) ) , ( abs ` 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 )
423	419, 422	eqtri 2644	. . . . . . . . . . . . . . . . . . . . 21 |- ( abs ` if ( t e. D , ( F ` t ) , 0 ) ) = if ( t e. D , ( abs ` ( F ` t ) ) , 0 )
424	418, 423	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
425	424	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
426	425	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
427	426	breq1d 4663	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
428	427	biimpd 219	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
429	428	ex 450	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
430	429	com23 86	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
431	430	imp32 449	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
432	431	anasss 679	. . . . . . . . . . . 12 |- ( ( 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 ) )
433	432	adantlr 751	. . . . . . . . . . 11 |- ( ( ( 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 ) )
434		1rp 11836	. . . . . . . . . . . . 13 |- 1 e. RR+
435	434	ne0ii 3923	. . . . . . . . . . . 12 |- RR+ =/= (/)
436	357	anassrs 680	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ w e. ( A [,] B ) ) -> ( ( G ` w ) - ( G ` u ) ) e. CC )
437	436	abscld 14175	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ u e. ( A [,] B ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
438	437	adantlrr 757	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ y e. RR+ ) ) /\ w e. ( A [,] B ) ) -> ( abs ` ( ( G ` w ) - ( G ` u ) ) ) e. RR )
439	438	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
440		rpre 11839	. . . . . . . . . . . . . . . . . . 19 |- ( y e. RR+ -> y e. RR )
441	440	rehalfcld 11279	. . . . . . . . . . . . . . . . . 18 |- ( y e. RR+ -> ( y / 2 ) e. RR )
442	441	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> ( y / 2 ) e. RR )
443	442	ad3antlr 767	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
444	440	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> y e. RR )
445	444	ad3antlr 767	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
446	439	rexrd 10089	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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* )
447	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ -. t e. D ) -> 0 e. ( 0 [,] +oo ) )
448	156, 447	ifclda 4120	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
449	448	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. RR ) -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. ( 0 [,] +oo ) )
450		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) )
451	449, 450	fmptd 6385	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
452		itg2cl 23499	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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* )
453	451, 452	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
454	453	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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* )
455	443	rexrd 10089	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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* )
456	111, 110	oveqan12rd 6670	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b = u /\ a = w ) -> ( ( G ` a ) - ( G ` b ) ) = ( ( G ` w ) - ( G ` u ) ) )
457	456	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( b = u /\ a = w ) -> ( abs ` ( ( G ` a ) - ( G ` b ) ) ) = ( abs ` ( ( G ` w ) - ( G ` u ) ) ) )
458	457	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) ) )
459	101, 100	oveqan12rd 6670	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b = w /\ a = u ) -> ( ( G ` a ) - ( G ` b ) ) = ( ( G ` u ) - ( G ` w ) ) )
460	459	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( b = w /\ a = u ) -> ( abs ` ( ( G ` a ) - ( G ` b ) ) ) = ( abs ` ( ( G ` u ) - ( G ` w ) ) ) )
461	460	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) ) )
462	131	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) ) )
463	325	abscld 14175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) e. RR )
464	463	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( abs ` S. ( u (,) w ) ( F ` t ) _d t ) e. RR* )
465	453	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR* )
466	451	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
467		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 ) ) )
468		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 ) ) )
469	152	leidd 10594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ t e. D ) -> ( abs ` ( F ` t ) ) <_ ( abs ` ( F ` t ) ) )
470		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 ) ) ) )
471		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 ) ) ) )
472	470, 471	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( abs ` ( F ` t ) ) <_ ( abs ` ( F ` t ) ) /\ 0 <_ ( abs ` ( F ` t ) ) ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
473	469, 154, 472	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
474	473	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ ( abs ` ( F ` t ) ) )
475	149	ssneld 3605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) -> ( -. t e. D -> -. t e. ( u (,) w ) ) )
476	475	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. D ) -> -. t e. ( u (,) w ) )
477	230, 228	syl6eqbr 4692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( -. t e. ( u (,) w ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ 0 )
478	476, 477	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( u e. ( A [,] B ) /\ w e. ( A [,] B ) ) ) /\ -. t e. D ) -> if ( t e. ( u (,) w ) , ( abs ` ( F ` t ) ) , 0 ) <_ 0 )
479	467, 468, 474, 478	ifbothda 4123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 ) )
480	479	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) )
481	237, 238	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. _V
482	481	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ t e. RR ) -> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) e. _V )
483		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. D , ( abs ` ( F ` t ) ) , 0 ) ) )
484	236, 240, 482, 244, 483	ofrfval2 6915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 ) ) )
485	484	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) ) )
486	480, 485	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) )
487		itg2le 23506	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) ) )
488	164, 466, 486, 487	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) ) ) )
489	464, 166, 465, 351, 488	xrletrd 11993	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) ) )
490	489	3adantr3 1222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) ) )
491	329, 490	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) )
492	458, 461, 117, 462, 491	wlogle 10561	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) ) )
493	492	anassrs 680	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) )
494	493	adantlrr 757	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
495	494	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) ) )
496		simplr 792	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) )
497	446, 454, 455, 495, 496	xrlelttrd 11991	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
498		rphalflt 11860	. . . . . . . . . . . . . . . . . 18 |- ( y e. RR+ -> ( y / 2 ) < y )
499	498	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( u e. ( A [,] B ) /\ y e. RR+ ) -> ( y / 2 ) < y )
500	499	ad3antlr 767	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
501	439, 443, 445, 497, 500	lttrd 10198	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
502	501	a1d 25	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
503	502	ralrimiva 2966	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
504	503	ralrimivw 2967	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
505		r19.2z 4060	. . . . . . . . . . . 12 |- ( ( 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 ) )
506	435, 504, 505	sylancr 695	. . . . . . . . . . 11 |- ( ( ( 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 ) )
507	433, 506	syldan 487	. . . . . . . . . 10 |- ( ( ( 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 ) )
508	507	anassrs 680	. . . . . . . . 9 |- ( ( ( ( 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 ) )
509	508	anassrs 680	. . . . . . . 8 |- ( ( ( ( ( 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 ) )
510	383, 509	sylan2b 492	. . . . . . 7 |- ( ( ( ( ( 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 ) )
511	379, 510	pm2.61dan 832	. . . . . 6 |- ( ( ( ( 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 ) )
512	511	ex 450	. . . . 5 |- ( ( ( 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 ) ) )
513	512	rexlimdvva 3038	. . . 4 |- ( ( 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 ) ) )
514	13, 513	mpd 15	. . 3 |- ( ( 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 ) )
515	514	ralrimivva 2971	. 2 |- ( 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 ) )
516		ssid 3624	. . 3 |- CC C_ CC
517		elcncf2 22693	. . 3 |- ( ( ( 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 ) ) ) )
518	120, 516, 517	sylancl 694	. 2 |- ( 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 ) ) ) )
519	9, 515, 518	mpbir2and 957	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   u. cun 3572   C_ wss 3574   (/)c0 3915   ifcif 4086   ~Pcpw 4158   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oRcofr 6896   Fincfn 7955   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   _ici 9938   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   2c2 11070   RR+crp 11832   (,)cioo 12175   [,]cicc 12178   abscabs 13974   -cn->ccncf 22679   volcvol 23232   S.1citg1 23384   S.2citg2 23385   L^1cibl 23386   S.citg 23387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cmp 21190  df-cncf 22681  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390  df-ibl 23391  df-itg 23392  df-0p 23437

This theorem is referenced by:  ftc2nc  33494