Metamath Proof Explorer

Theorem c1lip3

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

Ref Expression
Hypotheses c1lip3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
c1lip3.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
c1lip3.f ⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) )
c1lip3.rn ⊢ ( 𝜑 → ( 𝐹 “ ℝ ) ⊆ ℝ )
c1lip3.dm ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
Assertion c1lip3 ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 c1lip3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 c1lip3.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 c1lip3.f ⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) )
4 c1lip3.rn ⊢ ( 𝜑 → ( 𝐹 “ ℝ ) ⊆ ℝ )
5 c1lip3.dm ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
6 df-ima ⊢ ( 𝐹 “ ℝ ) = ran ( 𝐹 ↾ ℝ )
7 6 4 eqsstrrid ⊢ ( 𝜑 → ran ( 𝐹 ↾ ℝ ) ⊆ ℝ )
8 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
9 1 2 8 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
10 9 5 ssind ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( ℝ ∩ dom 𝐹 ) )
11 dmres ⊢ dom ( 𝐹 ↾ ℝ ) = ( ℝ ∩ dom 𝐹 )
12 10 11 sseqtrrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom ( 𝐹 ↾ ℝ ) )
13 1 2 3 7 12 c1lip2 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )
14 9 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → 𝑥 ∈ ℝ ) )
15 9 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → 𝑦 ∈ ℝ ) )
16 14 15 anim12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
17 16 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) )
18 fvres ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
19 fvres ⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
20 18 19 oveqan12rd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) )
21 20 fveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
22 21 breq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
23 22 biimpd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
24 17 23 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
25 24 ralimdvva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
26 25 reximdv ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( 𝐹 ↾ ℝ ) ‘ 𝑦 ) − ( ( 𝐹 ↾ ℝ ) ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) )
27 13 26 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )