Theorem c1liplem1 22932

Description: Lemma for c1lip1 22933. (Contributed by Stefan O'Rear, 15-Nov-2014.)

Hypotheses

Ref	Expression
c1liplem1.a	|- ( ph -> A e. RR )
c1liplem1.b	|- ( ph -> B e. RR )
c1liplem1.le	|- ( ph -> A <_ B )
c1liplem1.f	|- ( ph -> F e. ( CC ^pm RR ) )
c1liplem1.dv	|- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
c1liplem1.cn	|- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
c1liplem1.k	|- K = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )

Assertion

Ref	Expression
c1liplem1	|- ( ph -> ( K e. RR /\ A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) ) )

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

Allowed substitution hints:   K( x, y)

Proof of Theorem c1liplem1

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

Step	Hyp	Ref	Expression
1		c1liplem1.k	. . 3 |- K = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )
2		imassrn 5194	. . . . . 6 |- ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ ran abs
3		absf 13386	. . . . . . 7 |- abs : CC --> RR
4		frn 5748	. . . . . . 7 |- ( abs : CC --> RR -> ran abs C_ RR )
5	3, 4	ax-mp 5	. . . . . 6 |- ran abs C_ RR
6	2, 5	sstri 3473	. . . . 5 |- ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR
7	6	a1i 11	. . . 4 |- ( ph -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR )
8		dvf 22846	. . . . . . . 8 |- ( RR _D F ) : dom ( RR _D F ) --> CC
9		ffun 5744	. . . . . . . 8 |- ( ( RR _D F ) : dom ( RR _D F ) --> CC -> Fun ( RR _D F ) )
10	8, 9	ax-mp 5	. . . . . . 7 |- Fun ( RR _D F )
11	10	a1i 11	. . . . . 6 |- ( ph -> Fun ( RR _D F ) )
12		c1liplem1.dv	. . . . . . . 8 |- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
13		cncff 21909	. . . . . . . 8 |- ( ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( ( RR _D F ) |` ( A [,] B ) ) : ( A [,] B ) --> RR )
14		fdm 5746	. . . . . . . 8 |- ( ( ( RR _D F ) |` ( A [,] B ) ) : ( A [,] B ) --> RR -> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
15	12, 13, 14	3syl 18	. . . . . . 7 |- ( ph -> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
16		ssdmres 5141	. . . . . . 7 |- ( ( A [,] B ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
17	15, 16	sylibr 215	. . . . . 6 |- ( ph -> ( A [,] B ) C_ dom ( RR _D F ) )
18		c1liplem1.a	. . . . . . . 8 |- ( ph -> A e. RR )
19	18	rexrd 9690	. . . . . . 7 |- ( ph -> A e. RR* )
20		c1liplem1.b	. . . . . . . 8 |- ( ph -> B e. RR )
21	20	rexrd 9690	. . . . . . 7 |- ( ph -> B e. RR* )
22		c1liplem1.le	. . . . . . 7 |- ( ph -> A <_ B )
23		lbicc2 11748	. . . . . . 7 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
24	19, 21, 22, 23	syl3anc 1264	. . . . . 6 |- ( ph -> A e. ( A [,] B ) )
25		funfvima2 6152	. . . . . . 7 |- ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) -> ( A e. ( A [,] B ) -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
26	25	imp 430	. . . . . 6 |- ( ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) /\ A e. ( A [,] B ) ) -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) )
27	11, 17, 24, 26	syl21anc 1263	. . . . 5 |- ( ph -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) )
28		ffun 5744	. . . . . . 7 |- ( abs : CC --> RR -> Fun abs )
29	3, 28	ax-mp 5	. . . . . 6 |- Fun abs
30		imassrn 5194	. . . . . . . 8 |- ( ( RR _D F ) " ( A [,] B ) ) C_ ran ( RR _D F )
31		frn 5748	. . . . . . . . 9 |- ( ( RR _D F ) : dom ( RR _D F ) --> CC -> ran ( RR _D F ) C_ CC )
32	8, 31	ax-mp 5	. . . . . . . 8 |- ran ( RR _D F ) C_ CC
33	30, 32	sstri 3473	. . . . . . 7 |- ( ( RR _D F ) " ( A [,] B ) ) C_ CC
34	3	fdmi 5747	. . . . . . 7 |- dom abs = CC
35	33, 34	sseqtr4i 3497	. . . . . 6 |- ( ( RR _D F ) " ( A [,] B ) ) C_ dom abs
36		funfvima2 6152	. . . . . 6 |- ( ( Fun abs /\ ( ( RR _D F ) " ( A [,] B ) ) C_ dom abs ) -> ( ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) )
37	29, 35, 36	mp2an 676	. . . . 5 |- ( ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
38		ne0i 3767	. . . . 5 |- ( ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
39	27, 37, 38	3syl 18	. . . 4 |- ( ph -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
40		ax-resscn 9596	. . . . . . . 8 |- RR C_ CC
41		ssid 3483	. . . . . . . 8 |- CC C_ CC
42		cncfss 21915	. . . . . . . 8 |- ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
43	40, 41, 42	mp2an 676	. . . . . . 7 |- ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
44	43, 12	sseldi 3462	. . . . . 6 |- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
45		cniccbdd 22396	. . . . . 6 |- ( ( A e. RR /\ B e. RR /\ ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a )
46	18, 20, 44, 45	syl3anc 1264	. . . . 5 |- ( ph -> E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a )
47		fvelima 5929	. . . . . . . . . 10 |- ( ( Fun abs /\ b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) -> E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b )
48	29, 47	mpan 674	. . . . . . . . 9 |- ( b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b )
49		fvelima 5929	. . . . . . . . . . . . . 14 |- ( ( Fun ( RR _D F ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y )
50	10, 49	mpan 674	. . . . . . . . . . . . 13 |- ( y e. ( ( RR _D F ) " ( A [,] B ) ) -> E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y )
51		fvres 5891	. . . . . . . . . . . . . . . . . . 19 |- ( b e. ( A [,] B ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) = ( ( RR _D F ) ` b ) )
52	51	adantl 467	. . . . . . . . . . . . . . . . . 18 |- ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) = ( ( RR _D F ) ` b ) )
53	52	fveq2d 5881	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) = ( abs ` ( ( RR _D F ) ` b ) ) )
54		fveq2 5877	. . . . . . . . . . . . . . . . . . . 20 |- ( x = b -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) = ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) )
55	54	fveq2d 5881	. . . . . . . . . . . . . . . . . . 19 |- ( x = b -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) = ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) )
56	55	breq1d 4430	. . . . . . . . . . . . . . . . . 18 |- ( x = b -> ( ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a <-> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) <_ a ) )
57	56	rspccva 3181	. . . . . . . . . . . . . . . . 17 |- ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) <_ a )
58	53, 57	eqbrtrrd 4443	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` b ) ) <_ a )
59	58	adantll 718	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ b e. ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` b ) ) <_ a )
60		fveq2 5877	. . . . . . . . . . . . . . . 16 |- ( ( ( RR _D F ) ` b ) = y -> ( abs ` ( ( RR _D F ) ` b ) ) = ( abs ` y ) )
61	60	breq1d 4430	. . . . . . . . . . . . . . 15 |- ( ( ( RR _D F ) ` b ) = y -> ( ( abs ` ( ( RR _D F ) ` b ) ) <_ a <-> ( abs ` y ) <_ a ) )
62	59, 61	syl5ibcom 223	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ b e. ( A [,] B ) ) -> ( ( ( RR _D F ) ` b ) = y -> ( abs ` y ) <_ a ) )
63	62	rexlimdva 2917	. . . . . . . . . . . . 13 |- ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y -> ( abs ` y ) <_ a ) )
64	50, 63	syl5 33	. . . . . . . . . . . 12 |- ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( y e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` y ) <_ a ) )
65	64	imp 430	. . . . . . . . . . 11 |- ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs ` y ) <_ a )
66		breq1 4423	. . . . . . . . . . 11 |- ( ( abs ` y ) = b -> ( ( abs ` y ) <_ a <-> b <_ a ) )
67	65, 66	syl5ibcom 223	. . . . . . . . . 10 |- ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( ( abs ` y ) = b -> b <_ a ) )
68	67	rexlimdva 2917	. . . . . . . . 9 |- ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b -> b <_ a ) )
69	48, 68	syl5 33	. . . . . . . 8 |- ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> b <_ a ) )
70	69	ralrimiv 2837	. . . . . . 7 |- ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
71	70	ex 435	. . . . . 6 |- ( ( ph /\ a e. RR ) -> ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a -> A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) )
72	71	reximdva 2900	. . . . 5 |- ( ph -> ( E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) )
73	46, 72	mpd 15	. . . 4 |- ( ph -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
74		suprcl 10569	. . . 4 |- ( ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR /\ ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) /\ E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) -> sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) e. RR )
75	7, 39, 73, 74	syl3anc 1264	. . 3 |- ( ph -> sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) e. RR )
76	1, 75	syl5eqel 2514	. 2 |- ( ph -> K e. RR )
77		simplrr 769	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( A [,] B ) )
78		fvres 5891	. . . . . . . . . . 11 |- ( y e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` y ) = ( F ` y ) )
79	77, 78	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) = ( F ` y ) )
80		c1liplem1.cn	. . . . . . . . . . . . . 14 |- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
81		cncff 21909	. . . . . . . . . . . . . 14 |- ( ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
82	80, 81	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
83	82	ad2antrr 730	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
84	83, 77	ffvelrnd 6034	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) e. RR )
85	84	recnd 9669	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) e. CC )
86	79, 85	eqeltrrd 2511	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) e. CC )
87		simplrl 768	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( A [,] B ) )
88		fvres 5891	. . . . . . . . . . 11 |- ( x e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` x ) = ( F ` x ) )
89	87, 88	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) = ( F ` x ) )
90	83, 87	ffvelrnd 6034	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) e. RR )
91	90	recnd 9669	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) e. CC )
92	89, 91	eqeltrrd 2511	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) e. CC )
93	86, 92	subcld 9986	. . . . . . . 8 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) e. CC )
94		iccssre 11716	. . . . . . . . . . . . 13 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
95	18, 20, 94	syl2anc 665	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
96	95	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ RR )
97	96, 77	sseldd 3465	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR )
98	96, 87	sseldd 3465	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR )
99	97, 98	resubcld 10047	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR )
100	99	recnd 9669	. . . . . . . 8 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. CC )
101		simpr 462	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x < y )
102		difrp 11337	. . . . . . . . . . 11 |- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> ( y - x ) e. RR+ ) )
103	98, 97, 102	syl2anc 665	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x < y <-> ( y - x ) e. RR+ ) )
104	101, 103	mpbid 213	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR+ )
105	104	rpne0d 11346	. . . . . . . 8 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) =/= 0 )
106	93, 100, 105	absdivd 13502	. . . . . . 7 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) )
107	6	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR )
108	39	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
109	73	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
110	29	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> Fun abs )
111	93, 100, 105	divcld 10383	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. CC )
112	111, 34	syl6eleqr 2521	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs )
113	98	rexrd 9690	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR* )
114	97	rexrd 9690	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR* )
115	98, 97, 101	ltled 9783	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x <_ y )
116		ubicc2 11749	. . . . . . . . . . . . . . 15 |- ( ( x e. RR* /\ y e. RR* /\ x <_ y ) -> y e. ( x [,] y ) )
117	113, 114, 115, 116	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( x [,] y ) )
118		fvres 5891	. . . . . . . . . . . . . 14 |- ( y e. ( x [,] y ) -> ( ( F |` ( x [,] y ) ) ` y ) = ( F ` y ) )
119	117, 118	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( x [,] y ) ) ` y ) = ( F ` y ) )
120		lbicc2 11748	. . . . . . . . . . . . . . 15 |- ( ( x e. RR* /\ y e. RR* /\ x <_ y ) -> x e. ( x [,] y ) )
121	113, 114, 115, 120	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( x [,] y ) )
122		fvres 5891	. . . . . . . . . . . . . 14 |- ( x e. ( x [,] y ) -> ( ( F |` ( x [,] y ) ) ` x ) = ( F ` x ) )
123	121, 122	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( x [,] y ) ) ` x ) = ( F ` x ) )
124	119, 123	oveq12d 6319	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) = ( ( F ` y ) - ( F ` x ) ) )
125	124	oveq1d 6316	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) = ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) )
126		iccss2 11705	. . . . . . . . . . . . . . . 16 |- ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( x [,] y ) C_ ( A [,] B ) )
127	126	ad2antlr 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x [,] y ) C_ ( A [,] B ) )
128	127	resabs1d 5149	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) = ( F |` ( x [,] y ) ) )
129	80	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
130		rescncf 21913	. . . . . . . . . . . . . . 15 |- ( ( x [,] y ) C_ ( A [,] B ) -> ( ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) ) )
131	127, 129, 130	sylc 62	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) )
132	128, 131	eqeltrrd 2511	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) )
133	40	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> RR C_ CC )
134		c1liplem1.f	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F e. ( CC ^pm RR ) )
135	134	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F e. ( CC ^pm RR ) )
136		cnex 9620	. . . . . . . . . . . . . . . . . . . 20 |- CC e. _V
137		reex 9630	. . . . . . . . . . . . . . . . . . . 20 |- RR e. _V
138	136, 137	elpm2 7507	. . . . . . . . . . . . . . . . . . 19 |- ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
139	138	simplbi 461	. . . . . . . . . . . . . . . . . 18 |- ( F e. ( CC ^pm RR ) -> F : dom F --> CC )
140	135, 139	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F : dom F --> CC )
141	138	simprbi 465	. . . . . . . . . . . . . . . . . 18 |- ( F e. ( CC ^pm RR ) -> dom F C_ RR )
142	135, 141	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom F C_ RR )
143		iccssre 11716	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. RR /\ y e. RR ) -> ( x [,] y ) C_ RR )
144	98, 97, 143	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x [,] y ) C_ RR )
145		eqid 2422	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
146	145	tgioo2 21805	. . . . . . . . . . . . . . . . . 18 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
147	145, 146	dvres 22850	. . . . . . . . . . . . . . . . 17 |- ( ( ( RR C_ CC /\ F : dom F --> CC ) /\ ( dom F C_ RR /\ ( x [,] y ) C_ RR ) ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) )
148	133, 140, 142, 144, 147	syl22anc 1265	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) )
149		iccntr 21823	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. RR /\ y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
150	98, 97, 149	syl2anc 665	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
151	150	reseq2d 5120	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( x (,) y ) ) )
152	148, 151	eqtrd 2463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( x (,) y ) ) )
153	152	dmeqd 5052	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( RR _D ( F |` ( x [,] y ) ) ) = dom ( ( RR _D F ) |` ( x (,) y ) ) )
154		ioossicc 11720	. . . . . . . . . . . . . . . . 17 |- ( x (,) y ) C_ ( x [,] y )
155	154, 127	syl5ss 3475	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x (,) y ) C_ ( A [,] B ) )
156	17	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ dom ( RR _D F ) )
157	155, 156	sstrd 3474	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x (,) y ) C_ dom ( RR _D F ) )
158		ssdmres 5141	. . . . . . . . . . . . . . 15 |- ( ( x (,) y ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( x (,) y ) ) = ( x (,) y ) )
159	157, 158	sylib 199	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( ( RR _D F ) |` ( x (,) y ) ) = ( x (,) y ) )
160	153, 159	eqtrd 2463	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( RR _D ( F |` ( x [,] y ) ) ) = ( x (,) y ) )
161	98, 97, 101, 132, 160	mvth 22928	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> E. a e. ( x (,) y ) ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) )
162	152	fveq1d 5879	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) )
163	162	adantrr 721	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) )
164		fvres 5891	. . . . . . . . . . . . . . . . . 18 |- ( a e. ( x (,) y ) -> ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) = ( ( RR _D F ) ` a ) )
165	164	ad2antll 733	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) = ( ( RR _D F ) ` a ) )
166	163, 165	eqtrd 2463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( RR _D F ) ` a ) )
167	10	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> Fun ( RR _D F ) )
168	17	ad2antrr 730	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( A [,] B ) C_ dom ( RR _D F ) )
169	155	sseld 3463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( a e. ( x (,) y ) -> a e. ( A [,] B ) ) )
170	169	impr 623	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> a e. ( A [,] B ) )
171		funfvima2 6152	. . . . . . . . . . . . . . . . . 18 |- ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) -> ( a e. ( A [,] B ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
172	171	imp 430	. . . . . . . . . . . . . . . . 17 |- ( ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) /\ a e. ( A [,] B ) ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
173	167, 168, 170, 172	syl21anc 1263	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
174	166, 173	eqeltrd 2510	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
175		eleq1 2494	. . . . . . . . . . . . . . 15 |- ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) <-> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
176	174, 175	syl5ibcom 223	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
177	176	expr 618	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( a e. ( x (,) y ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) ) )
178	177	rexlimdv 2915	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( E. a e. ( x (,) y ) ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
179	161, 178	mpd 15	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) )
180	125, 179	eqeltrrd 2511	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) )
181		funfvima 6151	. . . . . . . . . . 11 |- ( ( Fun abs /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs ) -> ( ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) )
182	181	imp 430	. . . . . . . . . 10 |- ( ( ( Fun abs /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs ) /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
183	110, 112, 180, 182	syl21anc 1263	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
184		suprub 10570	. . . . . . . . 9 |- ( ( ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR /\ ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) /\ E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) /\ ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) <_ sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) )
185	107, 108, 109, 183, 184	syl31anc 1267	. . . . . . . 8 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) <_ sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) )
186	185, 1	syl6breqr 4461	. . . . . . 7 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) <_ K )
187	106, 186	eqbrtrrd 4443	. . . . . 6 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) <_ K )
188	93	abscld 13483	. . . . . . 7 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) e. RR )
189	76	ad2antrr 730	. . . . . . 7 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> K e. RR )
190	100, 105	absrpcld 13495	. . . . . . 7 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( y - x ) ) e. RR+ )
191	188, 189, 190	ledivmuld 11391	. . . . . 6 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) <_ K <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( ( abs ` ( y - x ) ) x. K ) ) )
192	187, 191	mpbid 213	. . . . 5 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( ( abs ` ( y - x ) ) x. K ) )
193	190	rpcnd 11343	. . . . . 6 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( y - x ) ) e. CC )
194	189	recnd 9669	. . . . . 6 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> K e. CC )
195	193, 194	mulcomd 9664	. . . . 5 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( abs ` ( y - x ) ) x. K ) = ( K x. ( abs ` ( y - x ) ) ) )
196	192, 195	breqtrd 4445	. . . 4 |- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) )
197	196	ex 435	. . 3 |- ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) )
198	197	ralrimivva 2846	. 2 |- ( ph -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) )
199	76, 198	jca 534	1 |- ( ph -> ( K e. RR /\ A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1868   =/= wne 2618   A.wral 2775   E.wrex 2776   C_ wss 3436   (/)c0 3761   class class class wbr 4420   dom cdm 4849   ran crn 4850   |` cres 4851   "cima 4852   Fun wfun 5591   -->wf 5593   ` cfv 5597  (class class class)co 6301   ^pm cpm 7477   supcsup 7956   CCcc 9537   RRcr 9538   x. cmul 9544   RR*cxr 9674   < clt 9675   <_ cle 9676   - cmin 9860   / cdiv 10269   RR+crp 11302   (,)cioo 11635   [,]cicc 11638   abscabs 13283   TopOpenctopn 15305   topGenctg 15321  ℂ_fldccnfld 18955   intcnt 20016   -cn->ccncf 21892   _D cdv 22802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-fi 7927  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-seq 12213  df-exp 12272  df-hash 12515  df-cj 13148  df-re 13149  df-im 13150  df-sqrt 13284  df-abs 13285  df-struct 15108  df-ndx 15109  df-slot 15110  df-base 15111  df-sets 15112  df-ress 15113  df-plusg 15188  df-mulr 15189  df-starv 15190  df-sca 15191  df-vsca 15192  df-ip 15193  df-tset 15194  df-ple 15195  df-ds 15197  df-unif 15198  df-hom 15199  df-cco 15200  df-rest 15306  df-topn 15307  df-0g 15325  df-gsum 15326  df-topgen 15327  df-pt 15328  df-prds 15331  df-xrs 15385  df-qtop 15391  df-imas 15392  df-xps 15395  df-mre 15477  df-mrc 15478  df-acs 15480  df-mgm 16473  df-sgrp 16512  df-mnd 16522  df-submnd 16568  df-mulg 16661  df-cntz 16956  df-cmn 17417  df-psmet 18947  df-xmet 18948  df-met 18949  df-bl 18950  df-mopn 18951  df-fbas 18952  df-fg 18953  df-cnfld 18956  df-top 19905  df-bases 19906  df-topon 19907  df-topsp 19908  df-cld 20018  df-ntr 20019  df-cls 20020  df-nei 20098  df-lp 20136  df-perf 20137  df-cn 20227  df-cnp 20228  df-haus 20315  df-cmp 20386  df-tx 20561  df-hmeo 20754  df-fil 20845  df-fm 20937  df-flim 20938  df-flf 20939  df-xms 21319  df-ms 21320  df-tms 21321  df-cncf 21894  df-limc 22805  df-dv 22806

This theorem is referenced by:  c1lip1  22933