c1liplem1

	Ref	Expression
Hypotheses	c1liplem1.a	$⊢ φ \to A \in ℝ$
	c1liplem1.b	$⊢ φ \to B \in ℝ$
	c1liplem1.le	$⊢ φ \to A \leq B$
	c1liplem1.f	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
	c1liplem1.dv	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
	c1liplem1.cn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
	c1liplem1.k	$⊢ K = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <)$
Assertion	c1liplem1	$⊢ φ \to (K \in ℝ \land \forall x \in [A, B] \forall y \in [A, B] (x < y \to \|F (y) - F (x)\| \leq K \|y - x\|))$

Proof

Step	Hyp	Ref	Expression
1		c1liplem1.a	$⊢ φ \to A \in ℝ$
2		c1liplem1.b	$⊢ φ \to B \in ℝ$
3		c1liplem1.le	$⊢ φ \to A \leq B$
4		c1liplem1.f	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
5		c1liplem1.dv	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
6		c1liplem1.cn	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
7		c1liplem1.k	$⊢ K = sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <)$
8		imassrn	$⊢ abs [F_{ℝ}^{'} [[A, B]]] \subseteq ran abs$
9		absf	$⊢ abs : ℂ ⟶ ℝ$
10		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
11	9 10	ax-mp	$⊢ ran abs \subseteq ℝ$
12	8 11	sstri	$⊢ abs [F_{ℝ}^{'} [[A, B]]] \subseteq ℝ$
13	12	a1i	$⊢ φ \to abs [F_{ℝ}^{'} [[A, B]]] \subseteq ℝ$
14		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
15		ffun	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to Fun F_{ℝ}^{'}$
16	14 15	ax-mp	$⊢ Fun F_{ℝ}^{'}$
17	16	a1i	$⊢ φ \to Fun F_{ℝ}^{'}$
18		cncff	$⊢ ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
19		fdm	$⊢ ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] ⟶ ℝ \to dom ({F_{ℝ}^{'} ↾}_{[A, B]}) = [A, B]$
20	5 18 19	3syl	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{[A, B]}) = [A, B]$
21		ssdmres	$⊢ [A, B] \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{[A, B]}) = [A, B]$
22	20 21	sylibr	$⊢ φ \to [A, B] \subseteq dom F_{ℝ}^{'}$
23	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
24	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
25		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
26	23 24 3 25	syl3anc	$⊢ φ \to A \in [A, B]$
27		funfvima2	$⊢ (Fun F_{ℝ}^{'} \land [A, B] \subseteq dom F_{ℝ}^{'}) \to (A \in [A, B] \to F_{ℝ}^{'} (A) \in F_{ℝ}^{'} [[A, B]])$
28	27	imp	$⊢ ((Fun F_{ℝ}^{'} \land [A, B] \subseteq dom F_{ℝ}^{'}) \land A \in [A, B]) \to F_{ℝ}^{'} (A) \in F_{ℝ}^{'} [[A, B]]$
29	17 22 26 28	syl21anc	$⊢ φ \to F_{ℝ}^{'} (A) \in F_{ℝ}^{'} [[A, B]]$
30		ffun	$⊢ abs : ℂ ⟶ ℝ \to Fun abs$
31	9 30	ax-mp	$⊢ Fun abs$
32		imassrn	$⊢ F_{ℝ}^{'} [[A, B]] \subseteq ran F_{ℝ}^{'}$
33		frn	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to ran F_{ℝ}^{'} \subseteq ℂ$
34	14 33	ax-mp	$⊢ ran F_{ℝ}^{'} \subseteq ℂ$
35	32 34	sstri	$⊢ F_{ℝ}^{'} [[A, B]] \subseteq ℂ$
36	9	fdmi	$⊢ dom abs = ℂ$
37	35 36	sseqtrri	$⊢ F_{ℝ}^{'} [[A, B]] \subseteq dom abs$
38		funfvima2	$⊢ (Fun abs \land F_{ℝ}^{'} [[A, B]] \subseteq dom abs) \to (F_{ℝ}^{'} (A) \in F_{ℝ}^{'} [[A, B]] \to \|F_{ℝ}^{'} (A)\| \in abs [F_{ℝ}^{'} [[A, B]]])$
39	31 37 38	mp2an	$⊢ F_{ℝ}^{'} (A) \in F_{ℝ}^{'} [[A, B]] \to \|F_{ℝ}^{'} (A)\| \in abs [F_{ℝ}^{'} [[A, B]]]$
40		ne0i	$⊢ \|F_{ℝ}^{'} (A)\| \in abs [F_{ℝ}^{'} [[A, B]]] \to abs [F_{ℝ}^{'} [[A, B]]] \neq \emptyset$
41	29 39 40	3syl	$⊢ φ \to abs [F_{ℝ}^{'} [[A, B]]] \neq \emptyset$
42		ax-resscn	$⊢ ℝ \subseteq ℂ$
43		ssid	$⊢ ℂ \subseteq ℂ$
44		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
45	42 43 44	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
46	45 5	sseldi	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
47		cniccbdd	$⊢ (A \in ℝ \land B \in ℝ \land ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ) \to \exists a \in ℝ \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a$
48	1 2 46 47	syl3anc	$⊢ φ \to \exists a \in ℝ \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a$
49		fvelima	$⊢ (Fun abs \land b \in abs [F_{ℝ}^{'} [[A, B]]]) \to \exists y \in F_{ℝ}^{'} [[A, B]] \|y\| = b$
50	31 49	mpan	$⊢ b \in abs [F_{ℝ}^{'} [[A, B]]] \to \exists y \in F_{ℝ}^{'} [[A, B]] \|y\| = b$
51		fvres	$⊢ b \in [A, B] \to ({F_{ℝ}^{'} ↾}_{[A, B]}) (b) = F_{ℝ}^{'} (b)$
52	51	adantl	$⊢ (\forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \land b \in [A, B]) \to ({F_{ℝ}^{'} ↾}_{[A, B]}) (b) = F_{ℝ}^{'} (b)$
53	52	fveq2d	$⊢ (\forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \land b \in [A, B]) \to \|({F_{ℝ}^{'} ↾}_{[A, B]}) (b)\| = \|F_{ℝ}^{'} (b)\|$
54		2fveq3	$⊢ x = b \to \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| = \|({F_{ℝ}^{'} ↾}_{[A, B]}) (b)\|$
55	54	breq1d	$⊢ x = b \to (\|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \leftrightarrow \|({F_{ℝ}^{'} ↾}_{[A, B]}) (b)\| \leq a)$
56	55	rspccva	$⊢ (\forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \land b \in [A, B]) \to \|({F_{ℝ}^{'} ↾}_{[A, B]}) (b)\| \leq a$
57	53 56	eqbrtrrd	$⊢ (\forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \land b \in [A, B]) \to \|F_{ℝ}^{'} (b)\| \leq a$
58	57	adantll	$⊢ (((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \land b \in [A, B]) \to \|F_{ℝ}^{'} (b)\| \leq a$
59		fveq2	$⊢ F_{ℝ}^{'} (b) = y \to \|F_{ℝ}^{'} (b)\| = \|y\|$
60	59	breq1d	$⊢ F_{ℝ}^{'} (b) = y \to (\|F_{ℝ}^{'} (b)\| \leq a \leftrightarrow \|y\| \leq a)$
61	58 60	syl5ibcom	$⊢ (((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \land b \in [A, B]) \to (F_{ℝ}^{'} (b) = y \to \|y\| \leq a)$
62	61	rexlimdva	$⊢ ((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \to (\exists b \in [A, B] F_{ℝ}^{'} (b) = y \to \|y\| \leq a)$
63		fvelima	$⊢ (Fun F_{ℝ}^{'} \land y \in F_{ℝ}^{'} [[A, B]]) \to \exists b \in [A, B] F_{ℝ}^{'} (b) = y$
64	16 63	mpan	$⊢ y \in F_{ℝ}^{'} [[A, B]] \to \exists b \in [A, B] F_{ℝ}^{'} (b) = y$
65	62 64	impel	$⊢ (((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \land y \in F_{ℝ}^{'} [[A, B]]) \to \|y\| \leq a$
66		breq1	$⊢ \|y\| = b \to (\|y\| \leq a \leftrightarrow b \leq a)$
67	65 66	syl5ibcom	$⊢ (((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \land y \in F_{ℝ}^{'} [[A, B]]) \to (\|y\| = b \to b \leq a)$
68	67	rexlimdva	$⊢ ((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \to (\exists y \in F_{ℝ}^{'} [[A, B]] \|y\| = b \to b \leq a)$
69	50 68	syl5	$⊢ ((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \to (b \in abs [F_{ℝ}^{'} [[A, B]]] \to b \leq a)$
70	69	ralrimiv	$⊢ ((φ \land a \in ℝ) \land \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a) \to \forall b \in abs [F_{ℝ}^{'} [[A, B]]] b \leq a$
71	70	ex	$⊢ (φ \land a \in ℝ) \to (\forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \to \forall b \in abs [F_{ℝ}^{'} [[A, B]]] b \leq a)$
72	71	reximdva	$⊢ φ \to (\exists a \in ℝ \forall x \in [A, B] \|({F_{ℝ}^{'} ↾}_{[A, B]}) (x)\| \leq a \to \exists a \in ℝ \forall b \in abs [F_{ℝ}^{'} [[A, B]]] b \leq a)$
73	48 72	mpd	$⊢ φ \to \exists a \in ℝ \forall b \in abs [F_{ℝ}^{'} [[A, B]]] b \leq a$
74	13 41 73	suprcld	$⊢ φ \to sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <) \in ℝ$
75	7 74	eqeltrid	$⊢ φ \to K \in ℝ$
76		simplrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in [A, B]$
77	76	fvresd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (y) = F (y)$
78		cncff	$⊢ ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
79	6 78	syl	$⊢ φ \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
80	79	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) : [A, B] ⟶ ℝ$
81	80 76	ffvelrnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (y) \in ℝ$
82	81	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (y) \in ℂ$
83	77 82	eqeltrrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) \in ℂ$
84		simplrl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in [A, B]$
85	84	fvresd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (x) = F (x)$
86	80 84	ffvelrnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (x) \in ℝ$
87	86	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) (x) \in ℂ$
88	85 87	eqeltrrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) \in ℂ$
89	83 88	subcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) - F (x) \in ℂ$
90		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
91	1 2 90	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
92	91	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [A, B] \subseteq ℝ$
93	92 76	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in ℝ$
94	92 84	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in ℝ$
95	93 94	resubcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℝ$
96	95	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℂ$
97		simpr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x < y$
98		difrp	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow y - x \in ℝ^{+})$
99	94 93 98	syl2anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (x < y \leftrightarrow y - x \in ℝ^{+})$
100	97 99	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℝ^{+}$
101	100	rpne0d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \neq 0$
102	89 96 101	absdivd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|\frac{F (y) - F (x)}{y - x}\| = \frac{\|F (y) - F (x)\|}{\|y - x\|}$
103	12	a1i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to abs [F_{ℝ}^{'} [[A, B]]] \subseteq ℝ$
104	41	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to abs [F_{ℝ}^{'} [[A, B]]] \neq \emptyset$
105	73	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \exists a \in ℝ \forall b \in abs [F_{ℝ}^{'} [[A, B]]] b \leq a$
106	31	a1i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to Fun abs$
107	89 96 101	divcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{F (y) - F (x)}{y - x} \in ℂ$
108	107 36	eleqtrrdi	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{F (y) - F (x)}{y - x} \in dom abs$
109	94	rexrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in ℝ^{*}$
110	93	rexrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in ℝ^{*}$
111	94 93 97	ltled	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \leq y$
112		ubicc2	$⊢ (x \in ℝ^{} \land y \in ℝ^{} \land x \leq y) \to y \in [x, y]$
113	109 110 111 112	syl3anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in [x, y]$
114	113	fvresd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[x, y]}) (y) = F (y)$
115		lbicc2	$⊢ (x \in ℝ^{} \land y \in ℝ^{} \land x \leq y) \to x \in [x, y]$
116	109 110 111 115	syl3anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in [x, y]$
117	116	fvresd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[x, y]}) (x) = F (x)$
118	114 117	oveq12d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x) = F (y) - F (x)$
119	118	oveq1d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} = \frac{F (y) - F (x)}{y - x}$
120		iccss2	$⊢ (x \in [A, B] \land y \in [A, B]) \to [x, y] \subseteq [A, B]$
121	120	ad2antlr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [x, y] \subseteq [A, B]$
122	121	resabs1d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to {({F ↾}_{[A, B]}) ↾}_{[x, y]} = {F ↾}_{[x, y]}$
123	6	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
124		rescncf	$⊢ [x, y] \subseteq [A, B] \to (({F ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ \to ({({F ↾}_{[A, B]}) ↾}_{[x, y]}) : [x, y] \underset{cn}{⟶} ℝ)$
125	121 123 124	sylc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({({F ↾}_{[A, B]}) ↾}_{[x, y]}) : [x, y] \underset{cn}{⟶} ℝ$
126	122 125	eqeltrrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ({F ↾}_{[x, y]}) : [x, y] \underset{cn}{⟶} ℝ$
127	42	a1i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ℝ \subseteq ℂ$
128	4	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
129		cnex	$⊢ ℂ \in V$
130		reex	$⊢ ℝ \in V$
131	129 130	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
132	131	simplbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to F : dom F ⟶ ℂ$
133	128 132	syl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F : dom F ⟶ ℂ$
134	131	simprbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
135	128 134	syl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to dom F \subseteq ℝ$
136		iccssre	$⊢ (x \in ℝ \land y \in ℝ) \to [x, y] \subseteq ℝ$
137	94 93 136	syl2anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [x, y] \subseteq ℝ$
138		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
139	138	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
140	138 139	dvres	$⊢ ((ℝ \subseteq ℂ \land F : dom F ⟶ ℂ) \land (dom F \subseteq ℝ \land [x, y] \subseteq ℝ)) \to ℝ D ({F ↾}_{[x, y]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([x, y])}$
141	127 133 135 137 140	syl22anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ℝ D ({F ↾}_{[x, y]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([x, y])}$
142		iccntr	$⊢ (x \in ℝ \land y \in ℝ) \to int (topGen (ran (.))) ([x, y]) = (x, y)$
143	94 93 142	syl2anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to int (topGen (ran (.))) ([x, y]) = (x, y)$
144	143	reseq2d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([x, y])} = {F_{ℝ}^{'} ↾}_{(x, y)}$
145	141 144	eqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to ℝ D ({F ↾}_{[x, y]}) = {F_{ℝ}^{'} ↾}_{(x, y)}$
146	145	dmeqd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to dom {({F ↾}_{[x, y]})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{(x, y)})$
147		ioossicc	$⊢ (x, y) \subseteq [x, y]$
148	147 121	sstrid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (x, y) \subseteq [A, B]$
149	22	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [A, B] \subseteq dom F_{ℝ}^{'}$
150	148 149	sstrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (x, y) \subseteq dom F_{ℝ}^{'}$
151		ssdmres	$⊢ (x, y) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(x, y)}) = (x, y)$
152	150 151	sylib	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to dom ({F_{ℝ}^{'} ↾}_{(x, y)}) = (x, y)$
153	146 152	eqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to dom {({F ↾}_{[x, y]})}_{ℝ}^{'} = (x, y)$
154	94 93 97 126 153	mvth	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \exists a \in (x, y) {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x}$
155	145	fveq1d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = ({F_{ℝ}^{'} ↾}_{(x, y)}) (a)$
156	155	adantrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = ({F_{ℝ}^{'} ↾}_{(x, y)}) (a)$
157		fvres	$⊢ a \in (x, y) \to ({F_{ℝ}^{'} ↾}_{(x, y)}) (a) = F_{ℝ}^{'} (a)$
158	157	ad2antll	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to ({F_{ℝ}^{'} ↾}_{(x, y)}) (a) = F_{ℝ}^{'} (a)$
159	156 158	eqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = F_{ℝ}^{'} (a)$
160	16	a1i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to Fun F_{ℝ}^{'}$
161	22	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to [A, B] \subseteq dom F_{ℝ}^{'}$
162	148	sseld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (a \in (x, y) \to a \in [A, B])$
163	162	impr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to a \in [A, B]$
164		funfvima2	$⊢ (Fun F_{ℝ}^{'} \land [A, B] \subseteq dom F_{ℝ}^{'}) \to (a \in [A, B] \to F_{ℝ}^{'} (a) \in F_{ℝ}^{'} [[A, B]])$
165	164	imp	$⊢ ((Fun F_{ℝ}^{'} \land [A, B] \subseteq dom F_{ℝ}^{'}) \land a \in [A, B]) \to F_{ℝ}^{'} (a) \in F_{ℝ}^{'} [[A, B]]$
166	160 161 163 165	syl21anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to F_{ℝ}^{'} (a) \in F_{ℝ}^{'} [[A, B]]$
167	159 166	eqeltrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) \in F_{ℝ}^{'} [[A, B]]$
168		eleq1	$⊢ {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \to ({({F ↾}_{[x, y]})}_{ℝ}^{'} (a) \in F_{ℝ}^{'} [[A, B]] \leftrightarrow \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \in F_{ℝ}^{'} [[A, B]])$
169	167 168	syl5ibcom	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land (x < y \land a \in (x, y))) \to ({({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \to \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \in F_{ℝ}^{'} [[A, B]])$
170	169	expr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (a \in (x, y) \to ({({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \to \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \in F_{ℝ}^{'} [[A, B]]))$
171	170	rexlimdv	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (\exists a \in (x, y) {({F ↾}_{[x, y]})}_{ℝ}^{'} (a) = \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \to \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \in F_{ℝ}^{'} [[A, B]])$
172	154 171	mpd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{({F ↾}_{[x, y]}) (y) - ({F ↾}_{[x, y]}) (x)}{y - x} \in F_{ℝ}^{'} [[A, B]]$
173	119 172	eqeltrrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{F (y) - F (x)}{y - x} \in F_{ℝ}^{'} [[A, B]]$
174		funfvima	$⊢ (Fun abs \land \frac{F (y) - F (x)}{y - x} \in dom abs) \to (\frac{F (y) - F (x)}{y - x} \in F_{ℝ}^{'} [[A, B]] \to \|\frac{F (y) - F (x)}{y - x}\| \in abs [F_{ℝ}^{'} [[A, B]]])$
175	174	imp	$⊢ ((Fun abs \land \frac{F (y) - F (x)}{y - x} \in dom abs) \land \frac{F (y) - F (x)}{y - x} \in F_{ℝ}^{'} [[A, B]]) \to \|\frac{F (y) - F (x)}{y - x}\| \in abs [F_{ℝ}^{'} [[A, B]]]$
176	106 108 173 175	syl21anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|\frac{F (y) - F (x)}{y - x}\| \in abs [F_{ℝ}^{'} [[A, B]]]$
177	103 104 105 176	suprubd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|\frac{F (y) - F (x)}{y - x}\| \leq sup (abs [F_{ℝ}^{'} [[A, B]]] ℝ <)$
178	177 7	breqtrrdi	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|\frac{F (y) - F (x)}{y - x}\| \leq K$
179	102 178	eqbrtrrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{\|F (y) - F (x)\|}{\|y - x\|} \leq K$
180	89	abscld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|F (y) - F (x)\| \in ℝ$
181	75	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to K \in ℝ$
182	96 101	absrpcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|y - x\| \in ℝ^{+}$
183	180 181 182	ledivmuld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (\frac{\|F (y) - F (x)\|}{\|y - x\|} \leq K \leftrightarrow \|F (y) - F (x)\| \leq \|y - x\| K)$
184	179 183	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|F (y) - F (x)\| \leq \|y - x\| K$
185	182	rpcnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|y - x\| \in ℂ$
186	181	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to K \in ℂ$
187	185 186	mulcomd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|y - x\| K = K \|y - x\|$
188	184 187	breqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \|F (y) - F (x)\| \leq K \|y - x\|$
189	188	ex	$⊢ (φ \land (x \in [A, B] \land y \in [A, B])) \to (x < y \to \|F (y) - F (x)\| \leq K \|y - x\|)$
190	189	ralrimivva	$⊢ φ \to \forall x \in [A, B] \forall y \in [A, B] (x < y \to \|F (y) - F (x)\| \leq K \|y - x\|)$
191	75 190	jca	$⊢ φ \to (K \in ℝ \land \forall x \in [A, B] \forall y \in [A, B] (x < y \to \|F (y) - F (x)\| \leq K \|y - x\|))$

Metamath Proof Explorer

Theorem c1liplem1

Proof