ftc2nc

Description: Choice-free proof of ftc2 . (Contributed by Brendan Leahy, 19-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ftc2nc.a	$⊢ φ \to A \in ℝ$
2		ftc2nc.b	$⊢ φ \to B \in ℝ$
3		ftc2nc.le	$⊢ φ \to A \leq B$
4		ftc2nc.c	$⊢ φ \to F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
5		ftc2nc.i	$⊢ φ \to ℝ D F \in 𝐿^{1}$
6		ftc2nc.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
7	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
8	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
9		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
10	7 8 3 9	syl3anc	$⊢ φ \to B \in [A, B]$
11		fvex	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) \in V$
12	11	fvconst2	$⊢ B \in [A, B] \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)$
13	10 12	syl	$⊢ φ \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)$
14		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
15	14	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
16	15	a1i	$⊢ φ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
17		eqid	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)$
18		ssidd	$⊢ φ \to (A, B) \subseteq (A, B)$
19		ioossre	$⊢ (A, B) \subseteq ℝ$
20	19	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
21		cncff	$⊢ F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
22	4 21	syl	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
23		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
24		ffun	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to Fun (.)$
25	23 24	ax-mp	$⊢ Fun (.)$
26		fvelima	$⊢ (Fun (.) \land s \in (.) [[A, B] \times [A, B]]) \to \exists x \in ([A, B] \times [A, B]) (.) (x) = s$
27	25 26	mpan	$⊢ s \in (.) [[A, B] \times [A, B]] \to \exists x \in ([A, B] \times [A, B]) (.) (x) = s$
28		1st2nd2	$⊢ x \in ([A, B] \times [A, B]) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
29	28	fveq2d	$⊢ x \in ([A, B] \times [A, B]) \to (.) (x) = (.) (⟨1^{st} (x), 2^{nd} (x)⟩)$
30		df-ov	$⊢ (1^{st} (x), 2^{nd} (x)) = (.) (⟨1^{st} (x), 2^{nd} (x)⟩)$
31	29 30	eqtr4di	$⊢ x \in ([A, B] \times [A, B]) \to (.) (x) = (1^{st} (x), 2^{nd} (x))$
32	31	eqeq1d	$⊢ x \in ([A, B] \times [A, B]) \to ((.) (x) = s \leftrightarrow (1^{st} (x), 2^{nd} (x)) = s)$
33	32	adantl	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to ((.) (x) = s \leftrightarrow (1^{st} (x), 2^{nd} (x)) = s)$
34	7 8	jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
35	34	adantr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (A \in ℝ^{} \land B \in ℝ^{})$
36		xp1st	$⊢ x \in ([A, B] \times [A, B]) \to 1^{st} (x) \in [A, B]$
37		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (1^{st} (x) \in [A, B] \leftrightarrow (1^{st} (x) \in ℝ^{*} \land A \leq 1^{st} (x) \land 1^{st} (x) \leq B))$
38	7 8 37	syl2anc	$⊢ φ \to (1^{st} (x) \in [A, B] \leftrightarrow (1^{st} (x) \in ℝ^{*} \land A \leq 1^{st} (x) \land 1^{st} (x) \leq B))$
39	38	biimpa	$⊢ (φ \land 1^{st} (x) \in [A, B]) \to (1^{st} (x) \in ℝ^{*} \land A \leq 1^{st} (x) \land 1^{st} (x) \leq B)$
40	39	simp2d	$⊢ (φ \land 1^{st} (x) \in [A, B]) \to A \leq 1^{st} (x)$
41	36 40	sylan2	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to A \leq 1^{st} (x)$
42		xp2nd	$⊢ x \in ([A, B] \times [A, B]) \to 2^{nd} (x) \in [A, B]$
43		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land 2^{nd} (x) \in [A, B]) \to 2^{nd} (x) \leq B$
44	43	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land 2^{nd} (x) \in [A, B]) \to 2^{nd} (x) \leq B$
45	34 42 44	syl2an	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to 2^{nd} (x) \leq B$
46		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq 1^{st} (x) \land 2^{nd} (x) \leq B)) \to (1^{st} (x), 2^{nd} (x)) \subseteq (A, B)$
47	35 41 45 46	syl12anc	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (1^{st} (x), 2^{nd} (x)) \subseteq (A, B)$
48	47	sselda	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (1^{st} (x), 2^{nd} (x))) \to t \in (A, B)$
49	22	ffvelcdmda	$⊢ (φ \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in ℂ$
50	49	adantlr	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in ℂ$
51	48 50	syldan	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (1^{st} (x), 2^{nd} (x))) \to F_{ℝ}^{'} (t) \in ℂ$
52		ioombl	$⊢ (1^{st} (x), 2^{nd} (x)) \in dom vol$
53	52	a1i	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (1^{st} (x), 2^{nd} (x)) \in dom vol$
54		fvexd	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in V$
55	22	feqmptd	$⊢ φ \to ℝ D F = (t \in (A, B) ⟼ F_{ℝ}^{'} (t))$
56	55 5	eqeltrrd	$⊢ φ \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
57	56	adantr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
58	47 53 54 57	iblss	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
59		ax-resscn	$⊢ ℝ \subseteq ℂ$
60		ssid	$⊢ ℂ \subseteq ℂ$
61		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
62	59 60 61	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
63		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
64	62 63	sselii	$⊢ abs : ℂ \underset{cn}{⟶} ℂ$
65	64	a1i	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to abs : ℂ \underset{cn}{⟶} ℂ$
66	55	reseq1d	$⊢ φ \to {F_{ℝ}^{'} ↾}_{(1^{st} (x), 2^{nd} (x))} = {(t \in (A, B) ⟼ F_{ℝ}^{'} (t)) ↾}_{(1^{st} (x), 2^{nd} (x))}$
67	66	adantr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to {F_{ℝ}^{'} ↾}_{(1^{st} (x), 2^{nd} (x))} = {(t \in (A, B) ⟼ F_{ℝ}^{'} (t)) ↾}_{(1^{st} (x), 2^{nd} (x))}$
68	47	resmptd	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to {(t \in (A, B) ⟼ F_{ℝ}^{'} (t)) ↾}_{(1^{st} (x), 2^{nd} (x))} = (t \in (1^{st} (x), 2^{nd} (x)) ⟼ F_{ℝ}^{'} (t))$
69	67 68	eqtrd	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to {F_{ℝ}^{'} ↾}_{(1^{st} (x), 2^{nd} (x))} = (t \in (1^{st} (x), 2^{nd} (x)) ⟼ F_{ℝ}^{'} (t))$
70	4	adantr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
71		rescncf	$⊢ (1^{st} (x), 2^{nd} (x)) \subseteq (A, B) \to (F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(1^{st} (x), 2^{nd} (x))}) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ)$
72	47 70 71	sylc	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to ({F_{ℝ}^{'} ↾}_{(1^{st} (x), 2^{nd} (x))}) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
73	69 72	eqeltrrd	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ F_{ℝ}^{'} (t)) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
74	65 73	cncfmpt1f	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ \|F_{ℝ}^{'} (t)\|) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
75		cnmbf	$⊢ ((1^{st} (x), 2^{nd} (x)) \in dom vol \land (t \in (1^{st} (x), 2^{nd} (x)) ⟼ \|F_{ℝ}^{'} (t)\|) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ \|F_{ℝ}^{'} (t)\|) \in MblFn$
76	52 74 75	sylancr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ \|F_{ℝ}^{'} (t)\|) \in MblFn$
77	51 58	itgcl	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to \int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t \in ℂ$
78	77	cjcld	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} \in ℂ$
79		ioossre	$⊢ (1^{st} (x), 2^{nd} (x)) \subseteq ℝ$
80	79 59	sstri	$⊢ (1^{st} (x), 2^{nd} (x)) \subseteq ℂ$
81		cncfmptc	$⊢ (\overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} \in ℂ \land (1^{st} (x), 2^{nd} (x)) \subseteq ℂ \land ℂ \subseteq ℂ) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t}) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
82	80 60 81	mp3an23	$⊢ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} \in ℂ \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t}) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
83	78 82	syl	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t}) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
84		nfcv	$⊢ \underline{Ⅎ} s F_{ℝ}^{'} (t)$
85		nfcsb1v	$⊢ \underline{Ⅎ} t ⦋ s / t ⦌ F_{ℝ}^{'} (t)$
86		csbeq1a	$⊢ t = s \to F_{ℝ}^{'} (t) = ⦋ s / t ⦌ F_{ℝ}^{'} (t)$
87	84 85 86	cbvmpt	$⊢ (t \in (1^{st} (x), 2^{nd} (x)) ⟼ F_{ℝ}^{'} (t)) = (s \in (1^{st} (x), 2^{nd} (x)) ⟼ ⦋ s / t ⦌ F_{ℝ}^{'} (t))$
88	87 73	eqeltrrid	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ ⦋ s / t ⦌ F_{ℝ}^{'} (t)) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
89	83 88	mulcncf	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} ⦋ s / t ⦌ F_{ℝ}^{'} (t)) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ$
90		cnmbf	$⊢ ((1^{st} (x), 2^{nd} (x)) \in dom vol \land (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} ⦋ s / t ⦌ F_{ℝ}^{'} (t)) : (1^{st} (x), 2^{nd} (x)) \underset{cn}{⟶} ℂ) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} ⦋ s / t ⦌ F_{ℝ}^{'} (t)) \in MblFn$
91	52 89 90	sylancr	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (s \in (1^{st} (x), 2^{nd} (x)) ⟼ \overline{\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t} ⦋ s / t ⦌ F_{ℝ}^{'} (t)) \in MblFn$
92	51 58 76 91	itgabsnc	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to \|\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t\| \leq \int_{(1^{st} (x), 2^{nd} (x))} \|F_{ℝ}^{'} (t)\| d t$
93	51	abscld	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (1^{st} (x), 2^{nd} (x))) \to \|F_{ℝ}^{'} (t)\| \in ℝ$
94		fvexd	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (1^{st} (x), 2^{nd} (x))) \to F_{ℝ}^{'} (t) \in V$
95	94 58 76	iblabsnc	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to (t \in (1^{st} (x), 2^{nd} (x)) ⟼ \|F_{ℝ}^{'} (t)\|) \in 𝐿^{1}$
96	51	absge0d	$⊢ ((φ \land x \in ([A, B] \times [A, B])) \land t \in (1^{st} (x), 2^{nd} (x))) \to 0 \leq \|F_{ℝ}^{'} (t)\|$
97	93 95 96	itgposval	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to \int_{(1^{st} (x), 2^{nd} (x))} \|F_{ℝ}^{'} (t)\| d t = \int^{2} ((t \in ℝ ⟼ if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0)))$
98	92 97	breqtrd	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to \|\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0)))$
99		itgeq1	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to \int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t = \int_{s} F_{ℝ}^{'} (t) d t$
100	99	fveq2d	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to \|\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t\| = \|\int_{s} F_{ℝ}^{'} (t) d t\|$
101		eleq2	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to (t \in (1^{st} (x), 2^{nd} (x)) \leftrightarrow t \in s)$
102	101	ifbid	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0) = if (t \in s, \|F_{ℝ}^{'} (t)\|, 0)$
103	102	mpteq2dv	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to (t \in ℝ ⟼ if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0)) = (t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))$
104	103	fveq2d	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to \int^{2} ((t \in ℝ ⟼ if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0))) = \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0)))$
105	100 104	breq12d	$⊢ (1^{st} (x), 2^{nd} (x)) = s \to (\|\int_{(1^{st} (x), 2^{nd} (x))} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in (1^{st} (x), 2^{nd} (x)), \|F_{ℝ}^{'} (t)\|, 0))) \leftrightarrow \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))))$
106	98 105	syl5ibcom	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to ((1^{st} (x), 2^{nd} (x)) = s \to \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))))$
107	33 106	sylbid	$⊢ (φ \land x \in ([A, B] \times [A, B])) \to ((.) (x) = s \to \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))))$
108	107	rexlimdva	$⊢ φ \to (\exists x \in ([A, B] \times [A, B]) (.) (x) = s \to \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))))$
109	27 108	syl5	$⊢ φ \to (s \in (.) [[A, B] \times [A, B]] \to \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0))))$
110	109	ralrimiv	$⊢ φ \to \forall s \in (.) [[A, B] \times [A, B]] \|\int_{s} F_{ℝ}^{'} (t) d t\| \leq \int^{2} ((t \in ℝ ⟼ if (t \in s, \|F_{ℝ}^{'} (t)\|, 0)))$
111	17 1 2 3 18 20 5 22 110	ftc1anc	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t) : [A, B] \underset{cn}{⟶} ℂ$
112		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
113	6 112	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
114	113	feqmptd	$⊢ φ \to F = (x \in [A, B] ⟼ F (x))$
115	114 6	eqeltrrd	$⊢ φ \to (x \in [A, B] ⟼ F (x)) : [A, B] \underset{cn}{⟶} ℂ$
116	14 16 111 115	cncfmpt2f	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) : [A, B] \underset{cn}{⟶} ℂ$
117	59	a1i	$⊢ φ \to ℝ \subseteq ℂ$
118		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
119	1 2 118	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
120		fvexd	$⊢ ((φ \land x \in [A, B]) \land t \in (A, x)) \to F_{ℝ}^{'} (t) \in V$
121	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
122	121	rexrd	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
123		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
124	1 2 123	syl2anc	$⊢ φ \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
125	124	biimpa	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
126	125	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
127		iooss2	$⊢ (B \in ℝ^{*} \land x \leq B) \to (A, x) \subseteq (A, B)$
128	122 126 127	syl2anc	$⊢ (φ \land x \in [A, B]) \to (A, x) \subseteq (A, B)$
129		ioombl	$⊢ (A, x) \in dom vol$
130	129	a1i	$⊢ (φ \land x \in [A, B]) \to (A, x) \in dom vol$
131		fvexd	$⊢ ((φ \land x \in [A, B]) \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in V$
132	56	adantr	$⊢ (φ \land x \in [A, B]) \to (t \in (A, B) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
133	128 130 131 132	iblss	$⊢ (φ \land x \in [A, B]) \to (t \in (A, x) ⟼ F_{ℝ}^{'} (t)) \in 𝐿^{1}$
134	120 133	itgcl	$⊢ (φ \land x \in [A, B]) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t \in ℂ$
135	113	ffvelcdmda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
136	134 135	subcld	$⊢ (φ \land x \in [A, B]) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) \in ℂ$
137		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
138		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
139	1 2 138	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
140	117 119 136 137 14 139	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x}$
141		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
142	141	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
143		ioossicc	$⊢ (A, B) \subseteq [A, B]$
144	143	sseli	$⊢ x \in (A, B) \to x \in [A, B]$
145	144 134	sylan2	$⊢ (φ \land x \in (A, B)) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t \in ℂ$
146	22	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
147	17 1 2 3 4 5	ftc1cnnc	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = ℝ D F$
148	117 119 134 137 14 139	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x}$
149	22	feqmptd	$⊢ φ \to ℝ D F = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
150	147 148 149	3eqtr3d	$⊢ φ \to \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t)}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
151	144 135	sylan2	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
152	114	oveq2d	$⊢ φ \to ℝ D F = \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x}$
153	117 119 135 137 14 139	dvmptntr	$⊢ φ \to \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x} = \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x}$
154	152 149 153	3eqtr3rd	$⊢ φ \to \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x))$
155	142 145 146 150 151 146 154	dvmptsub	$⊢ φ \to \frac{d (x \in (A, B)⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x))$
156	146	subidd	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x) = 0$
157	156	mpteq2dva	$⊢ φ \to (x \in (A, B) ⟼ F_{ℝ}^{'} (x) - F_{ℝ}^{'} (x)) = (x \in (A, B) ⟼ 0)$
158	140 155 157	3eqtrd	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ 0)$
159		fconstmpt	$⊢ (A, B) \times \{0\} = (x \in (A, B) ⟼ 0)$
160	158 159	eqtr4di	$⊢ φ \to \frac{d (x \in [A, B]⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))}{d_{ℝ} x} = (A, B) \times \{0\}$
161	1 2 116 160	dveq0	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) = [A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}$
162	161	fveq1d	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B)$
163		oveq2	$⊢ x = B \to (A, x) = (A, B)$
164		itgeq1	$⊢ (A, x) = (A, B) \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
165	163 164	syl	$⊢ x = B \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
166		fveq2	$⊢ x = B \to F (x) = F (B)$
167	165 166	oveq12d	$⊢ x = B \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
168		eqid	$⊢ (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) = (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x))$
169		ovex	$⊢ \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) \in V$
170	167 168 169	fvmpt	$⊢ B \in [A, B] \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
171	10 170	syl	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
172	162 171	eqtr3d	$⊢ φ \to ([A, B] \times \{(x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A)\}) (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B)$
173		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
174	7 8 3 173	syl3anc	$⊢ φ \to A \in [A, B]$
175		oveq2	$⊢ x = A \to (A, x) = (A, A)$
176		iooid	$⊢ (A, A) = \emptyset$
177	175 176	eqtrdi	$⊢ x = A \to (A, x) = \emptyset$
178		itgeq1	$⊢ (A, x) = \emptyset \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{\emptyset} F_{ℝ}^{'} (t) d t$
179	177 178	syl	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = \int_{\emptyset} F_{ℝ}^{'} (t) d t$
180		itg0	$⊢ \int_{\emptyset} F_{ℝ}^{'} (t) d t = 0$
181	179 180	eqtrdi	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t = 0$
182		fveq2	$⊢ x = A \to F (x) = F (A)$
183	181 182	oveq12d	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = 0 - F (A)$
184		df-neg	$⊢ - F (A) = 0 - F (A)$
185	183 184	eqtr4di	$⊢ x = A \to \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x) = - F (A)$
186		negex	$⊢ - F (A) \in V$
187	185 168 186	fvmpt	$⊢ A \in [A, B] \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) = - F (A)$
188	174 187	syl	$⊢ φ \to (x \in [A, B] ⟼ \int_{(A, x)} F_{ℝ}^{'} (t) d t - F (x)) (A) = - F (A)$
189	13 172 188	3eqtr3d	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = - F (A)$
190	189	oveq2d	$⊢ φ \to F (B) + \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = F (B) + (- F (A))$
191	113 10	ffvelcdmd	$⊢ φ \to F (B) \in ℂ$
192		fvexd	$⊢ (φ \land t \in (A, B)) \to F_{ℝ}^{'} (t) \in V$
193	192 56	itgcl	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t \in ℂ$
194	191 193	pncan3d	$⊢ φ \to F (B) + \int_{(A, B)} F_{ℝ}^{'} (t) d t - F (B) = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
195	113 174	ffvelcdmd	$⊢ φ \to F (A) \in ℂ$
196	191 195	negsubd	$⊢ φ \to F (B) + (- F (A)) = F (B) - F (A)$
197	190 194 196	3eqtr3d	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$

Metamath Proof Explorer

Theorem ftc2nc

Proof