ftc1lem1

	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 ⟶ ℂ$
	ftc1lem1.x	$⊢ φ \to X \in [A, B]$
	ftc1lem1.y	$⊢ φ \to Y \in [A, B]$
Assertion	ftc1lem1	$⊢ (φ \land X \leq Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$

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		ftc1lem1.x	$⊢ φ \to X \in [A, B]$
10		ftc1lem1.y	$⊢ φ \to Y \in [A, B]$
11		oveq2	$⊢ x = Y \to (A, x) = (A, Y)$
12		itgeq1	$⊢ (A, x) = (A, Y) \to \int_{(A, x)} F (t) d t = \int_{(A, Y)} F (t) d t$
13	11 12	syl	$⊢ x = Y \to \int_{(A, x)} F (t) d t = \int_{(A, Y)} F (t) d t$
14		itgex	$⊢ \int_{(A, Y)} F (t) d t \in V$
15	13 1 14	fvmpt	$⊢ Y \in [A, B] \to G (Y) = \int_{(A, Y)} F (t) d t$
16	10 15	syl	$⊢ φ \to G (Y) = \int_{(A, Y)} F (t) d t$
17	16	adantr	$⊢ (φ \land X \leq Y) \to G (Y) = \int_{(A, Y)} F (t) d t$
18	2	adantr	$⊢ (φ \land X \leq Y) \to A \in ℝ$
19		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
20	2 3 19	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
21	20 10	sseldd	$⊢ φ \to Y \in ℝ$
22	21	adantr	$⊢ (φ \land X \leq Y) \to Y \in ℝ$
23	20 9	sseldd	$⊢ φ \to X \in ℝ$
24	23	adantr	$⊢ (φ \land X \leq Y) \to X \in ℝ$
25		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
26	2 3 25	syl2anc	$⊢ φ \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
27	9 26	mpbid	$⊢ φ \to (X \in ℝ \land A \leq X \land X \leq B)$
28	27	simp2d	$⊢ φ \to A \leq X$
29	28	adantr	$⊢ (φ \land X \leq Y) \to A \leq X$
30		simpr	$⊢ (φ \land X \leq Y) \to X \leq Y$
31		elicc2	$⊢ (A \in ℝ \land Y \in ℝ) \to (X \in [A, Y] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq Y))$
32	2 21 31	syl2anc	$⊢ φ \to (X \in [A, Y] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq Y))$
33	32	adantr	$⊢ (φ \land X \leq Y) \to (X \in [A, Y] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq Y))$
34	24 29 30 33	mpbir3and	$⊢ (φ \land X \leq Y) \to X \in [A, Y]$
35	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
36		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
37	2 3 36	syl2anc	$⊢ φ \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
38	10 37	mpbid	$⊢ φ \to (Y \in ℝ \land A \leq Y \land Y \leq B)$
39	38	simp3d	$⊢ φ \to Y \leq B$
40		iooss2	$⊢ (B \in ℝ^{*} \land Y \leq B) \to (A, Y) \subseteq (A, B)$
41	35 39 40	syl2anc	$⊢ φ \to (A, Y) \subseteq (A, B)$
42	41 5	sstrd	$⊢ φ \to (A, Y) \subseteq D$
43	42	adantr	$⊢ (φ \land X \leq Y) \to (A, Y) \subseteq D$
44	43	sselda	$⊢ ((φ \land X \leq Y) \land t \in (A, Y)) \to t \in D$
45	8	ffvelrnda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
46	45	adantlr	$⊢ ((φ \land X \leq Y) \land t \in D) \to F (t) \in ℂ$
47	44 46	syldan	$⊢ ((φ \land X \leq Y) \land t \in (A, Y)) \to F (t) \in ℂ$
48	27	simp3d	$⊢ φ \to X \leq B$
49		iooss2	$⊢ (B \in ℝ^{*} \land X \leq B) \to (A, X) \subseteq (A, B)$
50	35 48 49	syl2anc	$⊢ φ \to (A, X) \subseteq (A, B)$
51	50 5	sstrd	$⊢ φ \to (A, X) \subseteq D$
52		ioombl	$⊢ (A, X) \in dom vol$
53	52	a1i	$⊢ φ \to (A, X) \in dom vol$
54		fvexd	$⊢ (φ \land t \in D) \to F (t) \in V$
55	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
56	55 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
57	51 53 54 56	iblss	$⊢ φ \to (t \in (A, X) ⟼ F (t)) \in 𝐿^{1}$
58	57	adantr	$⊢ (φ \land X \leq Y) \to (t \in (A, X) ⟼ F (t)) \in 𝐿^{1}$
59	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
60		iooss1	$⊢ (A \in ℝ^{*} \land A \leq X) \to (X, Y) \subseteq (A, Y)$
61	59 28 60	syl2anc	$⊢ φ \to (X, Y) \subseteq (A, Y)$
62	61 41	sstrd	$⊢ φ \to (X, Y) \subseteq (A, B)$
63	62 5	sstrd	$⊢ φ \to (X, Y) \subseteq D$
64		ioombl	$⊢ (X, Y) \in dom vol$
65	64	a1i	$⊢ φ \to (X, Y) \in dom vol$
66	63 65 54 56	iblss	$⊢ φ \to (t \in (X, Y) ⟼ F (t)) \in 𝐿^{1}$
67	66	adantr	$⊢ (φ \land X \leq Y) \to (t \in (X, Y) ⟼ F (t)) \in 𝐿^{1}$
68	18 22 34 47 58 67	itgsplitioo	$⊢ (φ \land X \leq Y) \to \int_{(A, Y)} F (t) d t = \int_{(A, X)} F (t) d t + \int_{(X, Y)} F (t) d t$
69	17 68	eqtrd	$⊢ (φ \land X \leq Y) \to G (Y) = \int_{(A, X)} F (t) d t + \int_{(X, Y)} F (t) d t$
70		oveq2	$⊢ x = X \to (A, x) = (A, X)$
71		itgeq1	$⊢ (A, x) = (A, X) \to \int_{(A, x)} F (t) d t = \int_{(A, X)} F (t) d t$
72	70 71	syl	$⊢ x = X \to \int_{(A, x)} F (t) d t = \int_{(A, X)} F (t) d t$
73		itgex	$⊢ \int_{(A, X)} F (t) d t \in V$
74	72 1 73	fvmpt	$⊢ X \in [A, B] \to G (X) = \int_{(A, X)} F (t) d t$
75	9 74	syl	$⊢ φ \to G (X) = \int_{(A, X)} F (t) d t$
76	75	adantr	$⊢ (φ \land X \leq Y) \to G (X) = \int_{(A, X)} F (t) d t$
77	69 76	oveq12d	$⊢ (φ \land X \leq Y) \to G (Y) - G (X) = \int_{(A, X)} F (t) d t + \int_{(X, Y)} F (t) d t - \int_{(A, X)} F (t) d t$
78		fvexd	$⊢ (φ \land t \in (A, X)) \to F (t) \in V$
79	78 57	itgcl	$⊢ φ \to \int_{(A, X)} F (t) d t \in ℂ$
80	63	sselda	$⊢ (φ \land t \in (X, Y)) \to t \in D$
81	80 45	syldan	$⊢ (φ \land t \in (X, Y)) \to F (t) \in ℂ$
82	81 66	itgcl	$⊢ φ \to \int_{(X, Y)} F (t) d t \in ℂ$
83	79 82	pncan2d	$⊢ φ \to \int_{(A, X)} F (t) d t + \int_{(X, Y)} F (t) d t - \int_{(A, X)} F (t) d t = \int_{(X, Y)} F (t) d t$
84	83	adantr	$⊢ (φ \land X \leq Y) \to \int_{(A, X)} F (t) d t + \int_{(X, Y)} F (t) d t - \int_{(A, X)} F (t) d t = \int_{(X, Y)} F (t) d t$
85	77 84	eqtrd	$⊢ (φ \land X \leq Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$

Metamath Proof Explorer

Theorem ftc1lem1

Proof