c1lip1

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

	Ref	Expression
Hypotheses	c1lip1.a	$⊢ φ \to A \in ℝ$
	c1lip1.b	$⊢ φ \to B \in ℝ$
	c1lip1.f	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
	c1lip1.dv	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
	c1lip1.cn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
Assertion	c1lip1	$⊢ φ \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		c1lip1.a	$⊢ φ \to A \in ℝ$
2		c1lip1.b	$⊢ φ \to B \in ℝ$
3		c1lip1.f	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
4		c1lip1.dv	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
5		c1lip1.cn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
6		0re	$⊢ 0 \in ℝ$
7	6	ne0ii	$⊢ ℝ \neq \emptyset$
8		ral0	$⊢ \forall x \in \emptyset \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$
9	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
10	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
11		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
12	9 10 11	syl2anc	$⊢ φ \to ([A, B] = \emptyset \leftrightarrow B < A)$
13	12	biimpar	$⊢ (φ \land B < A) \to [A, B] = \emptyset$
14	13	raleqdv	$⊢ (φ \land B < A) \to (\forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\| \leftrightarrow \forall x \in \emptyset \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|)$
15	8 14	mpbiri	$⊢ (φ \land B < A) \to \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$
16	15	ralrimivw	$⊢ (φ \land B < A) \to \forall k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$
17		r19.2z	$⊢ (ℝ \neq \emptyset \land \forall 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\|$
18	7 16 17	sylancr	$⊢ (φ \land B < A) \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$
19	1	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ$
20	2	adantr	$⊢ (φ \land A \leq B) \to B \in ℝ$
21		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
22	3	adantr	$⊢ (φ \land A \leq B) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
23	4	adantr	$⊢ (φ \land A \leq B) \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
24	5	adantr	$⊢ (φ \land A \leq B) \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
25		eqid	$⊢ sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <)$
26	19 20 21 22 23 24 25	c1liplem1	$⊢ (φ \land A \leq B) \to (sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \in ℝ \land \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|))$
27		oveq1	$⊢ k = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \to k \|b - a\| = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|$
28	27	breq2d	$⊢ k = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \to (\|F (b) - F (a)\| \leq k \|b - a\| \leftrightarrow \|F (b) - F (a)\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|)$
29	28	imbi2d	$⊢ k = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \to ((a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \leftrightarrow (a < b \to \|F (b) - F (a)\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|))$
30	29	2ralbidv	$⊢ k = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \leftrightarrow \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|))$
31	30	rspcev	$⊢ (sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \in ℝ \land \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \|b - a\|)) \to \exists k \in ℝ \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|)$
32	26 31	syl	$⊢ (φ \land A \leq B) \to \exists k \in ℝ \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|)$
33		breq1	$⊢ a = x \to (a < b \leftrightarrow x < b)$
34		fveq2	$⊢ a = x \to F (a) = F (x)$
35	34	oveq2d	$⊢ a = x \to F (b) - F (a) = F (b) - F (x)$
36	35	fveq2d	$⊢ a = x \to \|F (b) - F (a)\| = \|F (b) - F (x)\|$
37		oveq2	$⊢ a = x \to b - a = b - x$
38	37	fveq2d	$⊢ a = x \to \|b - a\| = \|b - x\|$
39	38	oveq2d	$⊢ a = x \to k \|b - a\| = k \|b - x\|$
40	36 39	breq12d	$⊢ a = x \to (\|F (b) - F (a)\| \leq k \|b - a\| \leftrightarrow \|F (b) - F (x)\| \leq k \|b - x\|)$
41	33 40	imbi12d	$⊢ a = x \to ((a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \leftrightarrow (x < b \to \|F (b) - F (x)\| \leq k \|b - x\|))$
42		breq2	$⊢ b = y \to (x < b \leftrightarrow x < y)$
43		fveq2	$⊢ b = y \to F (b) = F (y)$
44	43	fvoveq1d	$⊢ b = y \to \|F (b) - F (x)\| = \|F (y) - F (x)\|$
45		fvoveq1	$⊢ b = y \to \|b - x\| = \|y - x\|$
46	45	oveq2d	$⊢ b = y \to k \|b - x\| = k \|y - x\|$
47	44 46	breq12d	$⊢ b = y \to (\|F (b) - F (x)\| \leq k \|b - x\| \leftrightarrow \|F (y) - F (x)\| \leq k \|y - x\|)$
48	42 47	imbi12d	$⊢ b = y \to ((x < b \to \|F (b) - F (x)\| \leq k \|b - x\|) \leftrightarrow (x < y \to \|F (y) - F (x)\| \leq k \|y - x\|))$
49	41 48	rspc2v	$⊢ (x \in [A, B] \land y \in [A, B]) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to (x < y \to \|F (y) - F (x)\| \leq k \|y - x\|))$
50	49	ad2antlr	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to (x < y \to \|F (y) - F (x)\| \leq k \|y - x\|))$
51		pm2.27	$⊢ x < y \to ((x < y \to \|F (y) - F (x)\| \leq k \|y - x\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
52	51	adantl	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ((x < y \to \|F (y) - F (x)\| \leq k \|y - x\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
53	50 52	syld	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
54		0le0	$⊢ 0 \leq 0$
55		fvres	$⊢ x \in [A, B] \to ({F ↾}_{[A, B]}) (x) = F (x)$
56	55	ad2antrl	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to ({F ↾}_{[A, B]}) (x) = F (x)$
57		cncff	$⊢ ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
58	5 57	syl	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
59	58	ad2antrr	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
60		simpl	$⊢ (x \in [A, B] \land y \in [A, B]) \to x \in [A, B]$
61		ffvelrn	$⊢ (({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ \land x \in [A, B]) \to ({F ↾}_{[A, B]}) (x) \in ℝ$
62	59 60 61	syl2an	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to ({F ↾}_{[A, B]}) (x) \in ℝ$
63	56 62	eqeltrrd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to F (x) \in ℝ$
64	63	recnd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to F (x) \in ℂ$
65	64	subidd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to F (x) - F (x) = 0$
66	65	abs00bd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to \|F (x) - F (x)\| = 0$
67		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
68	1 2 67	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
69	68	ad3antrrr	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to [A, B] \subseteq ℝ$
70		simprl	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to x \in [A, B]$
71	69 70	sseldd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to x \in ℝ$
72	71	recnd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to x \in ℂ$
73	72	subidd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to x - x = 0$
74	73	abs00bd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to \|x - x\| = 0$
75	74	oveq2d	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to k \|x - x\| = k \cdot 0$
76		simplr	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to k \in ℝ$
77	76	recnd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to k \in ℂ$
78	77	mul01d	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to k \cdot 0 = 0$
79	75 78	eqtrd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to k \|x - x\| = 0$
80	66 79	breq12d	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to (\|F (x) - F (x)\| \leq k \|x - x\| \leftrightarrow 0 \leq 0)$
81	54 80	mpbiri	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to \|F (x) - F (x)\| \leq k \|x - x\|$
82		fveq2	$⊢ x = y \to F (x) = F (y)$
83	82	fvoveq1d	$⊢ x = y \to \|F (x) - F (x)\| = \|F (y) - F (x)\|$
84		fvoveq1	$⊢ x = y \to \|x - x\| = \|y - x\|$
85	84	oveq2d	$⊢ x = y \to k \|x - x\| = k \|y - x\|$
86	83 85	breq12d	$⊢ x = y \to (\|F (x) - F (x)\| \leq k \|x - x\| \leftrightarrow \|F (y) - F (x)\| \leq k \|y - x\|)$
87	81 86	syl5ibcom	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to (x = y \to \|F (y) - F (x)\| \leq k \|y - x\|)$
88	87	imp	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land x = y) \to \|F (y) - F (x)\| \leq k \|y - x\|$
89	88	a1d	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land x = y) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
90		breq1	$⊢ a = y \to (a < b \leftrightarrow y < b)$
91		fveq2	$⊢ a = y \to F (a) = F (y)$
92	91	oveq2d	$⊢ a = y \to F (b) - F (a) = F (b) - F (y)$
93	92	fveq2d	$⊢ a = y \to \|F (b) - F (a)\| = \|F (b) - F (y)\|$
94		oveq2	$⊢ a = y \to b - a = b - y$
95	94	fveq2d	$⊢ a = y \to \|b - a\| = \|b - y\|$
96	95	oveq2d	$⊢ a = y \to k \|b - a\| = k \|b - y\|$
97	93 96	breq12d	$⊢ a = y \to (\|F (b) - F (a)\| \leq k \|b - a\| \leftrightarrow \|F (b) - F (y)\| \leq k \|b - y\|)$
98	90 97	imbi12d	$⊢ a = y \to ((a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \leftrightarrow (y < b \to \|F (b) - F (y)\| \leq k \|b - y\|))$
99		breq2	$⊢ b = x \to (y < b \leftrightarrow y < x)$
100		fveq2	$⊢ b = x \to F (b) = F (x)$
101	100	fvoveq1d	$⊢ b = x \to \|F (b) - F (y)\| = \|F (x) - F (y)\|$
102		fvoveq1	$⊢ b = x \to \|b - y\| = \|x - y\|$
103	102	oveq2d	$⊢ b = x \to k \|b - y\| = k \|x - y\|$
104	101 103	breq12d	$⊢ b = x \to (\|F (b) - F (y)\| \leq k \|b - y\| \leftrightarrow \|F (x) - F (y)\| \leq k \|x - y\|)$
105	99 104	imbi12d	$⊢ b = x \to ((y < b \to \|F (b) - F (y)\| \leq k \|b - y\|) \leftrightarrow (y < x \to \|F (x) - F (y)\| \leq k \|x - y\|))$
106	98 105	rspc2v	$⊢ (y \in [A, B] \land x \in [A, B]) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to (y < x \to \|F (x) - F (y)\| \leq k \|x - y\|))$
107	106	ancoms	$⊢ (x \in [A, B] \land y \in [A, B]) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to (y < x \to \|F (x) - F (y)\| \leq k \|x - y\|))$
108	107	ad2antlr	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to (y < x \to \|F (x) - F (y)\| \leq k \|x - y\|))$
109		simpr	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to y < x$
110		fvres	$⊢ y \in [A, B] \to ({F ↾}_{[A, B]}) (y) = F (y)$
111	110	ad2antll	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to ({F ↾}_{[A, B]}) (y) = F (y)$
112		simpr	$⊢ (x \in [A, B] \land y \in [A, B]) \to y \in [A, B]$
113		ffvelrn	$⊢ (({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ \land y \in [A, B]) \to ({F ↾}_{[A, B]}) (y) \in ℝ$
114	59 112 113	syl2an	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to ({F ↾}_{[A, B]}) (y) \in ℝ$
115	111 114	eqeltrrd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to F (y) \in ℝ$
116	115	recnd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to F (y) \in ℂ$
117	64 116	abssubd	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to \|F (x) - F (y)\| = \|F (y) - F (x)\|$
118	117	adantr	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to \|F (x) - F (y)\| = \|F (y) - F (x)\|$
119	68	ad2antrr	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to [A, B] \subseteq ℝ$
120	119	sseld	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to (x \in [A, B] \to x \in ℝ)$
121	119	sseld	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to (y \in [A, B] \to y \in ℝ)$
122	120 121	anim12d	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to ((x \in [A, B] \land y \in [A, B]) \to (x \in ℝ \land y \in ℝ))$
123	122	imp	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to (x \in ℝ \land y \in ℝ)$
124		recn	$⊢ x \in ℝ \to x \in ℂ$
125		recn	$⊢ y \in ℝ \to y \in ℂ$
126		abssub	$⊢ (x \in ℂ \land y \in ℂ) \to \|x - y\| = \|y - x\|$
127	124 125 126	syl2an	$⊢ (x \in ℝ \land y \in ℝ) \to \|x - y\| = \|y - x\|$
128	123 127	syl	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to \|x - y\| = \|y - x\|$
129	128	adantr	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to \|x - y\| = \|y - x\|$
130	129	oveq2d	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to k \|x - y\| = k \|y - x\|$
131	118 130	breq12d	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to (\|F (x) - F (y)\| \leq k \|x - y\| \leftrightarrow \|F (y) - F (x)\| \leq k \|y - x\|)$
132	131	biimpd	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to (\|F (x) - F (y)\| \leq k \|x - y\| \to \|F (y) - F (x)\| \leq k \|y - x\|)$
133	109 132	embantd	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to ((y < x \to \|F (x) - F (y)\| \leq k \|x - y\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
134	108 133	syld	$⊢ ((((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \land y < x) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
135		lttri4	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \lor x = y \lor y < x)$
136	123 135	syl	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to (x < y \lor x = y \lor y < x)$
137	53 89 134 136	mpjao3dan	$⊢ (((φ \land A \leq B) \land k \in ℝ) \land (x \in [A, B] \land y \in [A, B])) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \|F (y) - F (x)\| \leq k \|y - x\|)$
138	137	ralrimdvva	$⊢ ((φ \land A \leq B) \land k \in ℝ) \to (\forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|)$
139	138	reximdva	$⊢ (φ \land A \leq B) \to (\exists k \in ℝ \forall a \in [A, B] \forall b \in [A, B] (a < b \to \|F (b) - F (a)\| \leq k \|b - a\|) \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|)$
140	32 139	mpd	$⊢ (φ \land A \leq B) \to \exists k \in ℝ \forall x \in [A, B] \forall y \in [A, B] \|F (y) - F (x)\| \leq k \|y - x\|$
141	18 140 2 1	ltlecasei	$⊢ φ \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 c1lip1

Proof