ftc1lem6

	Ref	Expression
Hypotheses	ftc1.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1.a	$⊢ φ \to A \in ℝ$
	ftc1.b	$⊢ φ \to B \in ℝ$
	ftc1.le	$⊢ φ \to A \leq B$
	ftc1.s	$⊢ φ \to (A, B) \subseteq D$
	ftc1.d	$⊢ φ \to D \subseteq ℝ$
	ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
	ftc1.c	$⊢ φ \to C \in (A, B)$
	ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
	ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
	ftc1.k	$⊢ K = L ↾_{𝑡} D$
	ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
	ftc1.h	$⊢ H = (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
Assertion	ftc1lem6	$⊢ φ \to F (C) \in (H {lim}_{ℂ} C)$

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1.a	$⊢ φ \to A \in ℝ$
3		ftc1.b	$⊢ φ \to B \in ℝ$
4		ftc1.le	$⊢ φ \to A \leq B$
5		ftc1.s	$⊢ φ \to (A, B) \subseteq D$
6		ftc1.d	$⊢ φ \to D \subseteq ℝ$
7		ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
8		ftc1.c	$⊢ φ \to C \in (A, B)$
9		ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
10		ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
11		ftc1.k	$⊢ K = L ↾_{𝑡} D$
12		ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
13		ftc1.h	$⊢ H = (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
14	1 2 3 4 5 6 7 8 9 10 11 12	ftc1lem3	$⊢ φ \to F : D ⟶ ℂ$
15	5 8	sseldd	$⊢ φ \to C \in D$
16	14 15	ffvelcdmd	$⊢ φ \to F (C) \in ℂ$
17		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
18		ax-resscn	$⊢ ℝ \subseteq ℂ$
19	6 18	sstrdi	$⊢ φ \to D \subseteq ℂ$
20	19	adantr	$⊢ (φ \land w \in ℝ^{+}) \to D \subseteq ℂ$
21		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land D \subseteq ℂ) \to {(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D)$
22	17 20 21	sylancr	$⊢ (φ \land w \in ℝ^{+}) \to {(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D)$
23	17	a1i	$⊢ (φ \land w \in ℝ^{+}) \to abs \circ - \in ∞Met (ℂ)$
24		eqid	$⊢ {(abs \circ -) ↾}_{(D \times D)} = {(abs \circ -) ↾}_{(D \times D)}$
25	12	cnfldtopn	$⊢ L = MetOpen (abs \circ -)$
26		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{(D \times D)}) = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
27	24 25 26	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land D \subseteq ℂ) \to L ↾_{𝑡} D = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
28	17 19 27	sylancr	$⊢ φ \to L ↾_{𝑡} D = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
29	11 28	eqtrid	$⊢ φ \to K = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
30	29	oveq1d	$⊢ φ \to K CnP L = MetOpen ({(abs \circ -) ↾}_{(D \times D)}) CnP L$
31	30	fveq1d	$⊢ φ \to (K CnP L) (C) = (MetOpen ({(abs \circ -) ↾}_{(D \times D)}) CnP L) (C)$
32	9 31	eleqtrd	$⊢ φ \to F \in (MetOpen ({(abs \circ -) ↾}_{(D \times D)}) CnP L) (C)$
33	32	adantr	$⊢ (φ \land w \in ℝ^{+}) \to F \in (MetOpen ({(abs \circ -) ↾}_{(D \times D)}) CnP L) (C)$
34		simpr	$⊢ (φ \land w \in ℝ^{+}) \to w \in ℝ^{+}$
35	26 25	metcnpi2	$⊢ (({(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D) \land abs \circ - \in ∞Met (ℂ)) \land (F \in (MetOpen ({(abs \circ -) ↾}_{(D \times D)}) CnP L) (C) \land w \in ℝ^{+})) \to \exists v \in ℝ^{+} \forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w)$
36	22 23 33 34 35	syl22anc	$⊢ (φ \land w \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w)$
37		simpr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to y \in D$
38	15	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to C \in D$
39	37 38	ovresd	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to y ({(abs \circ -) ↾}_{(D \times D)}) C = y (abs \circ -) C$
40	19	adantr	$⊢ (φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to D \subseteq ℂ$
41	40	sselda	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to y \in ℂ$
42		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
43	2 3 42	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
44	43 18	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
45		ioossicc	$⊢ (A, B) \subseteq [A, B]$
46	45 8	sselid	$⊢ φ \to C \in [A, B]$
47	44 46	sseldd	$⊢ φ \to C \in ℂ$
48	47	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to C \in ℂ$
49		eqid	$⊢ abs \circ - = abs \circ -$
50	49	cnmetdval	$⊢ (y \in ℂ \land C \in ℂ) \to y (abs \circ -) C = \|y - C\|$
51	41 48 50	syl2anc	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to y (abs \circ -) C = \|y - C\|$
52	39 51	eqtrd	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to y ({(abs \circ -) ↾}_{(D \times D)}) C = \|y - C\|$
53	52	breq1d	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \leftrightarrow \|y - C\| < v)$
54	14	adantr	$⊢ (φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to F : D ⟶ ℂ$
55	54	ffvelcdmda	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to F (y) \in ℂ$
56	16	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to F (C) \in ℂ$
57	49	cnmetdval	$⊢ (F (y) \in ℂ \land F (C) \in ℂ) \to F (y) (abs \circ -) F (C) = \|F (y) - F (C)\|$
58	55 56 57	syl2anc	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to F (y) (abs \circ -) F (C) = \|F (y) - F (C)\|$
59	58	breq1d	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to (F (y) (abs \circ -) F (C) < w \leftrightarrow \|F (y) - F (C)\| < w)$
60	53 59	imbi12d	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land y \in D) \to ((y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w) \leftrightarrow (\|y - C\| < v \to \|F (y) - F (C)\| < w))$
61	60	ralbidva	$⊢ (φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w) \leftrightarrow \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w))$
62		simprll	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to s \in ([A, B] ∖ \{C\})$
63		eldifsni	$⊢ s \in ([A, B] ∖ \{C\}) \to s \neq C$
64	62 63	syl	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to s \neq C$
65	2	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to A \in ℝ$
66	3	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to B \in ℝ$
67	4	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to A \leq B$
68	5	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to (A, B) \subseteq D$
69	6	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to D \subseteq ℝ$
70	7	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to F \in 𝐿^{1}$
71	8	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to C \in (A, B)$
72	9	ad2antrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to F \in (K CnP L) (C)$
73		simplrl	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to w \in ℝ^{+}$
74		simplrr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to v \in ℝ^{+}$
75		simprlr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)$
76		fvoveq1	$⊢ y = u \to \|y - C\| = \|u - C\|$
77	76	breq1d	$⊢ y = u \to (\|y - C\| < v \leftrightarrow \|u - C\| < v)$
78	77	imbrov2fvoveq	$⊢ y = u \to ((\|y - C\| < v \to \|F (y) - F (C)\| < w) \leftrightarrow (\|u - C\| < v \to \|F (u) - F (C)\| < w))$
79	78	rspccva	$⊢ (\forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w) \land u \in D) \to (\|u - C\| < v \to \|F (u) - F (C)\| < w)$
80	75 79	sylan	$⊢ (((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \land u \in D) \to (\|u - C\| < v \to \|F (u) - F (C)\| < w)$
81	62	eldifad	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to s \in [A, B]$
82		simprr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to \|s - C\| < v$
83	1 65 66 67 68 69 70 71 72 10 11 12 13 73 74 80 81 82	ftc1lem5	$⊢ (((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \land s \neq C) \to \|H (s) - F (C)\| < w$
84	64 83	mpdan	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w)) \land \|s - C\| < v)) \to \|H (s) - F (C)\| < w$
85	84	expr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land (s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w))) \to (\|s - C\| < v \to \|H (s) - F (C)\| < w)$
86	85	adantld	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land (s \in ([A, B] ∖ \{C\}) \land \forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w))) \to ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w)$
87	86	expr	$⊢ ((φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land s \in ([A, B] ∖ \{C\})) \to (\forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w) \to ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w))$
88	87	ralrimdva	$⊢ (φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall y \in D (\|y - C\| < v \to \|F (y) - F (C)\| < w) \to \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w))$
89	61 88	sylbid	$⊢ (φ \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w) \to \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w))$
90	89	anassrs	$⊢ ((φ \land w \in ℝ^{+}) \land v \in ℝ^{+}) \to (\forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w) \to \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w))$
91	90	reximdva	$⊢ (φ \land w \in ℝ^{+}) \to (\exists v \in ℝ^{+} \forall y \in D (y ({(abs \circ -) ↾}_{(D \times D)}) C < v \to F (y) (abs \circ -) F (C) < w) \to \exists v \in ℝ^{+} \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w))$
92	36 91	mpd	$⊢ (φ \land w \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w)$
93	92	ralrimiva	$⊢ φ \to \forall w \in ℝ^{+} \exists v \in ℝ^{+} \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w)$
94	1 2 3 4 5 6 7 14	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
95	94 44 46	dvlem	$⊢ (φ \land z \in ([A, B] ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
96	95 13	fmptd	$⊢ φ \to H : [A, B] ∖ \{C\} ⟶ ℂ$
97	44	ssdifssd	$⊢ φ \to [A, B] ∖ \{C\} \subseteq ℂ$
98	96 97 47	ellimc3	$⊢ φ \to (F (C) \in (H {lim}_{ℂ} C) \leftrightarrow (F (C) \in ℂ \land \forall w \in ℝ^{+} \exists v \in ℝ^{+} \forall s \in ([A, B] ∖ \{C\}) ((s \neq C \land \|s - C\| < v) \to \|H (s) - F (C)\| < w)))$
99	16 93 98	mpbir2and	$⊢ φ \to F (C) \in (H {lim}_{ℂ} C)$

Metamath Proof Explorer

Theorem ftc1lem6

Proof