ftc1lem3

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	12	cnfldtopon	$⊢ L \in TopOn (ℂ)$
14		ax-resscn	$⊢ ℝ \subseteq ℂ$
15	6 14	sstrdi	$⊢ φ \to D \subseteq ℂ$
16		resttopon	$⊢ (L \in TopOn (ℂ) \land D \subseteq ℂ) \to L ↾_{𝑡} D \in TopOn (D)$
17	13 15 16	sylancr	$⊢ φ \to L ↾_{𝑡} D \in TopOn (D)$
18	11 17	eqeltrid	$⊢ φ \to K \in TopOn (D)$
19	13	a1i	$⊢ φ \to L \in TopOn (ℂ)$
20		cnpf2	$⊢ (K \in TopOn (D) \land L \in TopOn (ℂ) \land F \in (K CnP L) (C)) \to F : D ⟶ ℂ$
21	18 19 9 20	syl3anc	$⊢ φ \to F : D ⟶ ℂ$

Metamath Proof Explorer