Metamath Proof Explorer

Theorem c1liplem1

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

Ref Expression
Hypotheses c1liplem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
c1liplem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
c1liplem1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
c1liplem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
c1liplem1.dv ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
c1liplem1.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
c1liplem1.k ⊢ 𝐾 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < )
Assertion c1liplem1 ( 𝜑 → ( 𝐾 ∈ ℝ ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 c1liplem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 c1liplem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 c1liplem1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 c1liplem1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
5 c1liplem1.dv ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
6 c1liplem1.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
7 c1liplem1.k ⊢ 𝐾 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < )
8 imassrn ⊢ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ran abs
9 absf ⊢ abs : ℂ ⟶ ℝ
10 frn ⊢ ( abs : ℂ ⟶ ℝ → ran abs ⊆ ℝ )
11 9 10 ax-mp ⊢ ran abs ⊆ ℝ
12 8 11 sstri ⊢ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ
13 12 a1i ⊢ ( 𝜑 → ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
14 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
15 ffun ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ → Fun ( ℝ D 𝐹 ) )
16 14 15 ax-mp ⊢ Fun ( ℝ D 𝐹 )
17 16 a1i ⊢ ( 𝜑 → Fun ( ℝ D 𝐹 ) )
18 cncff ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
19 fdm ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
20 5 18 19 3syl ⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
21 ssdmres ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 [,] 𝐵 ) )
22 20 21 sylibr ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) )
23 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
24 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
25 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
26 23 24 3 25 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
27 funfvima2 ⊢ ( ( Fun ( ℝ D 𝐹 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
28 27 imp ⊢ ( ( ( Fun ( ℝ D 𝐹 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ) ∧ 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
29 17 22 26 28 syl21anc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
30 ffun ⊢ ( abs : ℂ ⟶ ℝ → Fun abs )
31 9 30 ax-mp ⊢ Fun abs
32 imassrn ⊢ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ⊆ ran ( ℝ D 𝐹 )
33 frn ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ → ran ( ℝ D 𝐹 ) ⊆ ℂ )
34 14 33 ax-mp ⊢ ran ( ℝ D 𝐹 ) ⊆ ℂ
35 32 34 sstri ⊢ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℂ
36 9 fdmi ⊢ dom abs = ℂ
37 35 36 sseqtrri ⊢ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ⊆ dom abs
38 funfvima2 ⊢ ( ( Fun abs ∧ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ⊆ dom abs ) → ( ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ) )
39 31 37 38 mp2an ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
40 ne0i ⊢ ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝐴 ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ≠ ∅ )
41 29 39 40 3syl ⊢ ( 𝜑 → ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ≠ ∅ )
42 ax-resscn ⊢ ℝ ⊆ ℂ
43 ssid ⊢ ℂ ⊆ ℂ
44 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
45 42 43 44 mp2an ⊢ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
46 45 5 sselid ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
47 cniccbdd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 )
48 1 2 46 47 syl3anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 )
49 fvelima ⊢ ( ( Fun abs ∧ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ) → ∃ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ( abs ‘ 𝑦 ) = 𝑏 )
50 31 49 mpan ⊢ ( 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ( abs ‘ 𝑦 ) = 𝑏 )
51 fvres ⊢ ( 𝑏 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) = ( ( ℝ D 𝐹 ) ‘ 𝑏 ) )
52 51 adantl ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) = ( ( ℝ D 𝐹 ) ‘ 𝑏 ) )
53 52 fveq2d ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑏 ) ) )
54 2fveq3 ⊢ ( 𝑥 = 𝑏 → ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) ) )
55 54 breq1d ⊢ ( 𝑥 = 𝑏 → ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ↔ ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) ) ≤ 𝑎 ) )
56 55 rspccva ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑏 ) ) ≤ 𝑎 )
57 53 56 eqbrtrrd ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑏 ) ) ≤ 𝑎 )
58 57 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑏 ) ) ≤ 𝑎 )
59 fveq2 ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑏 ) ) = ( abs ‘ 𝑦 ) )
60 59 breq1d ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑏 ) ) ≤ 𝑎 ↔ ( abs ‘ 𝑦 ) ≤ 𝑎 ) )
61 58 60 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 → ( abs ‘ 𝑦 ) ≤ 𝑎 ) )
62 61 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 → ( abs ‘ 𝑦 ) ≤ 𝑎 ) )
63 fvelima ⊢ ( ( Fun ( ℝ D 𝐹 ) ∧ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 )
64 16 63 mpan ⊢ ( 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) → ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑏 ) = 𝑦 )
65 62 64 impel ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) ∧ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ 𝑦 ) ≤ 𝑎 )
66 breq1 ⊢ ( ( abs ‘ 𝑦 ) = 𝑏 → ( ( abs ‘ 𝑦 ) ≤ 𝑎 ↔ 𝑏 ≤ 𝑎 ) )
67 65 66 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) ∧ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ 𝑦 ) = 𝑏 → 𝑏 ≤ 𝑎 ) )
68 67 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( ∃ 𝑦 ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ( abs ‘ 𝑦 ) = 𝑏 → 𝑏 ≤ 𝑎 ) )
69 50 68 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → 𝑏 ≤ 𝑎 ) )
70 69 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∀ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) 𝑏 ≤ 𝑎 )
71 70 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 → ∀ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) 𝑏 ≤ 𝑎 ) )
72 71 reximdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ) ≤ 𝑎 → ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) 𝑏 ≤ 𝑎 ) )
73 48 72 mpd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) 𝑏 ≤ 𝑎 )
74 13 41 73 suprcld ⊢ ( 𝜑 → sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) ∈ ℝ )
75 7 74 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
76 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
77 76 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
78 cncff ⊢ ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
79 6 78 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
81 80 76 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ∈ ℝ )
82 81 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ∈ ℂ )
83 77 82 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
84 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
85 84 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
86 80 84 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ∈ ℝ )
87 86 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ∈ ℂ )
88 85 87 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
89 83 88 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
90 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
91 1 2 90 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
92 91 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
93 92 76 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ )
94 92 84 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ )
95 93 94 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℝ )
96 95 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
97 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
98 difrp ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ ( 𝑦 − 𝑥 ) ∈ ℝ+ ) )
99 94 93 98 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 < 𝑦 ↔ ( 𝑦 − 𝑥 ) ∈ ℝ+ ) )
100 97 99 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℝ+ )
101 100 rpne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ≠ 0 )
102 89 96 101 absdivd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
103 12 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
104 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ≠ ∅ )
105 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) 𝑏 ≤ 𝑎 )
106 31 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → Fun abs )
107 89 96 101 divcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ℂ )
108 107 36 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ dom abs )
109 94 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ* )
110 93 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ* )
111 94 93 97 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ≤ 𝑦 )
112 ubicc2 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ ( 𝑥 [,] 𝑦 ) )
113 109 110 111 112 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 𝑥 [,] 𝑦 ) )
114 113 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
115 lbicc2 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ ( 𝑥 [,] 𝑦 ) )
116 109 110 111 115 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 𝑥 [,] 𝑦 ) )
117 116 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
118 114 117 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) )
119 118 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) )
120 iccss2 ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) )
121 120 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) )
122 121 resabs1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( 𝑥 [,] 𝑦 ) ) = ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) )
123 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
124 rescncf ⊢ ( ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( 𝑥 [,] 𝑦 ) ) ∈ ( ( 𝑥 [,] 𝑦 ) –cn→ ℝ ) ) )
125 121 123 124 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( 𝑥 [,] 𝑦 ) ) ∈ ( ( 𝑥 [,] 𝑦 ) –cn→ ℝ ) )
126 122 125 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ∈ ( ( 𝑥 [,] 𝑦 ) –cn→ ℝ ) )
127 42 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ℝ ⊆ ℂ )
128 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
129 cnex ⊢ ℂ ∈ V
130 reex ⊢ ℝ ∈ V
131 129 130 elpm2 ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
132 131 simplbi ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → 𝐹 : dom 𝐹 ⟶ ℂ )
133 128 132 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝐹 : dom 𝐹 ⟶ ℂ )
134 131 simprbi ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → dom 𝐹 ⊆ ℝ )
135 128 134 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → dom 𝐹 ⊆ ℝ )
136 iccssre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 [,] 𝑦 ) ⊆ ℝ )
137 94 93 136 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 [,] 𝑦 ) ⊆ ℝ )
138 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
139 138 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
140 138 139 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) ∧ ( dom 𝐹 ⊆ ℝ ∧ ( 𝑥 [,] 𝑦 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) ) )
141 127 133 135 137 140 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) ) )
142 iccntr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
143 94 93 142 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
144 143 reseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) )
145 141 144 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) )
146 145 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → dom ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) )
147 ioossicc ⊢ ( 𝑥 (,) 𝑦 ) ⊆ ( 𝑥 [,] 𝑦 )
148 147 121 sstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 (,) 𝑦 ) ⊆ ( 𝐴 [,] 𝐵 ) )
149 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) )
150 148 149 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) )
151 ssdmres ⊢ ( ( 𝑥 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
152 150 151 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → dom ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
153 146 152 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → dom ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) = ( 𝑥 (,) 𝑦 ) )
154 94 93 97 126 153 mvth ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ∃ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) )
155 145 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) ‘ 𝑎 ) )
156 155 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) ‘ 𝑎 ) )
157 fvres ⊢ ( 𝑎 ∈ ( 𝑥 (,) 𝑦 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) ‘ 𝑎 ) = ( ( ℝ D 𝐹 ) ‘ 𝑎 ) )
158 157 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝑥 (,) 𝑦 ) ) ‘ 𝑎 ) = ( ( ℝ D 𝐹 ) ‘ 𝑎 ) )
159 156 158 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ℝ D 𝐹 ) ‘ 𝑎 ) )
160 16 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → Fun ( ℝ D 𝐹 ) )
161 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) )
162 148 sseld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑎 ∈ ( 𝑥 (,) 𝑦 ) → 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ) )
163 162 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → 𝑎 ∈ ( 𝐴 [,] 𝐵 ) )
164 funfvima2 ⊢ ( ( Fun ( ℝ D 𝐹 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ℝ D 𝐹 ) ‘ 𝑎 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
165 164 imp ⊢ ( ( ( Fun ( ℝ D 𝐹 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ) ∧ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑎 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
166 160 161 163 165 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑎 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
167 159 166 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
168 eleq1 ⊢ ( ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
169 167 168 syl5ibcom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝑥 < 𝑦 ∧ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
170 169 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑎 ∈ ( 𝑥 (,) 𝑦 ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ) )
171 170 rexlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ∃ 𝑎 ∈ ( 𝑥 (,) 𝑦 ) ( ( ℝ D ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ) ‘ 𝑎 ) = ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
172 154 171 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ( 𝑥 [,] 𝑦 ) ) ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
173 119 172 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) )
174 funfvima ⊢ ( ( Fun abs ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ dom abs ) → ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) ) )
175 174 imp ⊢ ( ( ( Fun abs ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ dom abs ) ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
176 106 108 173 175 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) ∈ ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) )
177 103 104 105 176 suprubd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) ≤ sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) )
178 177 7 breqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ) ≤ 𝐾 )
179 102 178 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ≤ 𝐾 )
180 89 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
181 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝐾 ∈ ℝ )
182 96 101 absrpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( 𝑦 − 𝑥 ) ) ∈ ℝ+ )
183 180 181 182 ledivmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ≤ 𝐾 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( 𝑦 − 𝑥 ) ) · 𝐾 ) ) )
184 179 183 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( 𝑦 − 𝑥 ) ) · 𝐾 ) )
185 182 rpcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( 𝑦 − 𝑥 ) ) ∈ ℂ )
186 181 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝐾 ∈ ℂ )
187 185 186 mulcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( abs ‘ ( 𝑦 − 𝑥 ) ) · 𝐾 ) = ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
188 184 187 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
189 188 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
190 189 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
191 75 190 jca ⊢ ( 𝜑 → ( 𝐾 ∈ ℝ ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝐾 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) ) )