This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝑋 − 𝑌 ) ) ) )