ftc1lem2

	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	ftc1lem2	$⊢ φ \to G : [A, B] ⟶ ℂ$

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		fvexd	$⊢ ((φ \land x \in [A, B]) \land t \in (A, x)) \to F (t) \in V$
10	3	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
11	10	rexrd	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
12		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
13	2 3 12	syl2anc	$⊢ φ \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
14	13	biimpa	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
15	14	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
16		iooss2	$⊢ (B \in ℝ^{*} \land x \leq B) \to (A, x) \subseteq (A, B)$
17	11 15 16	syl2anc	$⊢ (φ \land x \in [A, B]) \to (A, x) \subseteq (A, B)$
18	5	adantr	$⊢ (φ \land x \in [A, B]) \to (A, B) \subseteq D$
19	17 18	sstrd	$⊢ (φ \land x \in [A, B]) \to (A, x) \subseteq D$
20		ioombl	$⊢ (A, x) \in dom vol$
21	20	a1i	$⊢ (φ \land x \in [A, B]) \to (A, x) \in dom vol$
22		fvexd	$⊢ ((φ \land x \in [A, B]) \land t \in D) \to F (t) \in V$
23	8	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
24	23 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
25	24	adantr	$⊢ (φ \land x \in [A, B]) \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
26	19 21 22 25	iblss	$⊢ (φ \land x \in [A, B]) \to (t \in (A, x) ⟼ F (t)) \in 𝐿^{1}$
27	9 26	itgcl	$⊢ (φ \land x \in [A, B]) \to \int_{(A, x)} F (t) d t \in ℂ$
28	27 1	fmptd	$⊢ φ \to G : [A, B] ⟶ ℂ$

Metamath Proof Explorer

Theorem ftc1lem2

Proof