ftc1cnnc

Description: Choice-free proof of ftc1cn . (Contributed by Brendan Leahy, 20-Nov-2017)

	Ref	Expression
Hypotheses	ftc1cnnc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1cnnc.a	$⊢ φ \to A \in ℝ$
	ftc1cnnc.b	$⊢ φ \to B \in ℝ$
	ftc1cnnc.le	$⊢ φ \to A \leq B$
	ftc1cnnc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	ftc1cnnc.i	$⊢ φ \to F \in 𝐿^{1}$
Assertion	ftc1cnnc	$⊢ φ \to ℝ D G = F$

Proof

Step	Hyp	Ref	Expression
1		ftc1cnnc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1cnnc.a	$⊢ φ \to A \in ℝ$
3		ftc1cnnc.b	$⊢ φ \to B \in ℝ$
4		ftc1cnnc.le	$⊢ φ \to A \leq B$
5		ftc1cnnc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
6		ftc1cnnc.i	$⊢ φ \to F \in 𝐿^{1}$
7		dvf	$⊢ G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
8	7	a1i	$⊢ φ \to G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
9	8	ffund	$⊢ φ \to Fun G_{ℝ}^{'}$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	10	a1i	$⊢ φ \to ℝ \subseteq ℂ$
12		ssidd	$⊢ φ \to (A, B) \subseteq (A, B)$
13		ioossre	$⊢ (A, B) \subseteq ℝ$
14	13	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
15		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
16	5 15	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
17	1 2 3 4 12 14 6 16	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
18		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
19	2 3 18	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
20		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
21		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
22	11 17 19 20 21	dvbssntr	$⊢ φ \to dom G_{ℝ}^{'} \subseteq int (topGen (ran (.))) ([A, B])$
23		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
24	2 3 23	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
25	22 24	sseqtrd	$⊢ φ \to dom G_{ℝ}^{'} \subseteq (A, B)$
26		retop	$⊢ topGen (ran (.)) \in Top$
27	20 26	eqeltrri	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ \in Top$
28	27	a1i	$⊢ (φ \land c \in (A, B)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ \in Top$
29	19	adantr	$⊢ (φ \land c \in (A, B)) \to [A, B] \subseteq ℝ$
30		iooretop	$⊢ (A, B) \in topGen (ran (.))$
31	30 20	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
32	31	a1i	$⊢ (φ \land c \in (A, B)) \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
33		ioossicc	$⊢ (A, B) \subseteq [A, B]$
34	33	a1i	$⊢ (φ \land c \in (A, B)) \to (A, B) \subseteq [A, B]$
35		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
36	20	unieqi	$⊢ ⋃ topGen (ran (.)) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
37	35 36	eqtri	$⊢ ℝ = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
38	37	ssntr	$⊢ ((TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ \in Top \land [A, B] \subseteq ℝ) \land ((A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \land (A, B) \subseteq [A, B])) \to (A, B) \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ([A, B])$
39	28 29 32 34 38	syl22anc	$⊢ (φ \land c \in (A, B)) \to (A, B) \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ([A, B])$
40		simpr	$⊢ (φ \land c \in (A, B)) \to c \in (A, B)$
41	39 40	sseldd	$⊢ (φ \land c \in (A, B)) \to c \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ([A, B])$
42	16	ffvelcdmda	$⊢ (φ \land c \in (A, B)) \to F (c) \in ℂ$
43		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
44	13 10	sstri	$⊢ (A, B) \subseteq ℂ$
45		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land (A, B) \subseteq ℂ) \to {(abs \circ -) ↾}_{((A, B) \times (A, B))} \in ∞Met ((A, B))$
46	43 44 45	mp2an	$⊢ {(abs \circ -) ↾}_{((A, B) \times (A, B))} \in ∞Met ((A, B))$
47	46	a1i	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to {(abs \circ -) ↾}_{((A, B) \times (A, B))} \in ∞Met ((A, B))$
48	43	a1i	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to abs \circ - \in ∞Met (ℂ)$
49		ssid	$⊢ ℂ \subseteq ℂ$
50		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
51	21	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
52	51	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
53	21 50 52	cncfcn	$⊢ ((A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
54	44 49 53	mp2an	$⊢ (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
55	5 54	eleqtrdi	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
56		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (A, B) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
57	51 44 56	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
58	57	toponunii	$⊢ (A, B) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
59	58	eleq2i	$⊢ c \in (A, B) \leftrightarrow c \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
60	59	biimpi	$⊢ c \in (A, B) \to c \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
61		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
62	61	cncnpi	$⊢ (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})) \land c \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (c)$
63	55 60 62	syl2an	$⊢ (φ \land c \in (A, B)) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (c)$
64		eqid	$⊢ {(abs \circ -) ↾}_{((A, B) \times (A, B))} = {(abs \circ -) ↾}_{((A, B) \times (A, B))}$
65	21	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
66		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) = MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))})$
67	64 65 66	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land (A, B) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))})$
68	43 44 67	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))})$
69	68	oveq1i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld}) = MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) CnP TopOpen (ℂ_{fld})$
70	69	fveq1i	$⊢ ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (c) = (MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) CnP TopOpen (ℂ_{fld})) (c)$
71	63 70	eleqtrdi	$⊢ (φ \land c \in (A, B)) \to F \in (MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) CnP TopOpen (ℂ_{fld})) (c)$
72	71	adantr	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to F \in (MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) CnP TopOpen (ℂ_{fld})) (c)$
73		simpr	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to w \in ℝ^{+}$
74	66 65	metcnpi2	$⊢ (({(abs \circ -) ↾}_{((A, B) \times (A, B))} \in ∞Met ((A, B)) \land abs \circ - \in ∞Met (ℂ)) \land (F \in (MetOpen ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) CnP TopOpen (ℂ_{fld})) (c) \land w \in ℝ^{+})) \to \exists v \in ℝ^{+} \forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w)$
75	47 48 72 73 74	syl22anc	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w)$
76		simpr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to u \in (A, B)$
77		simpllr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to c \in (A, B)$
78	76 77	ovresd	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c = u (abs \circ -) c$
79		elioore	$⊢ u \in (A, B) \to u \in ℝ$
80	79	recnd	$⊢ u \in (A, B) \to u \in ℂ$
81	44	sseli	$⊢ c \in (A, B) \to c \in ℂ$
82	81	ad3antlr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to c \in ℂ$
83		eqid	$⊢ abs \circ - = abs \circ -$
84	83	cnmetdval	$⊢ (u \in ℂ \land c \in ℂ) \to u (abs \circ -) c = \|u - c\|$
85	80 82 84	syl2an2	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to u (abs \circ -) c = \|u - c\|$
86	78 85	eqtrd	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c = \|u - c\|$
87	86	breq1d	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \leftrightarrow \|u - c\| < v)$
88	16	ad2antrr	$⊢ ((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to F : (A, B) ⟶ ℂ$
89	88	ffvelcdmda	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to F (u) \in ℂ$
90	42	ad2antrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to F (c) \in ℂ$
91	83	cnmetdval	$⊢ (F (u) \in ℂ \land F (c) \in ℂ) \to F (u) (abs \circ -) F (c) = \|F (u) - F (c)\|$
92	89 90 91	syl2anc	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to F (u) (abs \circ -) F (c) = \|F (u) - F (c)\|$
93	92	breq1d	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to (F (u) (abs \circ -) F (c) < w \leftrightarrow \|F (u) - F (c)\| < w)$
94	87 93	imbi12d	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land u \in (A, B)) \to ((u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w) \leftrightarrow (\|u - c\| < v \to \|F (u) - F (c)\| < w))$
95	94	ralbidva	$⊢ ((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w) \leftrightarrow \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w))$
96		simprll	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to z \in ([A, B] ∖ \{c\})$
97		eldifsni	$⊢ z \in ([A, B] ∖ \{c\}) \to z \neq c$
98	96 97	syl	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to z \neq c$
99	19	ssdifssd	$⊢ φ \to [A, B] ∖ \{c\} \subseteq ℝ$
100	99	sselda	$⊢ (φ \land z \in ([A, B] ∖ \{c\})) \to z \in ℝ$
101	100	ad2ant2r	$⊢ ((φ \land c \in (A, B)) \land (z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w))) \to z \in ℝ$
102	101	ad2ant2r	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to z \in ℝ$
103		elioore	$⊢ c \in (A, B) \to c \in ℝ$
104	103	ad3antlr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to c \in ℝ$
105	102 104	lttri2d	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to (z \neq c \leftrightarrow (z < c \lor c < z))$
106	105	biimpa	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z \neq c) \to (z < c \lor c < z)$
107		fveq2	$⊢ s = z \to G (s) = G (z)$
108	107	oveq1d	$⊢ s = z \to G (s) - G (c) = G (z) - G (c)$
109		oveq1	$⊢ s = z \to s - c = z - c$
110	108 109	oveq12d	$⊢ s = z \to \frac{G (s) - G (c)}{s - c} = \frac{G (z) - G (c)}{z - c}$
111		eqid	$⊢ (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) = (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c})$
112		ovex	$⊢ \frac{G (z) - G (c)}{z - c} \in V$
113	110 111 112	fvmpt	$⊢ z \in ([A, B] ∖ \{c\}) \to (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) = \frac{G (z) - G (c)}{z - c}$
114	113	ad2antrr	$⊢ ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v) \to (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) = \frac{G (z) - G (c)}{z - c}$
115	114	ad2antlr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) = \frac{G (z) - G (c)}{z - c}$
116	17	ad4antr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to G : [A, B] ⟶ ℂ$
117		eldifi	$⊢ z \in ([A, B] ∖ \{c\}) \to z \in [A, B]$
118	117	ad2antrr	$⊢ ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v) \to z \in [A, B]$
119	118	ad2antlr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to z \in [A, B]$
120	116 119	ffvelcdmd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to G (z) \in ℂ$
121	33	sseli	$⊢ c \in (A, B) \to c \in [A, B]$
122	17	ffvelcdmda	$⊢ (φ \land c \in [A, B]) \to G (c) \in ℂ$
123	121 122	sylan2	$⊢ (φ \land c \in (A, B)) \to G (c) \in ℂ$
124	123	ad3antrrr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to G (c) \in ℂ$
125	102	adantr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to z \in ℝ$
126	125	recnd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to z \in ℂ$
127	81	ad4antlr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to c \in ℂ$
128		ltne	$⊢ (z \in ℝ \land z < c) \to c \neq z$
129	128	necomd	$⊢ (z \in ℝ \land z < c) \to z \neq c$
130	102 129	sylan	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to z \neq c$
131	120 124 126 127 130	div2subd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to \frac{G (z) - G (c)}{z - c} = \frac{G (c) - G (z)}{c - z}$
132	115 131	eqtrd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) = \frac{G (c) - G (z)}{c - z}$
133	132	fvoveq1d	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| = \|(\frac{G (c) - G (z)}{c - z}) - F (c)\|$
134	2	ad3antrrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to A \in ℝ$
135	3	ad3antrrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to B \in ℝ$
136	4	ad3antrrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to A \leq B$
137	5	ad3antrrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to F : (A, B) \underset{cn}{⟶} ℂ$
138	6	ad3antrrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to F \in 𝐿^{1}$
139		simpllr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to c \in (A, B)$
140		simplrl	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to w \in ℝ^{+}$
141		simplrr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to v \in ℝ^{+}$
142		simprlr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)$
143		fvoveq1	$⊢ u = y \to \|u - c\| = \|y - c\|$
144	143	breq1d	$⊢ u = y \to (\|u - c\| < v \leftrightarrow \|y - c\| < v)$
145	144	imbrov2fvoveq	$⊢ u = y \to ((\|u - c\| < v \to \|F (u) - F (c)\| < w) \leftrightarrow (\|y - c\| < v \to \|F (y) - F (c)\| < w))$
146	145	rspccva	$⊢ (\forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w) \land y \in (A, B)) \to (\|y - c\| < v \to \|F (y) - F (c)\| < w)$
147	142 146	sylan	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land y \in (A, B)) \to (\|y - c\| < v \to \|F (y) - F (c)\| < w)$
148	96 117	syl	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to z \in [A, B]$
149		simprr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to \|z - c\| < v$
150	121	ad3antlr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to c \in [A, B]$
151	103	recnd	$⊢ c \in (A, B) \to c \in ℂ$
152	151	subidd	$⊢ c \in (A, B) \to c - c = 0$
153	152	abs00bd	$⊢ c \in (A, B) \to \|c - c\| = 0$
154	153	ad3antlr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to \|c - c\| = 0$
155	141	rpgt0d	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to 0 < v$
156	154 155	eqbrtrd	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to \|c - c\| < v$
157	1 134 135 136 137 138 139 111 140 141 147 148 149 150 156	ftc1cnnclem	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to \|(\frac{G (c) - G (z)}{c - z}) - F (c)\| < w$
158	133 157	eqbrtrd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z < c) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w$
159	113	fvoveq1d	$⊢ z \in ([A, B] ∖ \{c\}) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| = \|(\frac{G (z) - G (c)}{z - c}) - F (c)\|$
160	159	ad2antrr	$⊢ ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| = \|(\frac{G (z) - G (c)}{z - c}) - F (c)\|$
161	160	ad2antlr	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land c < z) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| = \|(\frac{G (z) - G (c)}{z - c}) - F (c)\|$
162	1 134 135 136 137 138 139 111 140 141 147 150 156 148 149	ftc1cnnclem	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land c < z) \to \|(\frac{G (z) - G (c)}{z - c}) - F (c)\| < w$
163	161 162	eqbrtrd	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land c < z) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w$
164	158 163	jaodan	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land (z < c \lor c < z)) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w$
165	106 164	syldan	$⊢ ((((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \land z \neq c) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w$
166	98 165	mpdan	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land ((z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w)) \land \|z - c\| < v)) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w$
167	166	expr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land (z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w))) \to (\|z - c\| < v \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w)$
168	167	adantld	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land (z \in ([A, B] ∖ \{c\}) \land \forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w))) \to ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w)$
169	168	expr	$⊢ (((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \land z \in ([A, B] ∖ \{c\})) \to (\forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w) \to ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w))$
170	169	ralrimdva	$⊢ ((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall u \in (A, B) (\|u - c\| < v \to \|F (u) - F (c)\| < w) \to \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w))$
171	95 170	sylbid	$⊢ ((φ \land c \in (A, B)) \land (w \in ℝ^{+} \land v \in ℝ^{+})) \to (\forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w) \to \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w))$
172	171	anassrs	$⊢ (((φ \land c \in (A, B)) \land w \in ℝ^{+}) \land v \in ℝ^{+}) \to (\forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w) \to \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w))$
173	172	reximdva	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to (\exists v \in ℝ^{+} \forall u \in (A, B) (u ({(abs \circ -) ↾}_{((A, B) \times (A, B))}) c < v \to F (u) (abs \circ -) F (c) < w) \to \exists v \in ℝ^{+} \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w))$
174	75 173	mpd	$⊢ ((φ \land c \in (A, B)) \land w \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w)$
175	174	ralrimiva	$⊢ (φ \land c \in (A, B)) \to \forall w \in ℝ^{+} \exists v \in ℝ^{+} \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w)$
176	17	adantr	$⊢ (φ \land c \in (A, B)) \to G : [A, B] ⟶ ℂ$
177	19 10	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
178	177	adantr	$⊢ (φ \land c \in (A, B)) \to [A, B] \subseteq ℂ$
179	121	adantl	$⊢ (φ \land c \in (A, B)) \to c \in [A, B]$
180	176 178 179	dvlem	$⊢ ((φ \land c \in (A, B)) \land s \in ([A, B] ∖ \{c\})) \to \frac{G (s) - G (c)}{s - c} \in ℂ$
181	180	fmpttd	$⊢ (φ \land c \in (A, B)) \to (s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) : [A, B] ∖ \{c\} ⟶ ℂ$
182	177	ssdifssd	$⊢ φ \to [A, B] ∖ \{c\} \subseteq ℂ$
183	182	adantr	$⊢ (φ \land c \in (A, B)) \to [A, B] ∖ \{c\} \subseteq ℂ$
184	81	adantl	$⊢ (φ \land c \in (A, B)) \to c \in ℂ$
185	181 183 184	ellimc3	$⊢ (φ \land c \in (A, B)) \to (F (c) \in ((s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) {lim}_{ℂ} c) \leftrightarrow (F (c) \in ℂ \land \forall w \in ℝ^{+} \exists v \in ℝ^{+} \forall z \in ([A, B] ∖ \{c\}) ((z \neq c \land \|z - c\| < v) \to \|(s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) (z) - F (c)\| < w)))$
186	42 175 185	mpbir2and	$⊢ (φ \land c \in (A, B)) \to F (c) \in ((s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) {lim}_{ℂ} c)$
187		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
188	187 21 111 11 17 19	eldv	$⊢ φ \to (c G_{ℝ}^{'} F (c) \leftrightarrow (c \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ([A, B]) \land F (c) \in ((s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) {lim}_{ℂ} c)))$
189	188	adantr	$⊢ (φ \land c \in (A, B)) \to (c G_{ℝ}^{'} F (c) \leftrightarrow (c \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ([A, B]) \land F (c) \in ((s \in ([A, B] ∖ \{c\}) ⟼ \frac{G (s) - G (c)}{s - c}) {lim}_{ℂ} c)))$
190	41 186 189	mpbir2and	$⊢ (φ \land c \in (A, B)) \to c G_{ℝ}^{'} F (c)$
191		vex	$⊢ c \in V$
192		fvex	$⊢ F (c) \in V$
193	191 192	breldm	$⊢ c G_{ℝ}^{'} F (c) \to c \in dom G_{ℝ}^{'}$
194	190 193	syl	$⊢ (φ \land c \in (A, B)) \to c \in dom G_{ℝ}^{'}$
195	25 194	eqelssd	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
196		df-fn	$⊢ G_{ℝ}^{'} Fn (A, B) \leftrightarrow (Fun G_{ℝ}^{'} \land dom G_{ℝ}^{'} = (A, B))$
197	9 195 196	sylanbrc	$⊢ φ \to G_{ℝ}^{'} Fn (A, B)$
198	16	ffnd	$⊢ φ \to F Fn (A, B)$
199	9	adantr	$⊢ (φ \land c \in (A, B)) \to Fun G_{ℝ}^{'}$
200		funbrfv	$⊢ Fun G_{ℝ}^{'} \to (c G_{ℝ}^{'} F (c) \to G_{ℝ}^{'} (c) = F (c))$
201	199 190 200	sylc	$⊢ (φ \land c \in (A, B)) \to G_{ℝ}^{'} (c) = F (c)$
202	197 198 201	eqfnfvd	$⊢ φ \to ℝ D G = F$

Metamath Proof Explorer

Theorem ftc1cnnc

Proof