Theorem ftc2nc 38451

Description: Choice-free proof of ftc2 26271. (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 11283	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		ftc2nc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 11283	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		ftc2nc.le	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ubicc2 13518	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
7	2, 4, 5, 6	syl3anc 1398	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
8		fvex 6891	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V
9	8	fvconst2 7203	. . . . 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 25093	. . . . . . . . 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 3954	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16		ioossre 13460	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18		ftc2nc.i	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
19		ftc2nc.c	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
20		cncff 25121	. . . . . . . . . 10 ⊢ ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
21	19, 20	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
22		ioof 13500	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
23		ffun 6705	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (,)
25		fvelima 6943	. . . . . . . . . . . 12 ⊢ ((Fun (,) ∧ 𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
26	24, 25	mpan 703	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
27		1st2nd2 8025	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
28	27	fveq2d 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
29		df-ov 7416	. . . . . . . . . . . . . . . 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 8018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (1st ‘𝑥) ∈ (𝐴[,]𝐵))
36		elicc1 13442	. . . . . . . . . . . . . . . . . . . . . . 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 8019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (2nd ‘𝑥) ∈ (𝐴[,]𝐵))
42		iccleub 13454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
43	42	3expa 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
44	33, 41, 43	syl2an 608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (2nd ‘𝑥) ≤ 𝐵)
45		ioossioo 13494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ (1st ‘𝑥) ∧ (2nd ‘𝑥) ≤ 𝐵)) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
46	34, 40, 44, 45	syl12anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
47	46	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 𝑡 ∈ (𝐴(,)𝐵))
48	21	ffvelcdmda 7077	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
49	48	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
50	47, 49	syldan 603	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
51		ioombl 25793	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol
52	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol)
53		fvexd 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
54	21	feqmptd 6946	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
55	54, 18	eqeltrrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
56	55	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
57	46, 52, 53, 56	iblss 26032	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
58		ax-resscn 11181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
59		ssid 3953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ⊆ ℂ
60		cncfss 25127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
61	58, 59, 60	mp2an 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
62		abscncf 25129	. . . . . . . . . . . . . . . . . . . 20 ⊢ abs ∈ (ℂ–cn→ℝ)
63	61, 62	sselii 3928	. . . . . . . . . . . . . . . . . . 19 ⊢ abs ∈ (ℂ–cn→ℂ)
64	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → abs ∈ (ℂ–cn→ℂ))
65	54	reseq1d 5971	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
66	65	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
67	46	resmptd 6036	. . . . . . . . . . . . . . . . . . . 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 25125	. . . . . . . . . . . . . . . . . . . 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 25142	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
74		cnmbf 25887	. . . . . . . . . . . . . . . . 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 26011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
77	76	cjcld 15283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ)
78		ioossre 13460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℝ
79	78, 58	sstri 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ
80		cncfmptc 25140	. . . . . . . . . . . . . . . . . . . 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 5207	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) = (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
87	86, 72	eqeltrrid 2865	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
88	82, 87	mulcncf 25674	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
89		cnmbf 25887	. . . . . . . . . . . . . . . . 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 38438	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡)
92	50	abscld 15526	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → (abs‘((ℝ D 𝐹)‘𝑡)) ∈ ℝ)
93		fvexd 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ V)
94	93, 57, 75	iblabsnc 38433	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ 𝐿1)
95	50	absge0d 15534	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑡)))
96	92, 94, 95	itgposval 26023	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡 = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
97	91, 96	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
98		itgeq1 26000	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 = ∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡)
99	98	fveq2d 6882	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) = (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡))
100		eleq2 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↔ 𝑡 ∈ 𝑠))
101	100	ifbid 4506	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0) = if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))
102	101	mpteq2dv 5199	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))
103	102	fveq2d 6882	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
104	99, 103	breq12d 5116	. . . . . . . . . . . . . 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 38450	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
111		ftc2nc.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
112		cncff 25121	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
113	111, 112	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
114	113	feqmptd 6946	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
115	114, 111	eqeltrrd 2861	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
116	11, 13, 110, 115	cncfmpt2f 25143	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
117	58	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
118		iccssre 13482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
119	1, 3, 118	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
120		fvexd 6893	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
121	3	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
122	121	rexrd 11283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
123		elicc2 13464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
124	1, 3, 123	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
125	124	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
126	125	simp3d 1162	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
127		iooss2 13434	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
128	122, 126, 127	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
129		ioombl 25793	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝑥) ∈ dom vol
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
131		fvexd 6893	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
132	55	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
133	128, 130, 131, 132	iblss 26032	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
134	120, 133	itgcl 26011	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
135	113	ffvelcdmda 7077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
136	134, 135	subcld 11593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ)
137		tgioo4 25031	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
138		iccntr 25048	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
139	1, 3, 138	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
140	117, 119, 136, 137, 11, 139	dvmptntr 26198	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))))
141		reelprrecn 11216	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
142	141	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
143		ioossicc 13486	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
144	143	sseli 3927	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
145	144, 134	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
146	21	ffvelcdmda 7077	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
147	14, 1, 3, 5, 19, 18	ftc1cnnc 38441	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
148	117, 119, 134, 137, 11, 139	dvmptntr 26198	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
149	21	feqmptd 6946	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
150	147, 148, 149	3eqtr3d 2803	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
151	144, 135	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ)
152	114	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))))
153	117, 119, 135, 137, 11, 139	dvmptntr 26198	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))))
154	152, 149, 153	3eqtr3rd 2804	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
155	142, 145, 146, 150, 151, 146, 154	dvmptsub 26194	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
156	146	subidd 11581	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
157	156	mpteq2dva 5198	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
158	140, 155, 157	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
159		fconstmpt 5717	. . . . . . . 8 ⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
160	158, 159	eqtr4di 2813	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0}))
161	1, 3, 116, 160	dveq0 26227	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)}))
162	161	fveq1d 6880	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵))
163		oveq2 7421	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
164		itgeq1 26000	. . . . . . . . 9 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
165	163, 164	syl 18	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
166		fveq2 6878	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
167	165, 166	oveq12d 7431	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
168		eqid 2760	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))
169		ovex 7446	. . . . . . 7 ⊢ (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V
170	167, 168, 169	fvmpt 6986	. . . . . 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 13517	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
174	2, 4, 5, 173	syl3anc 1398	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
175		oveq2 7421	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
176		iooid 13426	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐴) = ∅
177	175, 176	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
178		itgeq1 26000	. . . . . . . . . 10 ⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
179	177, 178	syl 18	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
180		itg0 26007	. . . . . . . . 9 ⊢ ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
181	179, 180	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
182		fveq2 6878	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
183	181, 182	oveq12d 7431	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴)))
184		df-neg 11468	. . . . . . 7 ⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴))
185	183, 184	eqtr4di 2813	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴))
186		negex 11479	. . . . . 6 ⊢ -(𝐹‘𝐴) ∈ V
187	185, 168, 186	fvmpt 6986	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
188	174, 187	syl 18	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
189	10, 172, 188	3eqtr3d 2803	. . 3 ⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴))
190	189	oveq2d 7429	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴)))
191	113, 7	ffvelcdmd 7078	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
192		fvexd 6893	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
193	192, 55	itgcl 26011	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
194	191, 193	pncan3d 11596	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
195	113, 174	ffvelcdmd 7078	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
196	191, 195	negsubd 11599	. 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 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  ⦋csb 3847   ⊆ wss 3899  ∅c0 4279  ifcif 4482  𝒫 cpw 4557  {csn 4584  {cpr 4586  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186   × cxp 5653  dom cdm 5655  ran crn 5656   ↾ cres 5657   “ cima 5658  Fun wfun 6527  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413  1^st c1st 7984  2^nd c2nd 7985  ℂcc 11122  ℝcr 11123  0cc0 11124   + caddc 11127   · cmul 11129  ℝ^*cxr 11266   ≤ cle 11268   − cmin 11465  -cneg 11466  (,)cioo 13398  [,]cicc 13401  ∗ccj 15183  abscabs 15321  TopOpenctopn 17506  topGenctg 17522  ℂ_fldccnfld 21585  intcnt 23242   Cn ccn 23449   ×_t ctx 23786  –cn→ccncf 25104  volcvol 25691  MblFncmbf 25842  ∫₂citg2 25844  𝐿¹cibl 25845  ∫citg 25846   D cdv 26090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-inf2 9620  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202  ax-addf 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-symdif 4199  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-disj 5071  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7678  df-ofr 7679  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-omul 8460  df-er 8696  df-map 8828  df-pm 8829  df-ixp 8905  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-fsupp 9332  df-fi 9381  df-sup 9412  df-inf 9413  df-oi 9482  df-dju 9906  df-card 9944  df-acn 9947  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-div 11896  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-z 12616  df-dec 12737  df-uz 12888  df-q 12998  df-rp 13043  df-xneg 13163  df-xadd 13164  df-xmul 13165  df-ioo 13402  df-ico 13404  df-icc 13405  df-fz 13562  df-fzo 13710  df-fl 13853  df-mod 13931  df-seq 14066  df-exp 14126  df-hash 14395  df-cj 15186  df-re 15187  df-im 15188  df-sqrt 15322  df-abs 15323  df-clim 15575  df-rlim 15576  df-sum 15774  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-mulr 17356  df-starv 17357  df-sca 17358  df-vsca 17359  df-ip 17360  df-tset 17361  df-ple 17362  df-ds 17364  df-unif 17365  df-hom 17366  df-cco 17367  df-rest 17507  df-topn 17508  df-0g 17526  df-gsum 17527  df-topgen 17528  df-pt 17529  df-prds 17532  df-xrs 17588  df-qtop 17593  df-imas 17594  df-xps 17596  df-mre 17670  df-mrc 17671  df-acs 17673  df-mgm 18730  df-sgrp 18821  df-mnd 18837  df-submnd 18892  df-mulg 19191  df-cntz 19444  df-cmn 19909  df-psmet 21577  df-xmet 21578  df-met 21579  df-bl 21580  df-mopn 21581  df-fbas 21582  df-fg 21583  df-cnfld 21586  df-top 23119  df-topon 23136  df-topsp 23158  df-bases 23171  df-cld 23244  df-ntr 23245  df-cls 23246  df-nei 23323  df-lp 23361  df-perf 23362  df-cn 23452  df-cnp 23453  df-haus 23540  df-cmp 23612  df-tx 23788  df-hmeo 23981  df-fil 24072  df-fm 24164  df-flim 24165  df-flf 24166  df-xms 24546  df-ms 24547  df-tms 24548  df-cncf 25106  df-ovol 25692  df-vol 25693  df-mbf 25847  df-itg1 25848  df-itg2 25849  df-ibl 25850  df-itg 25851  df-0p 25898  df-limc 26093  df-dv 26094

This theorem is used by:  areacirc  38462