c1lip2

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

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

Proof

Step	Hyp	Ref	Expression
1		c1lip2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		c1lip2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		c1lip2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) )
4		c1lip2.rn	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
5		c1lip2.dm	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
6		ax-resscn	⊢ ℝ ⊆ ℂ
7		1nn0	⊢ 1 ∈ ℕ₀
8		elcpn	⊢ ( ( ℝ ⊆ ℂ ∧ 1 ∈ ℕ₀ ) → ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
9	6 7 8	mp2an	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
10	9	simplbi	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
11	3 10	syl	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
12		pmfun	⊢ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) → Fun 𝐹 )
13	11 12	syl	⊢ ( 𝜑 → Fun 𝐹 )
14	13	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
15		df-f	⊢ ( 𝐹 : dom 𝐹 ⟶ ℝ ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ℝ ) )
16	14 4 15	sylanbrc	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
17		cnex	⊢ ℂ ∈ V
18		reex	⊢ ℝ ∈ V
19	17 18	elpm2	⊢ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
20	19	simprbi	⊢ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) → dom 𝐹 ⊆ ℝ )
21	11 20	syl	⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
22		dvfre	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
23	16 21 22	syl2anc	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
24		0p1e1	⊢ ( 0 + 1 ) = 1
25	24	fveq2i	⊢ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ( ℝ D^𝑛 𝐹 ) ‘ 1 )
26		0nn0	⊢ 0 ∈ ℕ₀
27		dvnp1	⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 0 ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ) )
28	6 26 27	mp3an13	⊢ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ) )
29	11 28	syl	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ) )
30	25 29	syl5eqr	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ) )
31		dvn0	⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
32	6 11 31	sylancr	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
33	32	oveq2d	⊢ ( 𝜑 → ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ) = ( ℝ D 𝐹 ) )
34	30 33	eqtrd	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) = ( ℝ D 𝐹 ) )
35	9	simprbi	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
36	3 35	syl	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
37	34 36	eqeltrrd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
38		cncff	⊢ ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) → ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℂ )
39		fdm	⊢ ( ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℂ → dom ( ℝ D 𝐹 ) = dom 𝐹 )
40	37 38 39	3syl	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom 𝐹 )
41	40	feq2d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) )
42	23 41	mpbid	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ )
43		cncffvrn	⊢ ( ( ℝ ⊆ ℂ ∧ ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) )
44	6 37 43	sylancr	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) )
45	42 44	mpbird	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) )
46		rescncf	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) )
47	5 45 46	sylc	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
48	18	prid1	⊢ ℝ ∈ { ℝ , ℂ }
49		1eluzge0	⊢ 1 ∈ ( ℤ_≥ ‘ 0 )
50		cpnord	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 0 ∈ ℕ₀ ∧ 1 ∈ ( ℤ_≥ ‘ 0 ) ) → ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) ⊆ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 ) )
51	48 26 49 50	mp3an	⊢ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 1 ) ⊆ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 )
52	51 3	sseldi	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 ) )
53		elcpn	⊢ ( ( ℝ ⊆ ℂ ∧ 0 ∈ ℕ₀ ) → ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
54	6 26 53	mp2an	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
55	54	simprbi	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℝ ) ‘ 0 ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
56	52 55	syl	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
57	32 56	eqeltrrd	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
58		cncffvrn	⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) ) → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) ↔ 𝐹 : dom 𝐹 ⟶ ℝ ) )
59	6 57 58	sylancr	⊢ ( 𝜑 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) ↔ 𝐹 : dom 𝐹 ⟶ ℝ ) )
60	16 59	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) )
61		rescncf	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) )
62	5 60 61	sylc	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
63	1 2 11 47 62	c1lip1	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem c1lip2

Proof