Theorem dvlip 23756

Description: A function with derivative bounded by M is Lipschitz continuous with Lipschitz constant equal to M. (Contributed by Mario Carneiro, 3-Mar-2015.)

Hypotheses

Ref	Expression
dvlip.a	|- ( ph -> A e. RR )
dvlip.b	|- ( ph -> B e. RR )
dvlip.f	|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
dvlip.d	|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvlip.m	|- ( ph -> M e. RR )
dvlip.l	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )

Assertion

Ref	Expression
dvlip	|- ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) )

Distinct variable groups:   x, A   x, B   ph, x   x, F   x, M

Allowed substitution hints:   X( x)   Y( x)

Proof of Theorem dvlip

Dummy variables a b y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . . . . . . 8 |- ( a = Y -> ( F ` a ) = ( F ` Y ) )
2	1	oveq2d 6666	. . . . . . 7 |- ( a = Y -> ( ( F ` b ) - ( F ` a ) ) = ( ( F ` b ) - ( F ` Y ) ) )
3	2	fveq2d 6195	. . . . . 6 |- ( a = Y -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) )
4		oveq2 6658	. . . . . . . 8 |- ( a = Y -> ( b - a ) = ( b - Y ) )
5	4	fveq2d 6195	. . . . . . 7 |- ( a = Y -> ( abs ` ( b - a ) ) = ( abs ` ( b - Y ) ) )
6	5	oveq2d 6666	. . . . . 6 |- ( a = Y -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( abs ` ( b - Y ) ) ) )
7	3, 6	breq12d 4666	. . . . 5 |- ( a = Y -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) )
8	7	imbi2d 330	. . . 4 |- ( a = Y -> ( ( ph -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) <-> ( ph -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) ) )
9		fveq2 6191	. . . . . . . 8 |- ( b = X -> ( F ` b ) = ( F ` X ) )
10	9	oveq1d 6665	. . . . . . 7 |- ( b = X -> ( ( F ` b ) - ( F ` Y ) ) = ( ( F ` X ) - ( F ` Y ) ) )
11	10	fveq2d 6195	. . . . . 6 |- ( b = X -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) = ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) )
12		oveq1 6657	. . . . . . . 8 |- ( b = X -> ( b - Y ) = ( X - Y ) )
13	12	fveq2d 6195	. . . . . . 7 |- ( b = X -> ( abs ` ( b - Y ) ) = ( abs ` ( X - Y ) ) )
14	13	oveq2d 6666	. . . . . 6 |- ( b = X -> ( M x. ( abs ` ( b - Y ) ) ) = ( M x. ( abs ` ( X - Y ) ) ) )
15	11, 14	breq12d 4666	. . . . 5 |- ( b = X -> ( ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) <-> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
16	15	imbi2d 330	. . . 4 |- ( b = X -> ( ( ph -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) <-> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) ) )
17		fveq2 6191	. . . . . . . . . 10 |- ( y = b -> ( F ` y ) = ( F ` b ) )
18		fveq2 6191	. . . . . . . . . 10 |- ( x = a -> ( F ` x ) = ( F ` a ) )
19	17, 18	oveqan12d 6669	. . . . . . . . 9 |- ( ( y = b /\ x = a ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` b ) - ( F ` a ) ) )
20	19	fveq2d 6195	. . . . . . . 8 |- ( ( y = b /\ x = a ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) = ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
21		oveq12 6659	. . . . . . . . . 10 |- ( ( y = b /\ x = a ) -> ( y - x ) = ( b - a ) )
22	21	fveq2d 6195	. . . . . . . . 9 |- ( ( y = b /\ x = a ) -> ( abs ` ( y - x ) ) = ( abs ` ( b - a ) ) )
23	22	oveq2d 6666	. . . . . . . 8 |- ( ( y = b /\ x = a ) -> ( M x. ( abs ` ( y - x ) ) ) = ( M x. ( abs ` ( b - a ) ) ) )
24	20, 23	breq12d 4666	. . . . . . 7 |- ( ( y = b /\ x = a ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
25	24	ancoms 469	. . . . . 6 |- ( ( x = a /\ y = b ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
26		fveq2 6191	. . . . . . . . . 10 |- ( y = a -> ( F ` y ) = ( F ` a ) )
27		fveq2 6191	. . . . . . . . . 10 |- ( x = b -> ( F ` x ) = ( F ` b ) )
28	26, 27	oveqan12d 6669	. . . . . . . . 9 |- ( ( y = a /\ x = b ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` a ) - ( F ` b ) ) )
29	28	fveq2d 6195	. . . . . . . 8 |- ( ( y = a /\ x = b ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) = ( abs ` ( ( F ` a ) - ( F ` b ) ) ) )
30		oveq12 6659	. . . . . . . . . 10 |- ( ( y = a /\ x = b ) -> ( y - x ) = ( a - b ) )
31	30	fveq2d 6195	. . . . . . . . 9 |- ( ( y = a /\ x = b ) -> ( abs ` ( y - x ) ) = ( abs ` ( a - b ) ) )
32	31	oveq2d 6666	. . . . . . . 8 |- ( ( y = a /\ x = b ) -> ( M x. ( abs ` ( y - x ) ) ) = ( M x. ( abs ` ( a - b ) ) ) )
33	29, 32	breq12d 4666	. . . . . . 7 |- ( ( y = a /\ x = b ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
34	33	ancoms 469	. . . . . 6 |- ( ( x = b /\ y = a ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
35		dvlip.a	. . . . . . 7 |- ( ph -> A e. RR )
36		dvlip.b	. . . . . . 7 |- ( ph -> B e. RR )
37		iccssre 12255	. . . . . . 7 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
38	35, 36, 37	syl2anc 693	. . . . . 6 |- ( ph -> ( A [,] B ) C_ RR )
39		dvlip.f	. . . . . . . . . . 11 |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
40		cncff 22696	. . . . . . . . . . 11 |- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
41	39, 40	syl 17	. . . . . . . . . 10 |- ( ph -> F : ( A [,] B ) --> CC )
42		ffvelrn 6357	. . . . . . . . . . 11 |- ( ( F : ( A [,] B ) --> CC /\ a e. ( A [,] B ) ) -> ( F ` a ) e. CC )
43		ffvelrn 6357	. . . . . . . . . . 11 |- ( ( F : ( A [,] B ) --> CC /\ b e. ( A [,] B ) ) -> ( F ` b ) e. CC )
44	42, 43	anim12dan 882	. . . . . . . . . 10 |- ( ( F : ( A [,] B ) --> CC /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( F ` a ) e. CC /\ ( F ` b ) e. CC ) )
45	41, 44	sylan 488	. . . . . . . . 9 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( F ` a ) e. CC /\ ( F ` b ) e. CC ) )
46	45	simprd 479	. . . . . . . 8 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` b ) e. CC )
47	45	simpld 475	. . . . . . . 8 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` a ) e. CC )
48	46, 47	abssubd 14192	. . . . . . 7 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` a ) - ( F ` b ) ) ) )
49		ax-resscn 9993	. . . . . . . . . . . 12 |- RR C_ CC
50	38, 49	syl6ss 3615	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
51	50	sselda 3603	. . . . . . . . . 10 |- ( ( ph /\ b e. ( A [,] B ) ) -> b e. CC )
52	51	adantrl 752	. . . . . . . . 9 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> b e. CC )
53	50	sselda 3603	. . . . . . . . . 10 |- ( ( ph /\ a e. ( A [,] B ) ) -> a e. CC )
54	53	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> a e. CC )
55	52, 54	abssubd 14192	. . . . . . . 8 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( b - a ) ) = ( abs ` ( a - b ) ) )
56	55	oveq2d 6666	. . . . . . 7 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( abs ` ( a - b ) ) ) )
57	48, 56	breq12d 4666	. . . . . 6 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
58	41	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> F : ( A [,] B ) --> CC )
59		simpr2 1068	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. ( A [,] B ) )
60	58, 59	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F ` b ) e. CC )
61		simpr1 1067	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. ( A [,] B ) )
62	58, 61	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F ` a ) e. CC )
63	60, 62	subeq0ad 10402	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( ( F ` b ) - ( F ` a ) ) = 0 <-> ( F ` b ) = ( F ` a ) ) )
64	63	biimpar 502	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) = 0 )
65	64	abs00bd 14031	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = 0 )
66	38	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( A [,] B ) C_ RR )
67	66, 61	sseldd 3604	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. RR )
68	67	rexrd 10089	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. RR* )
69	66, 59	sseldd 3604	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. RR )
70	69	rexrd 10089	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. RR* )
71		ioon0 12201	. . . . . . . . . . . . 13 |- ( ( a e. RR* /\ b e. RR* ) -> ( ( a (,) b ) =/= (/) <-> a < b ) )
72	68, 70, 71	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( a (,) b ) =/= (/) <-> a < b ) )
73		dvlip.m	. . . . . . . . . . . . . . 15 |- ( ph -> M e. RR )
74	73	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> M e. RR )
75	69, 67	resubcld 10458	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b - a ) e. RR )
76	75	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> ( b - a ) e. RR )
77	35	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A e. RR )
78	77	rexrd 10089	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A e. RR* )
79	36	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> B e. RR )
80		elicc2 12238	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR /\ B e. RR ) -> ( a e. ( A [,] B ) <-> ( a e. RR /\ A <_ a /\ a <_ B ) ) )
81	77, 79, 80	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a e. ( A [,] B ) <-> ( a e. RR /\ A <_ a /\ a <_ B ) ) )
82	61, 81	mpbid 222	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a e. RR /\ A <_ a /\ a <_ B ) )
83	82	simp2d 1074	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A <_ a )
84		iooss1 12210	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ A <_ a ) -> ( a (,) b ) C_ ( A (,) b ) )
85	78, 83, 84	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a (,) b ) C_ ( A (,) b ) )
86	79	rexrd 10089	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> B e. RR* )
87		elicc2 12238	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR /\ B e. RR ) -> ( b e. ( A [,] B ) <-> ( b e. RR /\ A <_ b /\ b <_ B ) ) )
88	77, 79, 87	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b e. ( A [,] B ) <-> ( b e. RR /\ A <_ b /\ b <_ B ) ) )
89	59, 88	mpbid 222	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b e. RR /\ A <_ b /\ b <_ B ) )
90	89	simp3d 1075	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b <_ B )
91		iooss2 12211	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. RR* /\ b <_ B ) -> ( A (,) b ) C_ ( A (,) B ) )
92	86, 90, 91	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( A (,) b ) C_ ( A (,) B ) )
93	85, 92	sstrd 3613	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a (,) b ) C_ ( A (,) B ) )
94		ssn0 3976	. . . . . . . . . . . . . . . 16 |- ( ( ( a (,) b ) C_ ( A (,) B ) /\ ( a (,) b ) =/= (/) ) -> ( A (,) B ) =/= (/) )
95	93, 94	sylan 488	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> ( A (,) B ) =/= (/) )
96		n0 3931	. . . . . . . . . . . . . . . . 17 |- ( ( A (,) B ) =/= (/) <-> E. x x e. ( A (,) B ) )
97		0red 10041	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( A (,) B ) ) -> 0 e. RR )
98		dvf 23671	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( RR _D F ) : dom ( RR _D F ) --> CC
99		dvlip.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
100	99	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
101	98, 100	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
102	101	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
103	102	abscld 14175	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
104	73	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( A (,) B ) ) -> M e. RR )
105	102	absge0d 14183	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ ( abs ` ( ( RR _D F ) ` x ) ) )
106		dvlip.l	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
107	97, 103, 104, 105, 106	letrd 10194	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ M )
108	107	ex 450	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( x e. ( A (,) B ) -> 0 <_ M ) )
109	108	exlimdv 1861	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( E. x x e. ( A (,) B ) -> 0 <_ M ) )
110	109	imp 445	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ E. x x e. ( A (,) B ) ) -> 0 <_ M )
111	96, 110	sylan2b 492	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( A (,) B ) =/= (/) ) -> 0 <_ M )
112	111	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( A (,) B ) =/= (/) ) -> 0 <_ M )
113	95, 112	syldan 487	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ M )
114		simpr3 1069	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a <_ b )
115	69, 67	subge0d 10617	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( 0 <_ ( b - a ) <-> a <_ b ) )
116	114, 115	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( b - a ) )
117	116	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ ( b - a ) )
118	74, 76, 113, 117	mulge0d 10604	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ ( M x. ( b - a ) ) )
119	118	ex 450	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( a (,) b ) =/= (/) -> 0 <_ ( M x. ( b - a ) ) ) )
120	72, 119	sylbird 250	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a < b -> 0 <_ ( M x. ( b - a ) ) ) )
121	69	recnd 10068	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. CC )
122	67	recnd 10068	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. CC )
123	121, 122	subeq0ad 10402	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 <-> b = a ) )
124		equcom 1945	. . . . . . . . . . . . 13 |- ( b = a <-> a = b )
125	123, 124	syl6bb 276	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 <-> a = b ) )
126		0re 10040	. . . . . . . . . . . . . 14 |- 0 e. RR
127	73	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> M e. RR )
128	127	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> M e. CC )
129	128	mul01d 10235	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( M x. 0 ) = 0 )
130	129	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 = ( M x. 0 ) )
131		eqle 10139	. . . . . . . . . . . . . 14 |- ( ( 0 e. RR /\ 0 = ( M x. 0 ) ) -> 0 <_ ( M x. 0 ) )
132	126, 130, 131	sylancr 695	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( M x. 0 ) )
133		oveq2 6658	. . . . . . . . . . . . . 14 |- ( ( b - a ) = 0 -> ( M x. ( b - a ) ) = ( M x. 0 ) )
134	133	breq2d 4665	. . . . . . . . . . . . 13 |- ( ( b - a ) = 0 -> ( 0 <_ ( M x. ( b - a ) ) <-> 0 <_ ( M x. 0 ) ) )
135	132, 134	syl5ibrcom 237	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 -> 0 <_ ( M x. ( b - a ) ) ) )
136	125, 135	sylbird 250	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a = b -> 0 <_ ( M x. ( b - a ) ) ) )
137	67, 69	leloed 10180	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a <_ b <-> ( a < b \/ a = b ) ) )
138	114, 137	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a < b \/ a = b ) )
139	120, 136, 138	mpjaod 396	. . . . . . . . . 10 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( M x. ( b - a ) ) )
140	139	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> 0 <_ ( M x. ( b - a ) ) )
141	65, 140	eqbrtrd 4675	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
142	60, 62	subcld 10392	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
143	142	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
144	143	abscld 14175	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR )
145	144	recnd 10068	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. CC )
146	75	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) e. RR )
147	146	recnd 10068	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) e. CC )
148	138	ord 392	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( -. a < b -> a = b ) )
149		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( a = b -> ( F ` a ) = ( F ` b ) )
150	149	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( a = b -> ( F ` b ) = ( F ` a ) )
151	148, 150	syl6 35	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( -. a < b -> ( F ` b ) = ( F ` a ) ) )
152	151	necon1ad 2811	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( F ` b ) =/= ( F ` a ) -> a < b ) )
153	152	imp 445	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> a < b )
154	67	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> a e. RR )
155	69	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> b e. RR )
156	154, 155	posdifd 10614	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a < b <-> 0 < ( b - a ) ) )
157	153, 156	mpbid 222	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> 0 < ( b - a ) )
158	157	gt0ne0d 10592	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) =/= 0 )
159	145, 147, 158	divrec2d 10805	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) = ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
160		iccss2 12244	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) -> ( a [,] b ) C_ ( A [,] B ) )
161	61, 59, 160	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a [,] b ) C_ ( A [,] B ) )
162	161	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a [,] b ) C_ ( A [,] B ) )
163	162	sselda 3603	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> y e. ( A [,] B ) )
164	41	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> F : ( A [,] B ) --> CC )
165	164	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. CC )
166	163, 165	syldan 487	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( F ` y ) e. CC )
167	142	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
168	63	necon3bid 2838	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( ( F ` b ) - ( F ` a ) ) =/= 0 <-> ( F ` b ) =/= ( F ` a ) ) )
169	168	biimpar 502	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
170	169	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
171	166, 167, 170	divcld 10801	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
172	164, 162	feqresmpt 6250	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a [,] b ) ) = ( y e. ( a [,] b ) |-> ( F ` y ) ) )
173		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) = ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) )
174		oveq1 6657	. . . . . . . . . . . . . . . 16 |- ( x = ( F ` y ) -> ( x / ( ( F ` b ) - ( F ` a ) ) ) = ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) )
175	166, 172, 173, 174	fmptco 6396	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) = ( y e. ( a [,] b ) |-> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
176		ref 13852	. . . . . . . . . . . . . . . . 17 |- Re : CC --> RR
177	176	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re : CC --> RR )
178	177	feqmptd 6249	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re = ( x e. CC |-> ( Re ` x ) ) )
179		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( x = ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) -> ( Re ` x ) = ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
180	171, 175, 178, 179	fmptco 6396	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re o. ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) ) = ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
181	39	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> F e. ( ( A [,] B ) -cn-> CC ) )
182		rescncf 22700	. . . . . . . . . . . . . . . . . 18 |- ( ( a [,] b ) C_ ( A [,] B ) -> ( F e. ( ( A [,] B ) -cn-> CC ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) ) )
183	161, 181, 182	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) )
184	183	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) )
185		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) = ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) )
186	185	divccncf 22709	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F ` b ) - ( F ` a ) ) e. CC /\ ( ( F ` b ) - ( F ` a ) ) =/= 0 ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) e. ( CC -cn-> CC ) )
187	143, 169, 186	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) e. ( CC -cn-> CC ) )
188	184, 187	cncfco 22710	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) e. ( ( a [,] b ) -cn-> CC ) )
189		recncf 22705	. . . . . . . . . . . . . . . 16 |- Re e. ( CC -cn-> RR )
190	189	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re e. ( CC -cn-> RR ) )
191	188, 190	cncfco 22710	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re o. ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) ) e. ( ( a [,] b ) -cn-> RR ) )
192	180, 191	eqeltrrd 2702	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) e. ( ( a [,] b ) -cn-> RR ) )
193	49	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> RR C_ CC )
194		iccssre 12255	. . . . . . . . . . . . . . . . . 18 |- ( ( a e. RR /\ b e. RR ) -> ( a [,] b ) C_ RR )
195	154, 155, 194	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a [,] b ) C_ RR )
196	171	recld 13934	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
197	196	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. CC )
198		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
199	198	tgioo2 22606	. . . . . . . . . . . . . . . . 17 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
200		iccntr 22624	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. RR /\ b e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
201	67, 69, 200	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
202	201	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
203	193, 195, 197, 199, 198, 202	dvmptntr 23734	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( RR _D ( y e. ( a (,) b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) )
204		ioossicc 12259	. . . . . . . . . . . . . . . . . . 19 |- ( a (,) b ) C_ ( a [,] b )
205	204	sseli 3599	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( a (,) b ) -> y e. ( a [,] b ) )
206	205, 171	sylan2 491	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
207		ovexd 6680	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. _V )
208		reelprrecn 10028	. . . . . . . . . . . . . . . . . . 19 |- RR e. { RR , CC }
209	208	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> RR e. { RR , CC } )
210	205, 166	sylan2 491	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( F ` y ) e. CC )
211	93	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ ( A (,) B ) )
212	211	sselda 3603	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> y e. ( A (,) B ) )
213	101	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
214	213	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( A (,) B ) ) -> ( ( RR _D F ) ` y ) e. CC )
215	212, 214	syldan 487	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( RR _D F ) ` y ) e. CC )
216	38	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( A [,] B ) C_ RR )
217		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a (,) b ) C_ RR
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ RR )
219	198, 199	dvres 23675	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( RR C_ CC /\ F : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ RR /\ ( a (,) b ) C_ RR ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) )
220	193, 164, 216, 218, 219	syl22anc 1327	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) )
221		retop 22565	. . . . . . . . . . . . . . . . . . . . . 22 |- ( topGen ` ran (,) ) e. Top
222		iooretop 22569	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a (,) b ) e. ( topGen ` ran (,) )
223		isopn3i 20886	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( a (,) b ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) = ( a (,) b ) )
224	221, 222, 223	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) = ( a (,) b )
225	224	reseq2i 5393	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( a (,) b ) )
226	220, 225	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( a (,) b ) ) )
227	204, 162	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ ( A [,] B ) )
228	164, 227	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( F ` y ) ) )
229	228	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( RR _D ( y e. ( a (,) b ) |-> ( F ` y ) ) ) )
230	101	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
231	230, 93	fssresd 6071	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) : ( a (,) b ) --> CC )
232	231	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) )
233	232	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) )
234		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( a (,) b ) -> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) = ( ( RR _D F ) ` y ) )
235	234	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) )
236	233, 235	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) ) )
237	226, 229, 236	3eqtr3d 2664	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( F ` y ) ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) ) )
238	209, 210, 215, 237, 143, 169	dvmptdivc 23728	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
239	206, 207, 238	dvmptre 23732	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
240	203, 239	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
241	240	dmeqd 5326	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> dom ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
242		dmmptg 5632	. . . . . . . . . . . . . . 15 |- ( A. y e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V -> dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( a (,) b ) )
243		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
244	243	a1i 11	. . . . . . . . . . . . . . 15 |- ( y e. ( a (,) b ) -> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V )
245	242, 244	mprg 2926	. . . . . . . . . . . . . 14 |- dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( a (,) b )
246	241, 245	syl6eq 2672	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> dom ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( a (,) b ) )
247	154, 155, 153, 192, 246	mvth 23755	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> E. x e. ( a (,) b ) ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) )
248	240	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` x ) )
249		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( RR _D F ) ` y ) = ( ( RR _D F ) ` x ) )
250	249	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( y = x -> ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) = ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) )
251	250	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( y = x -> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
252		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
253		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
254	251, 252, 253	fvmpt 6282	. . . . . . . . . . . . . . 15 |- ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` x ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
255	248, 254	sylan9eq 2676	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
256		ubicc2 12289	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR* /\ b e. RR* /\ a <_ b ) -> b e. ( a [,] b ) )
257	68, 70, 114, 256	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. ( a [,] b ) )
258	257	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> b e. ( a [,] b ) )
259	17	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 |- ( y = b -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) = ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) )
260	259	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( y = b -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
261		eqid 2622	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
262		fvex 6201	. . . . . . . . . . . . . . . . . . 19 |- ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
263	260, 261, 262	fvmpt 6282	. . . . . . . . . . . . . . . . . 18 |- ( b e. ( a [,] b ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
264	258, 263	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
265		lbicc2 12288	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR* /\ b e. RR* /\ a <_ b ) -> a e. ( a [,] b ) )
266	68, 70, 114, 265	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. ( a [,] b ) )
267	266	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> a e. ( a [,] b ) )
268	26	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 |- ( y = a -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) = ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) )
269	268	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( y = a -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
270		fvex 6201	. . . . . . . . . . . . . . . . . . 19 |- ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
271	269, 261, 270	fvmpt 6282	. . . . . . . . . . . . . . . . . 18 |- ( a e. ( a [,] b ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
272	267, 271	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
273	264, 272	oveq12d 6668	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) = ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
274	60	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F ` b ) e. CC )
275	274, 143, 169	divcld 10801	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
276	62	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F ` a ) e. CC )
277	276, 143, 169	divcld 10801	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
278	275, 277	resubd 13956	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
279	274, 276, 143, 169	divsubdird 10840	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) - ( F ` a ) ) / ( ( F ` b ) - ( F ` a ) ) ) = ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
280	143, 169	dividd 10799	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) - ( F ` a ) ) / ( ( F ` b ) - ( F ` a ) ) ) = 1 )
281	279, 280	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) = 1 )
282	281	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( Re ` 1 ) )
283		re1 13894	. . . . . . . . . . . . . . . . . . 19 |- ( Re ` 1 ) = 1
284	282, 283	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
285	278, 284	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
286	285	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
287	273, 286	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) = 1 )
288	287	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) = ( 1 / ( b - a ) ) )
289	255, 288	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) <-> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) ) )
290	289	rexbidva 3049	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( E. x e. ( a (,) b ) ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) <-> E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) ) )
291	247, 290	mpbid 222	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) )
292	211	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> x e. ( A (,) B ) )
293	213	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
294	292, 293	syldan 487	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( RR _D F ) ` x ) e. CC )
295	142	ad2antrr 762	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
296	169	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
297	294, 295, 296	divcld 10801	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
298	297	recld 13934	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
299	144	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR )
300	298, 299	remulcld 10070	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
301	294	abscld 14175	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
302	127	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> M e. RR )
303	297	abscld 14175	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
304	143	absge0d 14183	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> 0 <_ ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
305	304	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> 0 <_ ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
306	297	releabsd 14190	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
307	298, 303, 299, 305, 306	lemul1ad 10963	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
308	297, 295	absmuld 14193	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) ) = ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
309	294, 295, 296	divcan1d 10802	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) = ( ( RR _D F ) ` x ) )
310	309	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
311	308, 310	eqtr3d 2658	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
312	307, 311	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( abs ` ( ( RR _D F ) ` x ) ) )
313	106	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
314	313	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
315	292, 314	syldan 487	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
316	300, 301, 302, 312, 315	letrd 10194	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M )
317		oveq1 6657	. . . . . . . . . . . . . 14 |- ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) = ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
318	317	breq1d 4663	. . . . . . . . . . . . 13 |- ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M <-> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
319	316, 318	syl5ibcom 235	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
320	319	rexlimdva 3031	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
321	291, 320	mpd 15	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M )
322	159, 321	eqbrtrd 4675	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M )
323	73	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> M e. RR )
324		ledivmul2 10902	. . . . . . . . . 10 |- ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR /\ M e. RR /\ ( ( b - a ) e. RR /\ 0 < ( b - a ) ) ) -> ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) ) )
325	144, 323, 146, 157, 324	syl112anc 1330	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) ) )
326	322, 325	mpbid 222	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
327	141, 326	pm2.61dane 2881	. . . . . . 7 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
328	67, 69, 114	abssubge0d 14170	. . . . . . . 8 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( b - a ) ) = ( b - a ) )
329	328	oveq2d 6666	. . . . . . 7 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( b - a ) ) )
330	327, 329	breqtrrd 4681	. . . . . 6 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) )
331	25, 34, 38, 57, 330	wlogle 10561	. . . . 5 |- ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) )
332	331	expcom 451	. . . 4 |- ( ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
333	8, 16, 332	vtocl2ga 3274	. . 3 |- ( ( Y e. ( A [,] B ) /\ X e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
334	333	ancoms 469	. 2 |- ( ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
335	334	impcom 446	1 |- ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   C_ wss 3574   (/)c0 3915   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   |` cres 5116   o. ccom 5118   -->wf 5884   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   x. cmul 9941   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   (,)cioo 12175   [,]cicc 12178   Recre 13837   abscabs 13974   TopOpenctopn 16082   topGenctg 16098  ℂ_fldccnfld 19746   Topctop 20698   intcnt 20821   -cn->ccncf 22679   _D cdv 23627

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  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  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-iin 4523  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-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  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-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  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-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  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-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631

This theorem is referenced by:  dvlipcn  23757  dvlip2  23758  dveq0  23763  dvfsumabs  23786  pige3  24269  lgamgulmlem2  24756