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	$⊢ φ \to A \in ℝ$
	c1lip2.b	$⊢ φ \to B \in ℝ$
	c1lip2.f	$⊢ φ \to F \in C^{n} (ℝ) (1)$
	c1lip2.rn	$⊢ φ \to ran F \subseteq ℝ$
	c1lip2.dm	$⊢ φ \to [A, B] \subseteq dom F$
Assertion	c1lip2	$⊢ φ \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$

Proof

Step	Hyp	Ref	Expression
1		c1lip2.a	$⊢ φ \to A \in ℝ$
2		c1lip2.b	$⊢ φ \to B \in ℝ$
3		c1lip2.f	$⊢ φ \to F \in C^{n} (ℝ) (1)$
4		c1lip2.rn	$⊢ φ \to ran F \subseteq ℝ$
5		c1lip2.dm	$⊢ φ \to [A, B] \subseteq dom F$
6		ax-resscn	$⊢ ℝ \subseteq ℂ$
7		1nn0	$⊢ 1 \in ℕ_{0}$
8		elcpn	$⊢ (ℝ \subseteq ℂ \land 1 \in ℕ_{0}) \to (F \in C^{n} (ℝ) (1) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (ℝ D^{n} F) (1) : dom F \underset{cn}{⟶} ℂ))$
9	6 7 8	mp2an	$⊢ F \in C^{n} (ℝ) (1) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (ℝ D^{n} F) (1) : dom F \underset{cn}{⟶} ℂ)$
10	9	simplbi	$⊢ F \in C^{n} (ℝ) (1) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
11	3 10	syl	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
12		pmfun	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to Fun F$
13	11 12	syl	$⊢ φ \to Fun F$
14	13	funfnd	$⊢ φ \to F Fn dom F$
15		df-f	$⊢ F : dom F ⟶ ℝ \leftrightarrow (F Fn dom F \land ran F \subseteq ℝ)$
16	14 4 15	sylanbrc	$⊢ φ \to F : dom F ⟶ ℝ$
17		cnex	$⊢ ℂ \in V$
18		reex	$⊢ ℝ \in V$
19	17 18	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
20	19	simprbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
21	11 20	syl	$⊢ φ \to dom F \subseteq ℝ$
22		dvfre	$⊢ (F : dom F ⟶ ℝ \land dom F \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
23	16 21 22	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
24		0p1e1	$⊢ 0 + 1 = 1$
25	24	fveq2i	$⊢ (ℝ D^{n} F) (0 + 1) = (ℝ D^{n} F) (1)$
26		0nn0	$⊢ 0 \in ℕ_{0}$
27		dvnp1	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land 0 \in ℕ_{0}) \to (ℝ D^{n} F) (0 + 1) = ℝ D (ℝ D^{n} F) (0)$
28	6 26 27	mp3an13	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to (ℝ D^{n} F) (0 + 1) = ℝ D (ℝ D^{n} F) (0)$
29	11 28	syl	$⊢ φ \to (ℝ D^{n} F) (0 + 1) = ℝ D (ℝ D^{n} F) (0)$
30	25 29	eqtr3id	$⊢ φ \to (ℝ D^{n} F) (1) = ℝ D (ℝ D^{n} F) (0)$
31		dvn0	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ)) \to (ℝ D^{n} F) (0) = F$
32	6 11 31	sylancr	$⊢ φ \to (ℝ D^{n} F) (0) = F$
33	32	oveq2d	$⊢ φ \to ℝ D (ℝ D^{n} F) (0) = ℝ D F$
34	30 33	eqtrd	$⊢ φ \to (ℝ D^{n} F) (1) = ℝ D F$
35	9	simprbi	$⊢ F \in C^{n} (ℝ) (1) \to (ℝ D^{n} F) (1) : dom F \underset{cn}{⟶} ℂ$
36	3 35	syl	$⊢ φ \to (ℝ D^{n} F) (1) : dom F \underset{cn}{⟶} ℂ$
37	34 36	eqeltrrd	$⊢ φ \to F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℂ$
38		cncff	$⊢ F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : dom F ⟶ ℂ$
39		fdm	$⊢ F_{ℝ}^{'} : dom F ⟶ ℂ \to dom F_{ℝ}^{'} = dom F$
40	37 38 39	3syl	$⊢ φ \to dom F_{ℝ}^{'} = dom F$
41	40	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : dom F ⟶ ℝ)$
42	23 41	mpbid	$⊢ φ \to F_{ℝ}^{'} : dom F ⟶ ℝ$
43		cncffvrn	$⊢ (ℝ \subseteq ℂ \land F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℂ) \to (F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℝ \leftrightarrow F_{ℝ}^{'} : dom F ⟶ ℝ)$
44	6 37 43	sylancr	$⊢ φ \to (F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℝ \leftrightarrow F_{ℝ}^{'} : dom F ⟶ ℝ)$
45	42 44	mpbird	$⊢ φ \to F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℝ$
46		rescncf	$⊢ [A, B] \subseteq dom F \to (F_{ℝ}^{'} : dom F \underset{cn}{⟶} ℝ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ)$
47	5 45 46	sylc	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
48	18	prid1	$⊢ ℝ \in \{ℝ, ℂ\}$
49		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
50		cpnord	$⊢ (ℝ \in \{ℝ, ℂ\} \land 0 \in ℕ_{0} \land 1 \in ℤ_{\geq 0}) \to C^{n} (ℝ) (1) \subseteq C^{n} (ℝ) (0)$
51	48 26 49 50	mp3an	$⊢ C^{n} (ℝ) (1) \subseteq C^{n} (ℝ) (0)$
52	51 3	sselid	$⊢ φ \to F \in C^{n} (ℝ) (0)$
53		elcpn	$⊢ (ℝ \subseteq ℂ \land 0 \in ℕ_{0}) \to (F \in C^{n} (ℝ) (0) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (ℝ D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ))$
54	6 26 53	mp2an	$⊢ F \in C^{n} (ℝ) (0) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (ℝ D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ)$
55	54	simprbi	$⊢ F \in C^{n} (ℝ) (0) \to (ℝ D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ$
56	52 55	syl	$⊢ φ \to (ℝ D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ$
57	32 56	eqeltrrd	$⊢ φ \to F : dom F \underset{cn}{⟶} ℂ$
58		cncffvrn	$⊢ (ℝ \subseteq ℂ \land F : dom F \underset{cn}{⟶} ℂ) \to (F : dom F \underset{cn}{⟶} ℝ \leftrightarrow F : dom F ⟶ ℝ)$
59	6 57 58	sylancr	$⊢ φ \to (F : dom F \underset{cn}{⟶} ℝ \leftrightarrow F : dom F ⟶ ℝ)$
60	16 59	mpbird	$⊢ φ \to F : dom F \underset{cn}{⟶} ℝ$
61		rescncf	$⊢ [A, B] \subseteq dom F \to (F : dom F \underset{cn}{⟶} ℝ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ)$
62	5 60 61	sylc	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
63	1 2 11 47 62	c1lip1	$⊢ φ \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$

Metamath Proof Explorer

Theorem c1lip2

Proof