Metamath Proof Explorer

Theorem c1lip1

Description: C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses c1lip1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
c1lip1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
c1lip1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
c1lip1.dv ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
c1lip1.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
Assertion c1lip1 ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 c1lip1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 c1lip1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 c1lip1.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
4 c1lip1.dv ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 c1lip1.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
6 0re ⊢ 0 ∈ ℝ
7 6 ne0ii ⊢ ℝ ≠ ∅
8 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) )
9 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
10 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
11 icc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
12 9 10 11 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
13 12 biimpar ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
14 13 raleqdv ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
15 8 14 mpbiri ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
16 15 ralrimivw ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ∀ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
17 r19.2z ⊢ ( ( ℝ ≠ ∅ ∧ ∀ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
18 7 16 17 sylancr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
19 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
20 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
21 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
22 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
25 eqid ⊢ sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < )
26 19 20 21 22 23 24 25 c1liplem1 ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) ∈ ℝ ∧ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ) )
27 oveq1 ⊢ ( 𝑘 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) → ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) )
28 27 breq2d ⊢ ( 𝑘 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
29 28 imbi2d ⊢ ( 𝑘 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) → ( ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ↔ ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ) )
30 29 2ralbidv ⊢ ( 𝑘 = sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ↔ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ) )
31 30 rspcev ⊢ ( ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) ∈ ℝ ∧ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( sup ( ( abs “ ( ( ℝ D 𝐹 ) “ ( 𝐴 [,] 𝐵 ) ) ) , ℝ , < ) · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
32 26 31 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) )
33 breq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 < 𝑏 ↔ 𝑥 < 𝑏 ) )
34 fveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑥 ) )
35 34 oveq2d ⊢ ( 𝑎 = 𝑥 → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) )
36 35 fveq2d ⊢ ( 𝑎 = 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
37 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑥 ) )
38 37 fveq2d ⊢ ( 𝑎 = 𝑥 → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑥 ) ) )
39 38 oveq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) )
40 36 39 breq12d ⊢ ( 𝑎 = 𝑥 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) ) )
41 33 40 imbi12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ↔ ( 𝑥 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) ) ) )
42 breq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑥 < 𝑏 ↔ 𝑥 < 𝑦 ) )
43 fveq2 ⊢ ( 𝑏 = 𝑦 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑦 ) )
44 43 fvoveq1d ⊢ ( 𝑏 = 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
45 fvoveq1 ⊢ ( 𝑏 = 𝑦 → ( abs ‘ ( 𝑏 − 𝑥 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
46 45 oveq2d ⊢ ( 𝑏 = 𝑦 → ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
47 44 46 breq12d ⊢ ( 𝑏 = 𝑦 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
48 42 47 imbi12d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑥 ) ) ) ) ↔ ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) ) )
49 41 48 rspc2v ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) ) )
50 49 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) ) )
51 pm2.27 ⊢ ( 𝑥 < 𝑦 → ( ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
52 51 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑥 < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
53 50 52 syld ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
54 0le0 ⊢ 0 ≤ 0
55 fvres ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
56 55 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
57 cncff ⊢ ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
58 5 57 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
60 simpl ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
61 ffvelrn ⊢ ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ∈ ℝ )
62 59 60 61 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑥 ) ∈ ℝ )
63 56 62 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
64 63 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
65 64 subidd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) = 0 )
66 65 abs00bd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) = 0 )
67 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
68 1 2 67 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
69 68 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
70 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
71 69 70 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ℝ )
72 71 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ℂ )
73 72 subidd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 − 𝑥 ) = 0 )
74 73 abs00bd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑥 − 𝑥 ) ) = 0 )
75 74 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) = ( 𝑘 · 0 ) )
76 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑘 ∈ ℝ )
77 76 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑘 ∈ ℂ )
78 77 mul01d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑘 · 0 ) = 0 )
79 75 78 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) = 0 )
80 66 79 breq12d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) ↔ 0 ≤ 0 ) )
81 54 80 mpbiri ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) )
82 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
83 82 fvoveq1d ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
84 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( 𝑥 − 𝑥 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
85 84 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
86 83 85 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
87 81 86 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 = 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
88 87 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 = 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
89 88 a1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 = 𝑦 ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
90 breq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 < 𝑏 ↔ 𝑦 < 𝑏 ) )
91 fveq2 ⊢ ( 𝑎 = 𝑦 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑦 ) )
92 91 oveq2d ⊢ ( 𝑎 = 𝑦 → ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) )
93 92 fveq2d ⊢ ( 𝑎 = 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) )
94 oveq2 ⊢ ( 𝑎 = 𝑦 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑦 ) )
95 94 fveq2d ⊢ ( 𝑎 = 𝑦 → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑦 ) ) )
96 95 oveq2d ⊢ ( 𝑎 = 𝑦 → ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) )
97 93 96 breq12d ⊢ ( 𝑎 = 𝑦 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) ) )
98 90 97 imbi12d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) ↔ ( 𝑦 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) ) ) )
99 breq2 ⊢ ( 𝑏 = 𝑥 → ( 𝑦 < 𝑏 ↔ 𝑦 < 𝑥 ) )
100 fveq2 ⊢ ( 𝑏 = 𝑥 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑥 ) )
101 100 fvoveq1d ⊢ ( 𝑏 = 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) )
102 fvoveq1 ⊢ ( 𝑏 = 𝑥 → ( abs ‘ ( 𝑏 − 𝑦 ) ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
103 102 oveq2d ⊢ ( 𝑏 = 𝑥 → ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) )
104 101 103 breq12d ⊢ ( 𝑏 = 𝑥 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) )
105 99 104 imbi12d ⊢ ( 𝑏 = 𝑥 → ( ( 𝑦 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑦 ) ) ) ) ↔ ( 𝑦 < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) ) )
106 98 105 rspc2v ⊢ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( 𝑦 < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) ) )
107 106 ancoms ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( 𝑦 < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) ) )
108 107 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( 𝑦 < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) ) )
109 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → 𝑦 < 𝑥 )
110 fvres ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
111 110 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
112 simpr ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
113 ffvelrn ⊢ ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ∈ ℝ )
114 59 112 113 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ∈ ℝ )
115 111 114 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
116 115 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
117 64 116 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
118 117 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
119 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
120 119 sseld ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → 𝑥 ∈ ℝ ) )
121 119 sseld ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → 𝑦 ∈ ℝ ) )
122 120 121 anim12d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
123 122 imp ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) )
124 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
125 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
126 abssub ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
127 124 125 126 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
128 123 127 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
129 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
130 129 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) = ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
131 118 130 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
132 131 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
133 109 132 embantd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( ( 𝑦 < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑥 − 𝑦 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
134 108 133 syld ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 < 𝑥 ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
135 lttri4 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) )
136 123 135 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) )
137 53 89 134 136 mpjao3dan ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
138 137 ralrimdvva ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
139 138 reximdva ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑎 < 𝑏 → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑏 − 𝑎 ) ) ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
140 32 139 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
141 18 140 2 1 ltlecasei ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )