Theorem ftc2nc 34970

Description: Choice-free proof of ftc2 24635. (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 10685	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		ftc2nc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 10685	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		ftc2nc.le	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ubicc2 12847	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
7	2, 4, 5, 6	syl3anc 1367	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
8		fvex 6677	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V
9	8	fvconst2 6960	. . . . 5 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
10	7, 9	syl 17	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
11		eqid 2821	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
12	11	subcn 23468	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
14		eqid 2821	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)
15		ssidd 3989	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16		ioossre 12792	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18		ftc2nc.i	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
19		ftc2nc.c	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
20		cncff 23495	. . . . . . . . . 10 ⊢ ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
22		ioof 12829	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
23		ffun 6511	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (,)
25		fvelima 6725	. . . . . . . . . . . 12 ⊢ ((Fun (,) ∧ 𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
26	24, 25	mpan 688	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
27		1st2nd2 7722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
28	27	fveq2d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
29		df-ov 7153	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
30	28, 29	syl6eqr 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((1st ‘𝑥)(,)(2nd ‘𝑥)))
31	30	eqeq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
32	31	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
33	2, 4	jca 514	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
34	33	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
35		xp1st 7715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (1st ‘𝑥) ∈ (𝐴[,]𝐵))
36		elicc1 12776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
37	2, 4, 36	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
38	37	biimpa 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵))
39	38	simp2d 1139	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (1st ‘𝑥))
40	35, 39	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → 𝐴 ≤ (1st ‘𝑥))
41		xp2nd 7716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (2nd ‘𝑥) ∈ (𝐴[,]𝐵))
42		iccleub 12786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
43	42	3expa 1114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
44	33, 41, 43	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (2nd ‘𝑥) ≤ 𝐵)
45		ioossioo 12823	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ (1st ‘𝑥) ∧ (2nd ‘𝑥) ≤ 𝐵)) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
46	34, 40, 44, 45	syl12anc 834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
47	46	sselda 3966	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 𝑡 ∈ (𝐴(,)𝐵))
48	21	ffvelrnda 6845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
49	48	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
50	47, 49	syldan 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
51		ioombl 24160	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol
52	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol)
53		fvexd 6679	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
54	21	feqmptd 6727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
55	54, 18	eqeltrrd 2914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
56	55	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
57	46, 52, 53, 56	iblss 24399	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
58		ax-resscn 10588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
59		ssid 3988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ⊆ ℂ
60		cncfss 23501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
61	58, 59, 60	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
62		abscncf 23503	. . . . . . . . . . . . . . . . . . . 20 ⊢ abs ∈ (ℂ–cn→ℝ)
63	61, 62	sselii 3963	. . . . . . . . . . . . . . . . . . 19 ⊢ abs ∈ (ℂ–cn→ℂ)
64	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → abs ∈ (ℂ–cn→ℂ))
65	54	reseq1d 5846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
66	65	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
67	46	resmptd 5902	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
68	66, 67	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
69	19	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
70		rescncf 23499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵) → ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)))
71	46, 69, 70	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
72	68, 71	eqeltrrd 2914	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
73	64, 72	cncfmpt1f 23515	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
74		cnmbf 24254	. . . . . . . . . . . . . . . . 17 ⊢ ((((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol ∧ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
75	51, 73, 74	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
76	50, 57	itgcl 24378	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
77	76	cjcld 14549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ)
78		ioossre 12792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℝ
79	78, 58	sstri 3975	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ
80		cncfmptc 23513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ ∧ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
81	79, 59, 80	mp3an23 1449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
82	77, 81	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
83		nfcv 2977	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠((ℝ D 𝐹)‘𝑡)
84		nfcsb1v 3906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)
85		csbeq1a 3896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑠 → ((ℝ D 𝐹)‘𝑡) = ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
86	83, 84, 85	cbvmpt 5159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) = (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
87	86, 72	eqeltrrid 2918	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
88	82, 87	mulcncf 24041	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
89		cnmbf 24254	. . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
91	50, 57, 75, 90	itgabsnc 34955	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡)
92	50	abscld 14790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → (abs‘((ℝ D 𝐹)‘𝑡)) ∈ ℝ)
93		fvexd 6679	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ V)
94	93, 57, 75	iblabsnc 34950	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ 𝐿1)
95	50	absge0d 14798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑡)))
96	92, 94, 95	itgposval 24390	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡 = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
97	91, 96	breqtrd 5084	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
98		itgeq1 24367	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 = ∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡)
99	98	fveq2d 6668	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) = (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡))
100		eleq2 2901	. . . . . . . . . . . . . . . . . 18 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↔ 𝑡 ∈ 𝑠))
101	100	ifbid 4488	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0) = if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))
102	101	mpteq2dv 5154	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))
103	102	fveq2d 6668	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
104	99, 103	breq12d 5071	. . . . . . . . . . . . . 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 247	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
106	32, 105	sylbid 242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
107	106	rexlimdva 3284	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
108	26, 107	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
109	108	ralrimiv 3181	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
110	14, 1, 3, 5, 15, 17, 18, 21, 109	ftc1anc 34969	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
111		ftc2nc.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
112		cncff 23495	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
113	111, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
114	113	feqmptd 6727	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
115	114, 111	eqeltrrd 2914	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
116	11, 13, 110, 115	cncfmpt2f 23516	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
117	58	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
118		iccssre 12812	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
119	1, 3, 118	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
120		fvexd 6679	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
121	3	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
122	121	rexrd 10685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
123		elicc2 12795	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
124	1, 3, 123	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
125	124	biimpa 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
126	125	simp3d 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
127		iooss2 12768	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
128	122, 126, 127	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
129		ioombl 24160	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝑥) ∈ dom vol
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
131		fvexd 6679	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
132	55	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
133	128, 130, 131, 132	iblss 24399	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
134	120, 133	itgcl 24378	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
135	113	ffvelrnda 6845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
136	134, 135	subcld 10991	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ)
137	11	tgioo2 23405	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
138		iccntr 23423	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
139	1, 3, 138	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
140	117, 119, 136, 137, 11, 139	dvmptntr 24562	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))))
141		reelprrecn 10623	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
142	141	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
143		ioossicc 12816	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
144	143	sseli 3962	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
145	144, 134	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
146	21	ffvelrnda 6845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
147	14, 1, 3, 5, 19, 18	ftc1cnnc 34960	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
148	117, 119, 134, 137, 11, 139	dvmptntr 24562	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
149	21	feqmptd 6727	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
150	147, 148, 149	3eqtr3d 2864	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
151	144, 135	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ)
152	114	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))))
153	117, 119, 135, 137, 11, 139	dvmptntr 24562	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))))
154	152, 149, 153	3eqtr3rd 2865	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
155	142, 145, 146, 150, 151, 146, 154	dvmptsub 24558	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
156	146	subidd 10979	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
157	156	mpteq2dva 5153	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
158	140, 155, 157	3eqtrd 2860	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
159		fconstmpt 5608	. . . . . . . 8 ⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
160	158, 159	syl6eqr 2874	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0}))
161	1, 3, 116, 160	dveq0 24591	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)}))
162	161	fveq1d 6666	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵))
163		oveq2 7158	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
164		itgeq1 24367	. . . . . . . . 9 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
165	163, 164	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
166		fveq2 6664	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
167	165, 166	oveq12d 7168	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
168		eqid 2821	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))
169		ovex 7183	. . . . . . 7 ⊢ (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V
170	167, 168, 169	fvmpt 6762	. . . . . 6 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
171	7, 170	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
172	162, 171	eqtr3d 2858	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
173		lbicc2 12846	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
174	2, 4, 5, 173	syl3anc 1367	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
175		oveq2 7158	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
176		iooid 12760	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐴) = ∅
177	175, 176	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
178		itgeq1 24367	. . . . . . . . . 10 ⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
179	177, 178	syl 17	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
180		itg0 24374	. . . . . . . . 9 ⊢ ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
181	179, 180	syl6eq 2872	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
182		fveq2 6664	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
183	181, 182	oveq12d 7168	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴)))
184		df-neg 10867	. . . . . . 7 ⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴))
185	183, 184	syl6eqr 2874	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴))
186		negex 10878	. . . . . 6 ⊢ -(𝐹‘𝐴) ∈ V
187	185, 168, 186	fvmpt 6762	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
188	174, 187	syl 17	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
189	10, 172, 188	3eqtr3d 2864	. . 3 ⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴))
190	189	oveq2d 7166	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴)))
191	113, 7	ffvelrnd 6846	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
192		fvexd 6679	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
193	192, 55	itgcl 24378	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
194	191, 193	pncan3d 10994	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
195	113, 174	ffvelrnd 6846	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
196	191, 195	negsubd 10997	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
197	190, 194, 196	3eqtr3d 2864	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∃wrex 3139  Vcvv 3494  ⦋csb 3882   ⊆ wss 3935  ∅c0 4290  ifcif 4466  𝒫 cpw 4538  {csn 4560  {cpr 4562  ⟨cop 4566   class class class wbr 5058   ↦ cmpt 5138   × cxp 5547  dom cdm 5549  ran crn 5550   ↾ cres 5551   “ cima 5552  Fun wfun 6343  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150  1^st c1st 7681  2^nd c2nd 7682  ℂcc 10529  ℝcr 10530  0cc0 10531   + caddc 10534   · cmul 10536  ℝ^*cxr 10668   ≤ cle 10670   − cmin 10864  -cneg 10865  (,)cioo 12732  [,]cicc 12735  ∗ccj 14449  abscabs 14587  TopOpenctopn 16689  topGenctg 16705  ℂ_fldccnfld 20539  intcnt 21619   Cn ccn 21826   ×_t ctx 22162  –cn→ccncf 23478  volcvol 24058  MblFncmbf 24209  ∫₂citg2 24211  𝐿¹cibl 24212  ∫citg 24213   D cdv 24455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-symdif 4218  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-iin 4914  df-disj 5024  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-omul 8101  df-er 8283  df-map 8402  df-pm 8403  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-acn 9365  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-q 12343  df-rp 12384  df-xneg 12501  df-xadd 12502  df-xmul 12503  df-ioo 12736  df-ico 12738  df-icc 12739  df-fz 12887  df-fzo 13028  df-fl 13156  df-mod 13232  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-rlim 14840  df-sum 15037  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-hom 16583  df-cco 16584  df-rest 16690  df-topn 16691  df-0g 16709  df-gsum 16710  df-topgen 16711  df-pt 16712  df-prds 16715  df-xrs 16769  df-qtop 16774  df-imas 16775  df-xps 16777  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-mulg 18219  df-cntz 18441  df-cmn 18902  df-psmet 20531  df-xmet 20532  df-met 20533  df-bl 20534  df-mopn 20535  df-fbas 20536  df-fg 20537  df-cnfld 20540  df-top 21496  df-topon 21513  df-topsp 21535  df-bases 21548  df-cld 21621  df-ntr 21622  df-cls 21623  df-nei 21700  df-lp 21738  df-perf 21739  df-cn 21829  df-cnp 21830  df-haus 21917  df-cmp 21989  df-tx 22164  df-hmeo 22357  df-fil 22448  df-fm 22540  df-flim 22541  df-flf 22542  df-xms 22924  df-ms 22925  df-tms 22926  df-cncf 23480  df-ovol 24059  df-vol 24060  df-mbf 24214  df-itg1 24215  df-itg2 24216  df-ibl 24217  df-itg 24218  df-0p 24265  df-limc 24458  df-dv 24459

This theorem is referenced by:  areacirc  34981