ftc2nc - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ftc2nc		Structured version Visualization version GIF version

Theorem ftc2nc 36559

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

**Hypotheses**
Ref	Expression
ftc2nc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc2nc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc2nc.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc2nc.c	⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
ftc2nc.i	⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿¹)
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 11261	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
3		ftc2nc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 11261	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
5		ftc2nc.le	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ubicc2 13439	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
7	2, 4, 5, 6	syl3anc 1372	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
8		fvex 6902	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V
9	8	fvconst2 7202	. . . . 5 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
10	7, 9	syl 17	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
11		eqid 2733	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
12	11	subcn 24374	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
14		eqid 2733	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)
15		ssidd 4005	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16		ioossre 13382	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18		ftc2nc.i	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿¹)
19		ftc2nc.c	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
20		cncff 24401	. . . . . . . . . 10 ⊢ ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
22		ioof 13421	. . . . . . . . . . . . 13 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
23		ffun 6718	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → Fun (,))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (,)
25		fvelima 6955	. . . . . . . . . . . 12 ⊢ ((Fun (,) ∧ 𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
26	24, 25	mpan 689	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
27		1st2nd2 8011	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
28	27	fveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((,)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
29		df-ov 7409	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = ((,)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
30	28, 29	eqtr4di 2791	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((1^st ‘𝑥)(,)(2^nd ‘𝑥)))
31	30	eqeq1d 2735	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (((,)‘𝑥) = 𝑠 ↔ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠))
32	31	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 ↔ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠))
33	2, 4	jca 513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
34	33	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
35		xp1st 8004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (1^st ‘𝑥) ∈ (𝐴[,]𝐵))
36		elicc1 13365	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ((1^st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1^st ‘𝑥) ∈ ℝ^ ∧ 𝐴 ≤ (1^st ‘𝑥) ∧ (1^st ‘𝑥) ≤ 𝐵)))
37	2, 4, 36	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1^st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1^st ‘𝑥) ∈ ℝ^* ∧ 𝐴 ≤ (1^st ‘𝑥) ∧ (1^st ‘𝑥) ≤ 𝐵)))
38	37	biimpa 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (1^st ‘𝑥) ∈ (𝐴[,]𝐵)) → ((1^st ‘𝑥) ∈ ℝ^* ∧ 𝐴 ≤ (1^st ‘𝑥) ∧ (1^st ‘𝑥) ≤ 𝐵))
39	38	simp2d 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (1^st ‘𝑥) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (1^st ‘𝑥))
40	35, 39	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → 𝐴 ≤ (1^st ‘𝑥))
41		xp2nd 8005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (2^nd ‘𝑥) ∈ (𝐴[,]𝐵))
42		iccleub 13376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (2^nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2^nd ‘𝑥) ≤ 𝐵)
43	42	3expa 1119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (2^nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2^nd ‘𝑥) ≤ 𝐵)
44	33, 41, 43	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (2^nd ‘𝑥) ≤ 𝐵)
45		ioossioo 13415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 ≤ (1^st ‘𝑥) ∧ (2^nd ‘𝑥) ≤ 𝐵)) → ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
46	34, 40, 44, 45	syl12anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
47	46	sselda 3982	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) → 𝑡 ∈ (𝐴(,)𝐵))
48	21	ffvelcdmda 7084	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
49	48	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
50	47, 49	syldan 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
51		ioombl 25074	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ∈ dom vol
52	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ∈ dom vol)
53		fvexd 6904	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
54	21	feqmptd 6958	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
55	54, 18	eqeltrrd 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿¹)
56	55	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿¹)
57	46, 52, 53, 56	iblss 25314	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿¹)
58		ax-resscn 11164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
59		ssid 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ⊆ ℂ
60		cncfss 24407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
61	58, 59, 60	mp2an 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
62		abscncf 24409	. . . . . . . . . . . . . . . . . . . 20 ⊢ abs ∈ (ℂ–cn→ℝ)
63	61, 62	sselii 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ abs ∈ (ℂ–cn→ℂ)
64	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → abs ∈ (ℂ–cn→ℂ))
65	54	reseq1d 5979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))))
66	65	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))))
67	46	resmptd 6039	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) = (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
68	66, 67	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) = (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
69	19	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
70		rescncf 24405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ (𝐴(,)𝐵) → ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → ((ℝ D 𝐹) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ)))
71	46, 69, 70	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
72	68, 71	eqeltrrd 2835	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
73	64, 72	cncfmpt1f 24422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
74		cnmbf 25168	. . . . . . . . . . . . . . . . 17 ⊢ ((((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ∈ dom vol ∧ (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ)) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
75	51, 73, 74	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
76	50, 57	itgcl 25293	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
77	76	cjcld 15140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ)
78		ioossre 13382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ ℝ
79	78, 58	sstri 3991	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ ℂ
80		cncfmptc 24420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ ∧ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
81	79, 59, 80	mp3an23 1454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
82	77, 81	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
83		nfcv 2904	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠((ℝ D 𝐹)‘𝑡)
84		nfcsb1v 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)
85		csbeq1a 3907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑠 → ((ℝ D 𝐹)‘𝑡) = ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
86	83, 84, 85	cbvmpt 5259	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) = (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
87	86, 72	eqeltrrid 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
88	82, 87	mulcncf 24955	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ))
89		cnmbf 25168	. . . . . . . . . . . . . . . . 17 ⊢ ((((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ∈ dom vol ∧ (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1^st ‘𝑥)(,)(2^nd ‘𝑥))–cn→ℂ)) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
90	51, 88, 89	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ ((∗‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
91	50, 57, 75, 90	itgabsnc 36546	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ ∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡)
92	50	abscld 15380	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) → (abs‘((ℝ D 𝐹)‘𝑡)) ∈ ℝ)
93		fvexd 6904	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ V)
94	93, 57, 75	iblabsnc 36541	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ 𝐿¹)
95	50	absge0d 15388	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥))) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑡)))
96	92, 94, 95	itgposval 25305	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡 = (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
97	91, 96	breqtrd 5174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
98		itgeq1 25282	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → ∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 = ∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡)
99	98	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → (abs‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) = (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡))
100		eleq2 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)) ↔ 𝑡 ∈ 𝑠))
101	100	ifbid 4551	. . . . . . . . . . . . . . . . 17 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0) = if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))
102	101	mpteq2dv 5250	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))
103	102	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) = (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
104	99, 103	breq12d 5161	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → ((abs‘∫((1^st ‘𝑥)(,)(2^nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1^st ‘𝑥)(,)(2^nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) ↔ (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
105	97, 104	syl5ibcom 244	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((1^st ‘𝑥)(,)(2^nd ‘𝑥)) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
106	32, 105	sylbid 239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
107	106	rexlimdva 3156	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
108	26, 107	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
109	108	ralrimiv 3146	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫₂‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
110	14, 1, 3, 5, 15, 17, 18, 21, 109	ftc1anc 36558	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
111		ftc2nc.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
112		cncff 24401	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
113	111, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
114	113	feqmptd 6958	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
115	114, 111	eqeltrrd 2835	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
116	11, 13, 110, 115	cncfmpt2f 24423	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
117	58	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
118		iccssre 13403	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
119	1, 3, 118	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
120		fvexd 6904	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
121	3	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
122	121	rexrd 11261	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ^*)
123		elicc2 13386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
124	1, 3, 123	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
125	124	biimpa 478	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
126	125	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
127		iooss2 13357	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
128	122, 126, 127	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
129		ioombl 25074	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝑥) ∈ dom vol
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
131		fvexd 6904	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
132	55	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿¹)
133	128, 130, 131, 132	iblss 25314	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿¹)
134	120, 133	itgcl 25293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
135	113	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
136	134, 135	subcld 11568	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ)
137	11	tgioo2 24311	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
138		iccntr 24329	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
139	1, 3, 138	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
140	117, 119, 136, 137, 11, 139	dvmptntr 25480	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))))
141		reelprrecn 11199	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
142	141	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
143		ioossicc 13407	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
144	143	sseli 3978	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
145	144, 134	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
146	21	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
147	14, 1, 3, 5, 19, 18	ftc1cnnc 36549	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
148	117, 119, 134, 137, 11, 139	dvmptntr 25480	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
149	21	feqmptd 6958	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
150	147, 148, 149	3eqtr3d 2781	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
151	144, 135	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ)
152	114	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))))
153	117, 119, 135, 137, 11, 139	dvmptntr 25480	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))))
154	152, 149, 153	3eqtr3rd 2782	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
155	142, 145, 146, 150, 151, 146, 154	dvmptsub 25476	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
156	146	subidd 11556	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
157	156	mpteq2dva 5248	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
158	140, 155, 157	3eqtrd 2777	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
159		fconstmpt 5737	. . . . . . . 8 ⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
160	158, 159	eqtr4di 2791	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0}))
161	1, 3, 116, 160	dveq0 25509	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)}))
162	161	fveq1d 6891	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵))
163		oveq2 7414	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
164		itgeq1 25282	. . . . . . . . 9 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
165	163, 164	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
166		fveq2 6889	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
167	165, 166	oveq12d 7424	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
168		eqid 2733	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))
169		ovex 7439	. . . . . . 7 ⊢ (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V
170	167, 168, 169	fvmpt 6996	. . . . . 6 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
171	7, 170	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
172	162, 171	eqtr3d 2775	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
173		lbicc2 13438	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
174	2, 4, 5, 173	syl3anc 1372	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
175		oveq2 7414	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
176		iooid 13349	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐴) = ∅
177	175, 176	eqtrdi 2789	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
178		itgeq1 25282	. . . . . . . . . 10 ⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
179	177, 178	syl 17	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
180		itg0 25289	. . . . . . . . 9 ⊢ ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
181	179, 180	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
182		fveq2 6889	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
183	181, 182	oveq12d 7424	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴)))
184		df-neg 11444	. . . . . . 7 ⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴))
185	183, 184	eqtr4di 2791	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴))
186		negex 11455	. . . . . 6 ⊢ -(𝐹‘𝐴) ∈ V
187	185, 168, 186	fvmpt 6996	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
188	174, 187	syl 17	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
189	10, 172, 188	3eqtr3d 2781	. . 3 ⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴))
190	189	oveq2d 7422	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴)))
191	113, 7	ffvelcdmd 7085	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
192		fvexd 6904	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
193	192, 55	itgcl 25293	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
194	191, 193	pncan3d 11571	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
195	113, 174	ffvelcdmd 7085	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
196	191, 195	negsubd 11574	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
197	190, 194, 196	3eqtr3d 2781	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 Vcvv 3475 ⦋csb 3893 ⊆ wss 3948 ∅c0 4322 ifcif 4528 𝒫 cpw 4602 {csn 4628 {cpr 4630 ⟨cop 4634 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 dom cdm 5676 ran crn 5677 ↾ cres 5678 “ cima 5679 Fun wfun 6535 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 1^st c1st 7970 2^nd c2nd 7971 ℂcc 11105 ℝcr 11106 0cc0 11107 + caddc 11110 · cmul 11112 ℝ^*cxr 11244 ≤ cle 11246 − cmin 11441 -cneg 11442 (,)cioo 13321 [,]cicc 13324 ∗ccj 15040 abscabs 15178 TopOpenctopn 17364 topGenctg 17380 ℂ_fldccnfld 20937 intcnt 22513 Cn ccn 22720 ×_t ctx 23056 –cn→ccncf 24384 volcvol 24972 MblFncmbf 25123 ∫₂citg2 25125 𝐿¹cibl 25126 ∫citg 25127 D cdv 25372

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-symdif 4242 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-disj 5114 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-ofr 7668 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-oadd 8467 df-omul 8468 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-dju 9893 df-card 9931 df-acn 9934 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-hash 14288 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-clim 15429 df-rlim 15430 df-sum 15630 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-cmp 22883 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-ovol 24973 df-vol 24974 df-mbf 25128 df-itg1 25129 df-itg2 25130 df-ibl 25131 df-itg 25132 df-0p 25179 df-limc 25375 df-dv 25376

This theorem is referenced by: areacirc 36570

W3C validator