ftc1a

Description: The Fundamental Theorem of Calculus, part one. The function G formed by varying the right endpoint of an integral of F is continuous if F is integrable. (Contributed by Mario Carneiro, 1-Sep-2014)

	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}$
	ftc1a.f	$⊢ φ \to F : D ⟶ ℂ$
Assertion	ftc1a	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

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		ftc1a.f	$⊢ φ \to F : D ⟶ ℂ$
9	1 2 3 4 5 6 7 8	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$
10		fvexd	$⊢ ((φ \land e \in ℝ^{+}) \land w \in D) \to F (w) \in V$
11	8	feqmptd	$⊢ φ \to F = (w \in D ⟼ F (w))$
12	11 7	eqeltrrd	$⊢ φ \to (w \in D ⟼ F (w)) \in 𝐿^{1}$
13	12	adantr	$⊢ (φ \land e \in ℝ^{+}) \to (w \in D ⟼ F (w)) \in 𝐿^{1}$
14		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
15	10 13 14	itgcn	$⊢ (φ \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)$
16		oveq12	$⊢ (s = z \land r = y) \to s - r = z - y$
17	16	fveq2d	$⊢ (s = z \land r = y) \to \|s - r\| = \|z - y\|$
18	17	breq1d	$⊢ (s = z \land r = y) \to (\|s - r\| < d \leftrightarrow \|z - y\| < d)$
19		fveq2	$⊢ s = z \to G (s) = G (z)$
20		fveq2	$⊢ r = y \to G (r) = G (y)$
21	19 20	oveqan12d	$⊢ (s = z \land r = y) \to G (s) - G (r) = G (z) - G (y)$
22	21	fveq2d	$⊢ (s = z \land r = y) \to \|G (s) - G (r)\| = \|G (z) - G (y)\|$
23	22	breq1d	$⊢ (s = z \land r = y) \to (\|G (s) - G (r)\| < e \leftrightarrow \|G (z) - G (y)\| < e)$
24	18 23	imbi12d	$⊢ (s = z \land r = y) \to ((\|s - r\| < d \to \|G (s) - G (r)\| < e) \leftrightarrow (\|z - y\| < d \to \|G (z) - G (y)\| < e))$
25	24	ancoms	$⊢ (r = y \land s = z) \to ((\|s - r\| < d \to \|G (s) - G (r)\| < e) \leftrightarrow (\|z - y\| < d \to \|G (z) - G (y)\| < e))$
26		oveq12	$⊢ (s = y \land r = z) \to s - r = y - z$
27	26	fveq2d	$⊢ (s = y \land r = z) \to \|s - r\| = \|y - z\|$
28	27	breq1d	$⊢ (s = y \land r = z) \to (\|s - r\| < d \leftrightarrow \|y - z\| < d)$
29		fveq2	$⊢ s = y \to G (s) = G (y)$
30		fveq2	$⊢ r = z \to G (r) = G (z)$
31	29 30	oveqan12d	$⊢ (s = y \land r = z) \to G (s) - G (r) = G (y) - G (z)$
32	31	fveq2d	$⊢ (s = y \land r = z) \to \|G (s) - G (r)\| = \|G (y) - G (z)\|$
33	32	breq1d	$⊢ (s = y \land r = z) \to (\|G (s) - G (r)\| < e \leftrightarrow \|G (y) - G (z)\| < e)$
34	28 33	imbi12d	$⊢ (s = y \land r = z) \to ((\|s - r\| < d \to \|G (s) - G (r)\| < e) \leftrightarrow (\|y - z\| < d \to \|G (y) - G (z)\| < e))$
35	34	ancoms	$⊢ (r = z \land s = y) \to ((\|s - r\| < d \to \|G (s) - G (r)\| < e) \leftrightarrow (\|y - z\| < d \to \|G (y) - G (z)\| < e))$
36		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
37	2 3 36	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
38	37	ad2antrr	$⊢ ((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \to [A, B] \subseteq ℝ$
39	37	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to [A, B] \subseteq ℝ$
40		simprr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to z \in [A, B]$
41	39 40	sseldd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to z \in ℝ$
42	41	recnd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to z \in ℂ$
43		simprl	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to y \in [A, B]$
44	39 43	sseldd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to y \in ℝ$
45	44	recnd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to y \in ℂ$
46	42 45	abssubd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to \|z - y\| = \|y - z\|$
47	46	breq1d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to (\|z - y\| < d \leftrightarrow \|y - z\| < d)$
48	9	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to G : [A, B] ⟶ ℂ$
49	48 40	ffvelrnd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to G (z) \in ℂ$
50	48 43	ffvelrnd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to G (y) \in ℂ$
51	49 50	abssubd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to \|G (z) - G (y)\| = \|G (y) - G (z)\|$
52	51	breq1d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to (\|G (z) - G (y)\| < e \leftrightarrow \|G (y) - G (z)\| < e)$
53	47 52	imbi12d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to ((\|z - y\| < d \to \|G (z) - G (y)\| < e) \leftrightarrow (\|y - z\| < d \to \|G (y) - G (z)\| < e))$
54		simpr3	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to y \leq z$
55	2	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to A \in ℝ$
56	3	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to B \in ℝ$
57	4	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to A \leq B$
58	5	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to (A, B) \subseteq D$
59	6	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to D \subseteq ℝ$
60	7	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to F \in 𝐿^{1}$
61	8	adantr	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to F : D ⟶ ℂ$
62		simpr1	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to y \in [A, B]$
63		simpr2	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to z \in [A, B]$
64	1 55 56 57 58 59 60 61 62 63	ftc1lem1	$⊢ ((φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \land y \leq z) \to G (z) - G (y) = \int_{(y, z)} F (t) d t$
65	54 64	mpdan	$⊢ (φ \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to G (z) - G (y) = \int_{(y, z)} F (t) d t$
66	65	adantlr	$⊢ ((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to G (z) - G (y) = \int_{(y, z)} F (t) d t$
67	66	ad2ant2r	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to G (z) - G (y) = \int_{(y, z)} F (t) d t$
68	67	fveq2d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|G (z) - G (y)\| = \|\int_{(y, z)} F (t) d t\|$
69		fvexd	$⊢ ((((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \land t \in (y, z)) \to F (t) \in V$
70	2	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to A \in ℝ$
71	70	rexrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to A \in ℝ^{*}$
72		simprl1	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to y \in [A, B]$
73	3	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to B \in ℝ$
74		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
75	70 73 74	syl2anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
76	72 75	mpbid	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y \in ℝ \land A \leq y \land y \leq B)$
77	76	simp2d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to A \leq y$
78		iooss1	$⊢ (A \in ℝ^{*} \land A \leq y) \to (y, z) \subseteq (A, z)$
79	71 77 78	syl2anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y, z) \subseteq (A, z)$
80	73	rexrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to B \in ℝ^{*}$
81		simprl2	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z \in [A, B]$
82		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
83	70 73 82	syl2anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
84	81 83	mpbid	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (z \in ℝ \land A \leq z \land z \leq B)$
85	84	simp3d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z \leq B$
86		iooss2	$⊢ (B \in ℝ^{*} \land z \leq B) \to (A, z) \subseteq (A, B)$
87	80 85 86	syl2anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (A, z) \subseteq (A, B)$
88	79 87	sstrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y, z) \subseteq (A, B)$
89	5	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (A, B) \subseteq D$
90	88 89	sstrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y, z) \subseteq D$
91		ioombl	$⊢ (y, z) \in dom vol$
92	91	a1i	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (y, z) \in dom vol$
93		fvexd	$⊢ ((((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \land t \in D) \to F (t) \in V$
94	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
95	94 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
96	95	ad3antrrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
97	90 92 93 96	iblss	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (t \in (y, z) ⟼ F (t)) \in 𝐿^{1}$
98	69 97	itgcl	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \int_{(y, z)} F (t) d t \in ℂ$
99	98	abscld	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|\int_{(y, z)} F (t) d t\| \in ℝ$
100		iblmbf	$⊢ (t \in (y, z) ⟼ F (t)) \in 𝐿^{1} \to (t \in (y, z) ⟼ F (t)) \in MblFn$
101	97 100	syl	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (t \in (y, z) ⟼ F (t)) \in MblFn$
102	101 69	mbfmptcl	$⊢ ((((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \land t \in (y, z)) \to F (t) \in ℂ$
103	102	abscld	$⊢ ((((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \land t \in (y, z)) \to \|F (t)\| \in ℝ$
104	69 97	iblabs	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (t \in (y, z) ⟼ \|F (t)\|) \in 𝐿^{1}$
105	103 104	itgrecl	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \int_{(y, z)} \|F (t)\| d t \in ℝ$
106		simprl	$⊢ (φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to e \in ℝ^{+}$
107	106	ad2antrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to e \in ℝ^{+}$
108	107	rpred	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to e \in ℝ$
109	69 97	itgabs	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|\int_{(y, z)} F (t) d t\| \leq \int_{(y, z)} \|F (t)\| d t$
110		mblvol	$⊢ (y, z) \in dom vol \to vol ((y, z)) = {vol}^{*} ((y, z))$
111	91 110	ax-mp	$⊢ vol ((y, z)) = {vol}^{*} ((y, z))$
112		ioossre	$⊢ (y, z) \subseteq ℝ$
113		ovolcl	$⊢ (y, z) \subseteq ℝ \to {vol}^{} ((y, z)) \in ℝ^{}$
114	112 113	mp1i	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to {vol}^{} ((y, z)) \in ℝ^{}$
115	84	simp1d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z \in ℝ$
116	76	simp1d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to y \in ℝ$
117	115 116	resubcld	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z - y \in ℝ$
118	117	rexrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z - y \in ℝ^{*}$
119		simprr	$⊢ (φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to d \in ℝ^{+}$
120	119	ad2antrr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to d \in ℝ^{+}$
121	120	rpxrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to d \in ℝ^{*}$
122		ioossicc	$⊢ (y, z) \subseteq [y, z]$
123		iccssre	$⊢ (y \in ℝ \land z \in ℝ) \to [y, z] \subseteq ℝ$
124	116 115 123	syl2anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to [y, z] \subseteq ℝ$
125		ovolss	$⊢ ((y, z) \subseteq [y, z] \land [y, z] \subseteq ℝ) \to {vol}^{} ((y, z)) \leq {vol}^{} ([y, z])$
126	122 124 125	sylancr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to {vol}^{} ((y, z)) \leq {vol}^{} ([y, z])$
127		simprl3	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to y \leq z$
128		ovolicc	$⊢ (y \in ℝ \land z \in ℝ \land y \leq z) \to {vol}^{*} ([y, z]) = z - y$
129	116 115 127 128	syl3anc	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to {vol}^{*} ([y, z]) = z - y$
130	126 129	breqtrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to {vol}^{*} ((y, z)) \leq z - y$
131	116 115 127	abssubge0d	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|z - y\| = z - y$
132		simprr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|z - y\| < d$
133	131 132	eqbrtrrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to z - y < d$
134	114 118 121 130 133	xrlelttrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to {vol}^{*} ((y, z)) < d$
135	111 134	eqbrtrid	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to vol ((y, z)) < d$
136		sseq1	$⊢ u = (y, z) \to (u \subseteq D \leftrightarrow (y, z) \subseteq D)$
137		fveq2	$⊢ u = (y, z) \to vol (u) = vol ((y, z))$
138	137	breq1d	$⊢ u = (y, z) \to (vol (u) < d \leftrightarrow vol ((y, z)) < d)$
139	136 138	anbi12d	$⊢ u = (y, z) \to ((u \subseteq D \land vol (u) < d) \leftrightarrow ((y, z) \subseteq D \land vol ((y, z)) < d))$
140		2fveq3	$⊢ w = t \to \|F (w)\| = \|F (t)\|$
141	140	cbvitgv	$⊢ \int_{u} \|F (w)\| d w = \int_{u} \|F (t)\| d t$
142		itgeq1	$⊢ u = (y, z) \to \int_{u} \|F (t)\| d t = \int_{(y, z)} \|F (t)\| d t$
143	141 142	syl5eq	$⊢ u = (y, z) \to \int_{u} \|F (w)\| d w = \int_{(y, z)} \|F (t)\| d t$
144	143	breq1d	$⊢ u = (y, z) \to (\int_{u} \|F (w)\| d w < e \leftrightarrow \int_{(y, z)} \|F (t)\| d t < e)$
145	139 144	imbi12d	$⊢ u = (y, z) \to (((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e) \leftrightarrow (((y, z) \subseteq D \land vol ((y, z)) < d) \to \int_{(y, z)} \|F (t)\| d t < e))$
146		simplr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)$
147	145 146 92	rspcdva	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to (((y, z) \subseteq D \land vol ((y, z)) < d) \to \int_{(y, z)} \|F (t)\| d t < e)$
148	90 135 147	mp2and	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \int_{(y, z)} \|F (t)\| d t < e$
149	99 105 108 109 148	lelttrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|\int_{(y, z)} F (t) d t\| < e$
150	68 149	eqbrtrd	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land ((y \in [A, B] \land z \in [A, B] \land y \leq z) \land \|z - y\| < d)) \to \|G (z) - G (y)\| < e$
151	150	expr	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B] \land y \leq z)) \to (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
152	25 35 38 53 151	wlogle	$⊢ (((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \land (y \in [A, B] \land z \in [A, B])) \to (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
153	152	ralrimivva	$⊢ ((φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \land \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e)) \to \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
154	153	ex	$⊢ (φ \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to (\forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e) \to \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e))$
155	154	anassrs	$⊢ ((φ \land e \in ℝ^{+}) \land d \in ℝ^{+}) \to (\forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e) \to \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e))$
156	155	reximdva	$⊢ (φ \land e \in ℝ^{+}) \to (\exists d \in ℝ^{+} \forall u \in dom vol ((u \subseteq D \land vol (u) < d) \to \int_{u} \|F (w)\| d w < e) \to \exists d \in ℝ^{+} \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e))$
157	15 156	mpd	$⊢ (φ \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
158		r19.12	$⊢ \exists d \in ℝ^{+} \forall y \in [A, B] \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e) \to \forall y \in [A, B] \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
159	157 158	syl	$⊢ (φ \land e \in ℝ^{+}) \to \forall y \in [A, B] \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
160	159	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \forall y \in [A, B] \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
161		ralcom	$⊢ \forall e \in ℝ^{+} \forall y \in [A, B] \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e) \leftrightarrow \forall y \in [A, B] \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
162	160 161	sylib	$⊢ φ \to \forall y \in [A, B] \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)$
163		ax-resscn	$⊢ ℝ \subseteq ℂ$
164	37 163	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
165		ssid	$⊢ ℂ \subseteq ℂ$
166		elcncf2	$⊢ ([A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall y \in [A, B] \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)))$
167	164 165 166	sylancl	$⊢ φ \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall y \in [A, B] \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in [A, B] (\|z - y\| < d \to \|G (z) - G (y)\| < e)))$
168	9 162 167	mpbir2and	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem ftc1a

Proof