c1lip3

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

	Ref	Expression
Hypotheses	c1lip3.a	$⊢ φ \to A \in ℝ$
	c1lip3.b	$⊢ φ \to B \in ℝ$
	c1lip3.f	$⊢ φ \to {F ↾}_{ℝ} \in C^{n} (ℝ) (1)$
	c1lip3.rn	$⊢ φ \to F [ℝ] \subseteq ℝ$
	c1lip3.dm	$⊢ φ \to [A, B] \subseteq dom F$
Assertion	c1lip3	$⊢ φ \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		c1lip3.a	$⊢ φ \to A \in ℝ$
2		c1lip3.b	$⊢ φ \to B \in ℝ$
3		c1lip3.f	$⊢ φ \to {F ↾}_{ℝ} \in C^{n} (ℝ) (1)$
4		c1lip3.rn	$⊢ φ \to F [ℝ] \subseteq ℝ$
5		c1lip3.dm	$⊢ φ \to [A, B] \subseteq dom F$
6		df-ima	$⊢ F [ℝ] = ran ({F ↾}_{ℝ})$
7	6 4	eqsstrrid	$⊢ φ \to ran ({F ↾}_{ℝ}) \subseteq ℝ$
8		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
9	1 2 8	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
10	9 5	ssind	$⊢ φ \to [A, B] \subseteq ℝ \cap dom F$
11		dmres	$⊢ dom ({F ↾}_{ℝ}) = ℝ \cap dom F$
12	10 11	sseqtrrdi	$⊢ φ \to [A, B] \subseteq dom ({F ↾}_{ℝ})$
13	1 2 3 7 12	c1lip2	$⊢ φ \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\|$
14	9	sseld	$⊢ φ \to (x \in [A, B] \to x \in ℝ)$
15	9	sseld	$⊢ φ \to (y \in [A, B] \to y \in ℝ)$
16	14 15	anim12d	$⊢ φ \to ((x \in [A, B] \land y \in [A, B]) \to (x \in ℝ \land y \in ℝ))$
17	16	imp	$⊢ (φ \land (x \in [A, B] \land y \in [A, B])) \to (x \in ℝ \land y \in ℝ)$
18		fvres	$⊢ y \in ℝ \to ({F ↾}_{ℝ}) (y) = F (y)$
19		fvres	$⊢ x \in ℝ \to ({F ↾}_{ℝ}) (x) = F (x)$
20	18 19	oveqan12rd	$⊢ (x \in ℝ \land y \in ℝ) \to ({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x) = F (y) - F (x)$
21	20	fveq2d	$⊢ (x \in ℝ \land y \in ℝ) \to \|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| = \|F (y) - F (x)\|$
22	21	breq1d	$⊢ (x \in ℝ \land y \in ℝ) \to (\|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\| \leftrightarrow \|F (y) - F (x)\| \leq k \|y - x\|)$
23	22	biimpd	$⊢ (x \in ℝ \land y \in ℝ) \to (\|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\| \to \|F (y) - F (x)\| \leq k \|y - x\|)$
24	17 23	syl	$⊢ (φ \land (x \in [A, B] \land y \in [A, B])) \to (\|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\| \to \|F (y) - F (x)\| \leq k \|y - x\|)$
25	24	ralimdvva	$⊢ φ \to (\forall x \in [A, B] \forall y \in [A, B] \|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\| \to \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|)$
26	25	reximdv	$⊢ φ \to (\exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|({F ↾}_{ℝ}) (y) - ({F ↾}_{ℝ}) (x)\| \leq k \|y - x\| \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|)$
27	13 26	mpd	$⊢ φ \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 c1lip3

Proof