Theorem dvlip

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

	Ref	Expression
Hypotheses	dvlip.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	dvlip.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	dvlip.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
	dvlip.d	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
	dvlip.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	dvlip.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
Assertion	dvlip	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvlip.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		dvlip.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		dvlip.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
4		dvlip.d	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5		dvlip.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
6		dvlip.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
7		fveq2	⊢ ( 𝑎 = 𝑌 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑌 ) )
8	7	oveq2d	⊢ ( 𝑎 = 𝑌 → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) )
9	8	fveq2d	⊢ ( 𝑎 = 𝑌 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) )
10		oveq2	⊢ ( 𝑎 = 𝑌 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑌 ) )
11	10	fveq2d	⊢ ( 𝑎 = 𝑌 → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑌 ) ) )
12	11	oveq2d	⊢ ( 𝑎 = 𝑌 → ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) )
13	9 12	breq12d	⊢ ( 𝑎 = 𝑌 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) ) )
14	13	imbi2d	⊢ ( 𝑎 = 𝑌 → ( ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ↔ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) ) ) )
15		fveq2	⊢ ( 𝑏 = 𝑋 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑋 ) )
16	15	fvoveq1d	⊢ ( 𝑏 = 𝑋 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) )
17		fvoveq1	⊢ ( 𝑏 = 𝑋 → ( abs ‘ ( 𝑏 − 𝑌 ) ) = ( abs ‘ ( 𝑋 − 𝑌 ) ) )
18	17	oveq2d	⊢ ( 𝑏 = 𝑋 → ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) )
19	16 18	breq12d	⊢ ( 𝑏 = 𝑋 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) ) )
20	19	imbi2d	⊢ ( 𝑏 = 𝑋 → ( ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑌 ) ) ) ) ↔ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) ) ) )
21		fveq2	⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
22		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
23	21 22	oveqan12d	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) )
24	23	fveq2d	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) )
25		oveq12	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( 𝑦 − 𝑥 ) = ( 𝑏 − 𝑎 ) )
26	25	fveq2d	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( abs ‘ ( 𝑦 − 𝑥 ) ) = ( abs ‘ ( 𝑏 − 𝑎 ) ) )
27	26	oveq2d	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) )
28	24 27	breq12d	⊢ ( ( 𝑦 = 𝑏 ∧ 𝑥 = 𝑎 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
29	28	ancoms	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
30		fveq2	⊢ ( 𝑦 = 𝑎 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) )
31		fveq2	⊢ ( 𝑥 = 𝑏 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑏 ) )
32	30 31	oveqan12d	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) )
33	32	fveq2d	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) ) )
34		oveq12	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( 𝑦 − 𝑥 ) = ( 𝑎 − 𝑏 ) )
35	34	fveq2d	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( abs ‘ ( 𝑦 − 𝑥 ) ) = ( abs ‘ ( 𝑎 − 𝑏 ) ) )
36	35	oveq2d	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑎 − 𝑏 ) ) ) )
37	33 36	breq12d	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑎 − 𝑏 ) ) ) ) )
38	37	ancoms	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑎 − 𝑏 ) ) ) ) )
39		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
40	1 2 39	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
41		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
42	3 41	syl	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
43		ffvelcdm	⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
44		ffvelcdm	⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
45	43 44	anim12dan	⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑏 ) ∈ ℂ ) )
46	42 45	sylan	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑏 ) ∈ ℂ ) )
47	46	simprd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
48	46	simpld	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
49	47 48	abssubd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) ) )
50		ax-resscn	⊢ ℝ ⊆ ℂ
51	40 50	sstrdi	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
52	51	sselda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑏 ∈ ℂ )
53	52	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑏 ∈ ℂ )
54	51	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑎 ∈ ℂ )
55	54	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑎 ∈ ℂ )
56	53 55	abssubd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑎 − 𝑏 ) ) )
57	56	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑎 − 𝑏 ) ) ) )
58	49 57	breq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑎 − 𝑏 ) ) ) ) )
59	42	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
60		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ( 𝐴 [,] 𝐵 ) )
61	59 60	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
62		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ( 𝐴 [,] 𝐵 ) )
63	59 62	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
64	61 63	subeq0ad	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) = 0 ↔ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
65	64	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) = 0 )
66	65	abs00bd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = 0 )
67	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
68	67 62	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ℝ )
69	68	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ℝ* )
70	67 60	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ℝ )
71	70	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ℝ* )
72		ioon0	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
73	69 71 72	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
74	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → 𝑀 ∈ ℝ )
75	70 68	resubcld	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑏 − 𝑎 ) ∈ ℝ )
76	75	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝑏 − 𝑎 ) ∈ ℝ )
77	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐴 ∈ ℝ )
78	77	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐴 ∈ ℝ* )
79	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐵 ∈ ℝ )
80		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵 ) ) )
81	77 79 80	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵 ) ) )
82	62 81	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵 ) )
83	82	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐴 ≤ 𝑎 )
84		iooss1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑎 ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝑏 ) )
85	78 83 84	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝑏 ) )
86	79	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐵 ∈ ℝ* )
87		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵 ) ) )
88	77 79 87	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵 ) ) )
89	60 88	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵 ) )
90	89	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ≤ 𝐵 )
91		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑏 ≤ 𝐵 ) → ( 𝐴 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝐵 ) )
92	86 90 91	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝐴 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝐵 ) )
93	85 92	sstrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝐵 ) )
94		ssn0	⊢ ( ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
95	93 94	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
96		n0	⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
97		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
98		dvf	⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
99	4	feq2d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
100	98 99	mpbii	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
101	100	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
102	101	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
103	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑀 ∈ ℝ )
104	101	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
105	97 102 103 104 6	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝑀 )
106	105	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 0 ≤ 𝑀 ) )
107	106	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 0 ≤ 𝑀 ) )
108	107	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ 𝑀 )
109	96 108	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → 0 ≤ 𝑀 )
110	109	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → 0 ≤ 𝑀 )
111	95 110	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → 0 ≤ 𝑀 )
112		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ≤ 𝑏 )
113	70 68	subge0d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 0 ≤ ( 𝑏 − 𝑎 ) ↔ 𝑎 ≤ 𝑏 ) )
114	112 113	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 0 ≤ ( 𝑏 − 𝑎 ) )
115	114	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → 0 ≤ ( 𝑏 − 𝑎 ) )
116	74 76 111 115	mulge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
117	116	ex	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
118	73 117	sylbird	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 < 𝑏 → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
119	70	recnd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ℂ )
120	68	recnd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ℂ )
121	119 120	subeq0ad	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝑏 − 𝑎 ) = 0 ↔ 𝑏 = 𝑎 ) )
122		equcom	⊢ ( 𝑏 = 𝑎 ↔ 𝑎 = 𝑏 )
123	121 122	bitrdi	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝑏 − 𝑎 ) = 0 ↔ 𝑎 = 𝑏 ) )
124		0re	⊢ 0 ∈ ℝ
125	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑀 ∈ ℝ )
126	125	recnd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑀 ∈ ℂ )
127	126	mul01d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑀 · 0 ) = 0 )
128	127	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 0 = ( 𝑀 · 0 ) )
129		eqle	⊢ ( ( 0 ∈ ℝ ∧ 0 = ( 𝑀 · 0 ) ) → 0 ≤ ( 𝑀 · 0 ) )
130	124 128 129	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 0 ≤ ( 𝑀 · 0 ) )
131		oveq2	⊢ ( ( 𝑏 − 𝑎 ) = 0 → ( 𝑀 · ( 𝑏 − 𝑎 ) ) = ( 𝑀 · 0 ) )
132	131	breq2d	⊢ ( ( 𝑏 − 𝑎 ) = 0 → ( 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ↔ 0 ≤ ( 𝑀 · 0 ) ) )
133	130 132	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝑏 − 𝑎 ) = 0 → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
134	123 133	sylbird	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 = 𝑏 → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
135	68 70	leloed	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) ) )
136	112 135	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) )
137	118 134 136	mpjaod	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
138	137	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 0 ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
139	66 138	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
140	61 63	subcld	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
141	140	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
142	141	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℝ )
143	142	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
144	75	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑏 − 𝑎 ) ∈ ℝ )
145	144	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑏 − 𝑎 ) ∈ ℂ )
146	136	ord	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ¬ 𝑎 < 𝑏 → 𝑎 = 𝑏 ) )
147		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
148	147	eqcomd	⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) )
149	146 148	syl6	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ¬ 𝑎 < 𝑏 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
150	149	necon1ad	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) → 𝑎 < 𝑏 ) )
151	150	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 𝑎 < 𝑏 )
152	68	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 𝑎 ∈ ℝ )
153	70	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 𝑏 ∈ ℝ )
154	152 153	posdifd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 < 𝑏 ↔ 0 < ( 𝑏 − 𝑎 ) ) )
155	151 154	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 0 < ( 𝑏 − 𝑎 ) )
156	155	gt0ne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑏 − 𝑎 ) ≠ 0 )
157	143 145 156	divrec2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) = ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
158		iccss2	⊢ ( ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 𝐴 [,] 𝐵 ) )
159	62 60 158	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 𝐴 [,] 𝐵 ) )
160	159	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 𝐴 [,] 𝐵 ) )
161	160	sselda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
162	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
163	162	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
164	161 163	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
165	140	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
166	64	necon3bid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ≠ 0 ↔ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) )
167	166	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ≠ 0 )
168	167	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ≠ 0 )
169	164 165 168	divcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
170	162 160	feqresmpt	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) = ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
171		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
172		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) )
173	164 170 171 172	fmptco	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∘ ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ) = ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
174		ref	⊢ ℜ : ℂ ⟶ ℝ
175	174	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ℜ : ℂ ⟶ ℝ )
176	175	feqmptd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ℜ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ 𝑥 ) ) )
177		fveq2	⊢ ( 𝑥 = ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
178	169 173 176 177	fmptco	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℜ ∘ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∘ ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ) ) = ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
179	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
180		rescncf	⊢ ( ( 𝑎 [,] 𝑏 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℂ ) ) )
181	159 179 180	sylc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℂ ) )
182	181	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℂ ) )
183		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) )
184	183	divccncf	⊢ ( ( ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
185	141 167 184	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
186	182 185	cncfco	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∘ ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℂ ) )
187		recncf	⊢ ℜ ∈ ( ℂ –cn→ ℝ )
188	187	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ℜ ∈ ( ℂ –cn→ ℝ ) )
189	186 188	cncfco	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℜ ∘ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∘ ( 𝐹 ↾ ( 𝑎 [,] 𝑏 ) ) ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℝ ) )
190	178 189	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ∈ ( ( 𝑎 [,] 𝑏 ) –cn→ ℝ ) )
191	50	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ℝ ⊆ ℂ )
192		iccssre	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ )
193	152 153 192	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ )
194	169	recld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
195	194	recnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℂ )
196		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
197		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
198		iccntr	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 [,] 𝑏 ) ) = ( 𝑎 (,) 𝑏 ) )
199	68 70 198	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 [,] 𝑏 ) ) = ( 𝑎 (,) 𝑏 ) )
200	199	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 [,] 𝑏 ) ) = ( 𝑎 (,) 𝑏 ) )
201	191 193 195 196 197 200	dvmptntr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) = ( ℝ D ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) )
202		ioossicc	⊢ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑎 [,] 𝑏 )
203	202	sseli	⊢ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑎 [,] 𝑏 ) )
204	203 169	sylan2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
205		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ V )
206		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
207	206	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ℝ ∈ { ℝ , ℂ } )
208	203 164	sylan2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
209	93	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 (,) 𝐵 ) )
210	209	sselda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
211	100	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
212	211	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℂ )
213	210 212	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℂ )
214	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
215		ioossre	⊢ ( 𝑎 (,) 𝑏 ) ⊆ ℝ
216	215	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ℝ )
217	197 196	dvres	⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝑎 (,) 𝑏 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑎 (,) 𝑏 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 (,) 𝑏 ) ) ) )
218	191 162 214 216 217	syl22anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑎 (,) 𝑏 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 (,) 𝑏 ) ) ) )
219		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
220		iooretop	⊢ ( 𝑎 (,) 𝑏 ) ∈ ( topGen ‘ ran (,) )
221		isopn3i	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝑎 (,) 𝑏 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 (,) 𝑏 ) ) = ( 𝑎 (,) 𝑏 ) )
222	219 220 221	mp2an	⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 (,) 𝑏 ) ) = ( 𝑎 (,) 𝑏 )
223	222	reseq2i	⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑎 (,) 𝑏 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) )
224	218 223	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑎 (,) 𝑏 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) )
225	202 160	sstrid	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ ( 𝐴 [,] 𝐵 ) )
226	162 225	feqresmpt	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐹 ↾ ( 𝑎 (,) 𝑏 ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
227	226	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑎 (,) 𝑏 ) ) ) = ( ℝ D ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
228	100	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
229	228 93	fssresd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) : ( 𝑎 (,) 𝑏 ) ⟶ ℂ )
230	229	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) ‘ 𝑦 ) ) )
231	230	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) ‘ 𝑦 ) ) )
232		fvres	⊢ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
233	232	mpteq2ia	⊢ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) ‘ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
234	231 233	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ℝ D 𝐹 ) ↾ ( 𝑎 (,) 𝑏 ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
235	224 227 234	3eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
236	207 208 213 235 141 167	dvmptdivc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
237	204 205 236	dvmptre	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
238	201 237	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
239	238	dmeqd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → dom ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) = dom ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
240		dmmptg	⊢ ( ∀ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V → dom ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( 𝑎 (,) 𝑏 ) )
241		fvex	⊢ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V
242	241	a1i	⊢ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V )
243	240 242	mprg	⊢ dom ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( 𝑎 (,) 𝑏 )
244	239 243	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → dom ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) = ( 𝑎 (,) 𝑏 ) )
245	152 153 151 190 244	mvth	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ∃ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ( ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) / ( 𝑏 − 𝑎 ) ) )
246	238	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑥 ) )
247		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
248	247	fvoveq1d	⊢ ( 𝑦 = 𝑥 → ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
249		eqid	⊢ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
250		fvex	⊢ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V
251	248 249 250	fvmpt	⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ↦ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑥 ) = ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
252	246 251	sylan9eq	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) ‘ 𝑥 ) = ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
253		ubicc2	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝑎 ≤ 𝑏 ) → 𝑏 ∈ ( 𝑎 [,] 𝑏 ) )
254	69 71 112 253	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ( 𝑎 [,] 𝑏 ) )
255	254	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑏 ∈ ( 𝑎 [,] 𝑏 ) )
256	21	fvoveq1d	⊢ ( 𝑦 = 𝑏 → ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
257		eqid	⊢ ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
258		fvex	⊢ ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V
259	256 257 258	fvmpt	⊢ ( 𝑏 ∈ ( 𝑎 [,] 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
260	255 259	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
261		lbicc2	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝑎 ≤ 𝑏 ) → 𝑎 ∈ ( 𝑎 [,] 𝑏 ) )
262	69 71 112 261	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ( 𝑎 [,] 𝑏 ) )
263	262	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑎 ∈ ( 𝑎 [,] 𝑏 ) )
264	30	fvoveq1d	⊢ ( 𝑦 = 𝑎 → ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
265		fvex	⊢ ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ V
266	264 257 265	fvmpt	⊢ ( 𝑎 ∈ ( 𝑎 [,] 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
267	263 266	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) = ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
268	260 267	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) = ( ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) − ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
269	61	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
270	269 141 167	divcld	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
271	63	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
272	271 141 167	divcld	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
273	270 272	resubd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℜ ‘ ( ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) − ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) − ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) )
274	269 271 141 167	divsubdird	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) − ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
275	141 167	dividd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = 1 )
276	274 275	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) − ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = 1 )
277	276	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℜ ‘ ( ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) − ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = ( ℜ ‘ 1 ) )
278		re1	⊢ ( ℜ ‘ 1 ) = 1
279	277 278	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ℜ ‘ ( ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) − ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = 1 )
280	273 279	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) − ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = 1 )
281	280	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( 𝐹 ‘ 𝑏 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) − ( ℜ ‘ ( ( 𝐹 ‘ 𝑎 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) = 1 )
282	268 281	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) = 1 )
283	282	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) / ( 𝑏 − 𝑎 ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) )
284	252 283	eqeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) / ( 𝑏 − 𝑎 ) ) ↔ ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) ) )
285	284	rexbidva	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ∃ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ( ( ℝ D ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑏 ) − ( ( 𝑦 ∈ ( 𝑎 [,] 𝑏 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑦 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ) ‘ 𝑎 ) ) / ( 𝑏 − 𝑎 ) ) ↔ ∃ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) ) )
286	245 285	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ∃ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) )
287	209	sselda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
288	211	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
289	287 288	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
290	140	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
291	167	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ≠ 0 )
292	289 290 291	divcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℂ )
293	292	recld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
294	142	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℝ )
295	293 294	remulcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
296	289	abscld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
297	125	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑀 ∈ ℝ )
298	292	abscld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
299	141	absge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) )
300	299	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) )
301	292	releabsd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ ( abs ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
302	293 298 294 300 301	lemul1ad	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
303	292 290	absmuld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) · ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
304	289 290 291	divcan1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) · ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
305	304	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) · ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
306	303 305	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
307	302 306	breqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
308	6	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
309	287 308	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
310	295 296 297 307 309	letrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 )
311		oveq1	⊢ ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) )
312	311	breq1d	⊢ ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) → ( ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 ↔ ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 ) )
313	310 312	syl5ibcom	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) → ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 ) )
314	313	rexlimdva	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ∃ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ( ℜ ‘ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) / ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) = ( 1 / ( 𝑏 − 𝑎 ) ) → ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 ) )
315	286 314	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( 1 / ( 𝑏 − 𝑎 ) ) · ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ) ≤ 𝑀 )
316	157 315	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ≤ 𝑀 )
317	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → 𝑀 ∈ ℝ )
318		ledivmul2	⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( ( 𝑏 − 𝑎 ) ∈ ℝ ∧ 0 < ( 𝑏 − 𝑎 ) ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
319	142 317 144 155 318	syl112anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) ) )
320	316 319	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ≠ ( 𝐹 ‘ 𝑎 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
321	139 320	pm2.61dane	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
322	68 70 112	abssubge0d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( 𝑏 − 𝑎 ) )
323	322	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝑀 · ( 𝑏 − 𝑎 ) ) )
324	321 323	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑎 ≤ 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) )
325	29 38 40 58 324	wlogle	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) )
326	325	expcom	⊢ ( ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
327	14 20 326	vtocl2ga	⊢ ( ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) ) )
328	327	ancoms	⊢ ( ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) ) )
329	328	impcom	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑋 ) − ( 𝐹 ‘ 𝑌 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑋 − 𝑌 ) ) ) )