Theorem ftc2nc 38757

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

Hypotheses

Ref	Expression
ftc2nc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc2nc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc2nc.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc2nc.c	⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
ftc2nc.i	⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
ftc2nc.f	⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))

Assertion

Ref	Expression
ftc2nc	⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝑡,𝐹   𝜑,𝑡

Proof of Theorem ftc2nc

Dummy variables 𝑠 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ftc2nc.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2	1	rexrd 11366	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		ftc2nc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 11366	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		ftc2nc.le	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ubicc2 13603	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
7	2, 4, 5, 6	syl3anc 1398	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
8		fvex 6903	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V
9	8	fvconst2 7214	. . . . 5 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
10	7, 9	syl 18	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
11		eqid 2760	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
12	11	subcn 25195	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
14		eqid 2760	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)
15		ssidd 3932	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16		ioossre 13545	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18		ftc2nc.i	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
19		ftc2nc.c	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
20		cncff 25223	. . . . . . . . . 10 ⊢ ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
21	19, 20	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
22		ioof 13585	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
23		ffun 6717	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (,)
25		fvelima 6955	. . . . . . . . . . . 12 ⊢ ((Fun (,) ∧ 𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
26	24, 25	mpan 703	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
27		1st2nd2 8044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
28	27	fveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
29		df-ov 7427	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
30	28, 29	eqtr4di 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((1st ‘𝑥)(,)(2nd ‘𝑥)))
31	30	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
32	31	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
33	2, 4	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
34	33	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
35		xp1st 8037	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (1st ‘𝑥) ∈ (𝐴[,]𝐵))
36		elicc1 13527	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
37	2, 4, 36	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
38	37	biimpa 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵))
39	38	simp2d 1161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (1st ‘𝑥))
40	35, 39	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → 𝐴 ≤ (1st ‘𝑥))
41		xp2nd 8038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (2nd ‘𝑥) ∈ (𝐴[,]𝐵))
42		iccleub 13539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
43	42	3expa 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
44	33, 41, 43	syl2an 608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (2nd ‘𝑥) ≤ 𝐵)
45		ioossioo 13579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ (1st ‘𝑥) ∧ (2nd ‘𝑥) ≤ 𝐵)) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
46	34, 40, 44, 45	syl12anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
47	46	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 𝑡 ∈ (𝐴(,)𝐵))
48	21	ffvelcdmda 7089	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
49	48	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
50	47, 49	syldan 603	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
51		ioombl 25895	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol
52	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol)
53		fvexd 6905	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
54	21	feqmptd 6958	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
55	54, 18	eqeltrrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
56	55	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
57	46, 52, 53, 56	iblss 26134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
58		ax-resscn 11264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
59		ssid 3931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ⊆ ℂ
60		cncfss 25229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
61	58, 59, 60	mp2an 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
62		abscncf 25231	. . . . . . . . . . . . . . . . . . . 20 ⊢ abs ∈ (ℂ–cn→ℝ)
63	61, 62	sselii 3906	. . . . . . . . . . . . . . . . . . 19 ⊢ abs ∈ (ℂ–cn→ℂ)
64	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → abs ∈ (ℂ–cn→ℂ))
65	54	reseq1d 5970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
66	65	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
67	46	resmptd 6034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
68	66, 67	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
69	19	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
70		rescncf 25227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵) → ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)))
71	46, 69, 70	sylc 66	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
72	68, 71	eqeltrrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
73	64, 72	cncfmpt1f 25244	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
74		cnmbf 25989	. . . . . . . . . . . . . . . . 17 ⊢ ((((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol ∧ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
75	51, 73, 74	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
76	50, 57	itgcl 26113	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
77	76	cjcld 15372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ)
78		ioossre 13545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℝ
79	78, 58	sstri 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ
80		cncfmptc 25242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ ∧ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
81	79, 59, 80	mp3an23 1482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
82	77, 81	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
83		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠((ℝ D 𝐹)‘𝑡)
84		nfcsb1v 3871	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)
85		csbeq1a 3861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑠 → ((ℝ D 𝐹)‘𝑡) = ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
86	83, 84, 85	cbvmpt 5206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) = (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
87	86, 72	eqeltrrid 2865	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
88	82, 87	mulcncf 25776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
89		cnmbf 25989	. . . . . . . . . . . . . . . . 17 ⊢ ((((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol ∧ (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
90	51, 88, 89	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
91	50, 57, 75, 90	itgabsnc 38744	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡)
92	50	abscld 15615	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → (abs‘((ℝ D 𝐹)‘𝑡)) ∈ ℝ)
93		fvexd 6905	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ V)
94	93, 57, 75	iblabsnc 38739	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ 𝐿1)
95	50	absge0d 15623	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑡)))
96	92, 94, 95	itgposval 26125	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡 = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
97	91, 96	breqtrd 5130	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
98		itgeq1 26102	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 = ∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡)
99	98	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) = (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡))
100		eleq2 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↔ 𝑡 ∈ 𝑠))
101	100	ifbid 4505	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0) = if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))
102	101	mpteq2dv 5198	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))
103	102	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
104	99, 103	breq12d 5115	. . . . . . . . . . . . . 14 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ((abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) ↔ (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
105	97, 104	syl5ibcom 248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
106	32, 105	sylbid 243	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
107	106	rexlimdva 3163	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
108	26, 107	syl5 35	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
109	108	ralrimiv 3153	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
110	14, 1, 3, 5, 15, 17, 18, 21, 109	ftc1anc 38756	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
111		ftc2nc.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
112		cncff 25223	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
113	111, 112	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
114	113	feqmptd 6958	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
115	114, 111	eqeltrrd 2861	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
116	11, 13, 110, 115	cncfmpt2f 25245	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
117	58	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
118		iccssre 13567	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
119	1, 3, 118	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
120		fvexd 6905	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
121	3	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
122	121	rexrd 11366	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
123		elicc2 13549	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
124	1, 3, 123	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
125	124	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
126	125	simp3d 1162	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
127		iooss2 13519	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
128	122, 126, 127	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
129		ioombl 25895	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝑥) ∈ dom vol
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
131		fvexd 6905	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
132	55	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
133	128, 130, 131, 132	iblss 26134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
134	120, 133	itgcl 26113	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
135	113	ffvelcdmda 7089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
136	134, 135	subcld 11676	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ)
137		tgioo4 25133	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
138		iccntr 25150	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
139	1, 3, 138	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
140	117, 119, 136, 137, 11, 139	dvmptntr 26300	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))))
141		reelprrecn 11299	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
142	141	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
143		ioossicc 13571	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
144	143	sseli 3905	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
145	144, 134	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
146	21	ffvelcdmda 7089	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
147	14, 1, 3, 5, 19, 18	ftc1cnnc 38747	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
148	117, 119, 134, 137, 11, 139	dvmptntr 26300	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
149	21	feqmptd 6958	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
150	147, 148, 149	3eqtr3d 2803	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
151	144, 135	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ)
152	114	oveq2d 7440	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))))
153	117, 119, 135, 137, 11, 139	dvmptntr 26300	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))))
154	152, 149, 153	3eqtr3rd 2804	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
155	142, 145, 146, 150, 151, 146, 154	dvmptsub 26296	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
156	146	subidd 11664	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
157	156	mpteq2dva 5197	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
158	140, 155, 157	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
159		fconstmpt 5713	. . . . . . . 8 ⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
160	158, 159	eqtr4di 2813	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0}))
161	1, 3, 116, 160	dveq0 26329	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)}))
162	161	fveq1d 6892	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵))
163		oveq2 7432	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
164		itgeq1 26102	. . . . . . . . 9 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
165	163, 164	syl 18	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
166		fveq2 6890	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
167	165, 166	oveq12d 7442	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
168		eqid 2760	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))
169		ovex 7457	. . . . . . 7 ⊢ (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V
170	167, 168, 169	fvmpt 6998	. . . . . 6 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
171	7, 170	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
172	162, 171	eqtr3d 2797	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
173		lbicc2 13602	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
174	2, 4, 5, 173	syl3anc 1398	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
175		oveq2 7432	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
176		iooid 13511	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐴) = ∅
177	175, 176	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
178		itgeq1 26102	. . . . . . . . . 10 ⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
179	177, 178	syl 18	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
180		itg0 26109	. . . . . . . . 9 ⊢ ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
181	179, 180	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
182		fveq2 6890	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
183	181, 182	oveq12d 7442	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴)))
184		df-neg 11551	. . . . . . 7 ⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴))
185	183, 184	eqtr4di 2813	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴))
186		negex 11562	. . . . . 6 ⊢ -(𝐹‘𝐴) ∈ V
187	185, 168, 186	fvmpt 6998	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
188	174, 187	syl 18	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
189	10, 172, 188	3eqtr3d 2803	. . 3 ⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴))
190	189	oveq2d 7440	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴)))
191	113, 7	ffvelcdmd 7090	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
192		fvexd 6905	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
193	192, 55	itgcl 26113	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
194	191, 193	pncan3d 11679	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
195	113, 174	ffvelcdmd 7090	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
196	191, 195	negsubd 11682	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
197	190, 194, 196	3eqtr3d 2803	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  Vcvv 3450  ⦋csb 3847   ⊆ wss 3896  ∅c0 4277  ifcif 4481  𝒫 cpw 4556  {csn 4584  {cpr 4586  ⟨cop 4834   class class class wbr 5102   ↦ cmpt 5185   × cxp 5649  dom cdm 5651  ran crn 5652   ↾ cres 5653   “ cima 5654  Fun wfun 6537  ⟶wf 6539  ‘cfv 6543  (class class class)co 7424  1^st c1st 8003  2^nd c2nd 8004  ℂcc 11205  ℝcr 11206  0cc0 11207   + caddc 11210   · cmul 11212  ℝ^*cxr 11349   ≤ cle 11351   − cmin 11548   -cneg 11549  (,)cioo 13483  [,]cicc 13486  ∗ccj 15272  abscabs 15410  TopOpenctopn 17601  topGenctg 17617  ℂ_fldccnfld 21687  intcnt 23344   Cn ccn 23551   ×_t ctx 23888  –cn→ccncf 25206  volcvol 25793  MblFncmbf 25944  ∫₂citg2 25946  𝐿¹cibl 25947  ∫citg 25948   D cdv 26192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-inf2 9649  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284  ax-pre-sup 11285  ax-addf 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-symdif 4197  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-disj 5070  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7697  df-ofr 7698  df-om 7882  df-1st 8005  df-2nd 8006  df-supp 8185  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-1o 8484  df-2o 8485  df-oadd 8488  df-omul 8489  df-er 8725  df-map 8857  df-pm 8858  df-ixp 8934  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-fsupp 9362  df-fi 9410  df-sup 9441  df-inf 9442  df-oi 9511  df-dju 9989  df-card 10027  df-acn 10030  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-div 11981  df-nn 12343  df-2 12412  df-3 12413  df-4 12414  df-5 12415  df-6 12416  df-7 12417  df-8 12418  df-9 12419  df-n0 12614  df-z 12701  df-dec 12822  df-uz 12973  df-q 13083  df-rp 13128  df-xneg 13248  df-xadd 13249  df-xmul 13250  df-ioo 13487  df-ico 13489  df-icc 13490  df-fz 13647  df-fzo 13796  df-fl 13939  df-mod 14017  df-seq 14152  df-exp 14212  df-hash 14482  df-cj 15275  df-re 15276  df-im 15277  df-sqrt 15411  df-abs 15412  df-clim 15664  df-rlim 15665  df-sum 15863  df-struct 17334  df-sets 17351  df-slot 17369  df-ndx 17381  df-base 17397  df-ress 17418  df-plusg 17450  df-mulr 17451  df-starv 17452  df-sca 17453  df-vsca 17454  df-ip 17455  df-tset 17456  df-ple 17457  df-ds 17459  df-unif 17460  df-hom 17461  df-cco 17462  df-rest 17602  df-topn 17603  df-0g 17621  df-gsum 17622  df-topgen 17623  df-pt 17624  df-prds 17627  df-xrs 17683  df-qtop 17688  df-imas 17689  df-xps 17691  df-mre 17765  df-mrc 17766  df-acs 17768  df-mgm 18825  df-sgrp 18917  df-mnd 18933  df-submnd 18988  df-mulg 19287  df-cntz 19540  df-cmn 20005  df-psmet 21679  df-xmet 21680  df-met 21681  df-bl 21682  df-mopn 21683  df-fbas 21684  df-fg 21685  df-cnfld 21688  df-top 23221  df-topon 23238  df-topsp 23260  df-bases 23273  df-cld 23346  df-ntr 23347  df-cls 23348  df-nei 23425  df-lp 23463  df-perf 23464  df-cn 23554  df-cnp 23555  df-haus 23642  df-cmp 23714  df-tx 23890  df-hmeo 24083  df-fil 24174  df-fm 24266  df-flim 24267  df-flf 24268  df-xms 24648  df-ms 24649  df-tms 24650  df-cncf 25208  df-ovol 25794  df-vol 25795  df-mbf 25949  df-itg1 25950  df-itg2 25951  df-ibl 25952  df-itg 25953  df-0p 26000  df-limc 26195  df-dv 26196

This theorem is used by:  areacirc  38768