Theorem ftc2nc 33126

Description: Choice-free proof of ftc2 23711. (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 10033	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		ftc2nc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 10033	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		ftc2nc.le	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6		ubicc2 12231	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
7	2, 4, 5, 6	syl3anc 1323	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
8		fvex 6158	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V
9	8	fvconst2 6423	. . . . 5 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
10	7, 9	syl 17	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴))
11		eqid 2621	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
12	11	subcn 22577	. . . . . . . . 9 ⊢ − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
14		eqid 2621	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)
15		ssid 3603	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
17		ioossre 12177	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ ℝ
18	17	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
19		ftc2nc.i	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
20		ftc2nc.c	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
21		cncff 22604	. . . . . . . . . 10 ⊢ ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
22	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
23		ioof 12213	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
24		ffun 6005	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
25	23, 24	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun (,)
26		fvelima 6205	. . . . . . . . . . . 12 ⊢ ((Fun (,) ∧ 𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
27	25, 26	mpan 705	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠)
28		1st2nd2 7150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
29	28	fveq2d 6152	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
30		df-ov 6607	. . . . . . . . . . . . . . . 16 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = ((,)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
31	29, 30	syl6eqr 2673	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘𝑥) = ((1st ‘𝑥)(,)(2nd ‘𝑥)))
32	31	eqeq1d 2623	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
33	32	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 ↔ ((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠))
34	2, 4	jca 554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
35	34	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
36		xp1st 7143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (1st ‘𝑥) ∈ (𝐴[,]𝐵))
37		elicc1 12161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
38	2, 4, 37	syl2anc 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1st ‘𝑥) ∈ (𝐴[,]𝐵) ↔ ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵)))
39	38	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → ((1st ‘𝑥) ∈ ℝ* ∧ 𝐴 ≤ (1st ‘𝑥) ∧ (1st ‘𝑥) ≤ 𝐵))
40	39	simp2d 1072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (1st ‘𝑥) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (1st ‘𝑥))
41	36, 40	sylan2 491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → 𝐴 ≤ (1st ‘𝑥))
42		xp2nd 7144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → (2nd ‘𝑥) ∈ (𝐴[,]𝐵))
43		iccleub 12171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
44	43	3expa 1262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (2nd ‘𝑥) ∈ (𝐴[,]𝐵)) → (2nd ‘𝑥) ≤ 𝐵)
45	34, 42, 44	syl2an 494	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (2nd ‘𝑥) ≤ 𝐵)
46		ioossioo 12207	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ (1st ‘𝑥) ∧ (2nd ‘𝑥) ≤ 𝐵)) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
47	35, 41, 45, 46	syl12anc 1321	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵))
48	47	sselda 3583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 𝑡 ∈ (𝐴(,)𝐵))
49	22	ffvelrnda 6315	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
50	49	adantlr 750	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
51	48, 50	syldan 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ ℂ)
52		ioombl 23240	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol
53	52	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol)
54		fvex 6158	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℝ D 𝐹)‘𝑡) ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
56	22	feqmptd 6206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
57	56, 19	eqeltrrd 2699	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
58	57	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
59	47, 53, 55, 58	iblss 23477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
60		ax-resscn 9937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
61		ssid 3603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ⊆ ℂ
62		cncfss 22610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
63	60, 61, 62	mp2an 707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
64		abscncf 22612	. . . . . . . . . . . . . . . . . . . 20 ⊢ abs ∈ (ℂ–cn→ℝ)
65	63, 64	sselii 3580	. . . . . . . . . . . . . . . . . . 19 ⊢ abs ∈ (ℂ–cn→ℂ)
66	65	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → abs ∈ (ℂ–cn→ℂ))
67	56	reseq1d 5355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
68	67	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))))
69	47	resmptd 5411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
70	68, 69	eqtrd 2655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) = (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)))
71	20	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
72		rescncf 22608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ (𝐴(,)𝐵) → ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)))
73	47, 71, 72	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((ℝ D 𝐹) ↾ ((1st ‘𝑥)(,)(2nd ‘𝑥))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
74	70, 73	eqeltrrd 2699	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
75	66, 74	cncfmpt1f 22624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
76		cnmbf 23332	. . . . . . . . . . . . . . . . 17 ⊢ ((((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol ∧ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
77	52, 75, 76	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
78	51, 59	itgcl 23456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
79	78	cjcld 13870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ)
80		ioossre 12177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℝ
81	80, 60	sstri 3592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ
82		cncfmptc 22622	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ ∧ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
83	81, 61, 82	mp3an23 1413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ℂ → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
84	79, 83	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
85		nfcv 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑠((ℝ D 𝐹)‘𝑡)
86		nfcsb1v 3530	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)
87		csbeq1a 3523	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑠 → ((ℝ D 𝐹)‘𝑡) = ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
88	85, 86, 87	cbvmpt 4709	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((ℝ D 𝐹)‘𝑡)) = (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))
89	88, 74	syl5eqelr 2703	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡)) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
90	84, 89	mulcncf 23123	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ))
91		cnmbf 23332	. . . . . . . . . . . . . . . . 17 ⊢ ((((1st ‘𝑥)(,)(2nd ‘𝑥)) ∈ dom vol ∧ (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ (((1st ‘𝑥)(,)(2nd ‘𝑥))–cn→ℂ)) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
92	52, 90, 91	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑠 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ ((∗‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) · ⦋𝑠 / 𝑡⦌((ℝ D 𝐹)‘𝑡))) ∈ MblFn)
93	51, 59, 77, 92	itgabsnc 33111	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡)
94	51	abscld 14109	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → (abs‘((ℝ D 𝐹)‘𝑡)) ∈ ℝ)
95	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → ((ℝ D 𝐹)‘𝑡) ∈ V)
96	95, 59, 77	iblabsnc 33106	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↦ (abs‘((ℝ D 𝐹)‘𝑡))) ∈ 𝐿1)
97	51	absge0d 14117	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) ∧ 𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥))) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑡)))
98	94, 96, 97	itgposval 23468	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))(abs‘((ℝ D 𝐹)‘𝑡)) d𝑡 = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
99	93, 98	breqtrd 4639	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
100		itgeq1 23445	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡 = ∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡)
101	100	fveq2d 6152	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) = (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡))
102		eleq2 2687	. . . . . . . . . . . . . . . . . 18 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)) ↔ 𝑡 ∈ 𝑠))
103	102	ifbid 4080	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0) = if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))
104	103	mpteq2dv 4705	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))
105	104	fveq2d 6152	. . . . . . . . . . . . . . 15 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
106	101, 105	breq12d 4626	. . . . . . . . . . . . . 14 ⊢ (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → ((abs‘∫((1st ‘𝑥)(,)(2nd ‘𝑥))((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ((1st ‘𝑥)(,)(2nd ‘𝑥)), (abs‘((ℝ D 𝐹)‘𝑡)), 0))) ↔ (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
107	99, 106	syl5ibcom 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((1st ‘𝑥)(,)(2nd ‘𝑥)) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
108	33, 107	sylbid 230	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
109	108	rexlimdva 3024	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑥 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))((,)‘𝑥) = 𝑠 → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
110	27, 109	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → (abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0)))))
111	110	ralrimiv 2959	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠((ℝ D 𝐹)‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘((ℝ D 𝐹)‘𝑡)), 0))))
112	14, 1, 3, 5, 16, 18, 19, 22, 111	ftc1anc 33125	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
113		ftc2nc.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
114		cncff 22604	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
115	113, 114	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
116	115	feqmptd 6206	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
117	116, 113	eqeltrrd 2699	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
118	11, 13, 112, 117	cncfmpt2f 22625	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
119	60	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
120		iccssre 12197	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
121	1, 3, 120	syl2anc 692	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
122	54	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
123	3	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
124	123	rexrd 10033	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
125		elicc2 12180	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
126	1, 3, 125	syl2anc 692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
127	126	biimpa 501	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
128	127	simp3d 1073	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
129		iooss2 12153	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
130	124, 128, 129	syl2anc 692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
131		ioombl 23240	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝑥) ∈ dom vol
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
133	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
134	57	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
135	130, 132, 133, 134	iblss 23477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
136	122, 135	itgcl 23456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
137	115	ffvelrnda 6315	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
138	136, 137	subcld 10336	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ)
139	11	tgioo2 22514	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
140		iccntr 22532	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
141	1, 3, 140	syl2anc 692	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
142	119, 121, 138, 139, 11, 141	dvmptntr 23640	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))))
143		reelprrecn 9972	. . . . . . . . . . 11 ⊢ ℝ ∈ {ℝ, ℂ}
144	143	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
145		ioossicc 12201	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
146	145	sseli 3579	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
147	146, 136	sylan2 491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
148	22	ffvelrnda 6315	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
149	14, 1, 3, 5, 20, 19	ftc1cnnc 33116	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
150	119, 121, 136, 139, 11, 141	dvmptntr 23640	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
151	22	feqmptd 6206	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
152	149, 150, 151	3eqtr3d 2663	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
153	146, 137	sylan2 491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ)
154	116	oveq2d 6620	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))))
155	119, 121, 137, 139, 11, 141	dvmptntr 23640	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))))
156	154, 151, 155	3eqtr3rd 2664	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
157	144, 147, 148, 152, 153, 148, 156	dvmptsub 23636	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
158	148	subidd 10324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
159	158	mpteq2dva 4704	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
160	142, 157, 159	3eqtrd 2659	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
161		fconstmpt 5123	. . . . . . . 8 ⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
162	160, 161	syl6eqr 2673	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0}))
163	1, 3, 118, 162	dveq0 23667	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)}))
164	163	fveq1d 6150	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵))
165		oveq2 6612	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
166		itgeq1 23445	. . . . . . . . 9 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
167	165, 166	syl 17	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
168		fveq2 6148	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
169	167, 168	oveq12d 6622	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
170		eqid 2621	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))
171		ovex 6632	. . . . . . 7 ⊢ (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V
172	169, 170, 171	fvmpt 6239	. . . . . 6 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
173	7, 172	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
174	164, 173	eqtr3d 2657	. . . 4 ⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)))
175		lbicc2 12230	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
176	2, 4, 5, 175	syl3anc 1323	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
177		oveq2 6612	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
178		iooid 12145	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐴) = ∅
179	177, 178	syl6eq 2671	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
180		itgeq1 23445	. . . . . . . . . 10 ⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
181	179, 180	syl 17	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
182		itg0 23452	. . . . . . . . 9 ⊢ ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
183	181, 182	syl6eq 2671	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
184		fveq2 6148	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
185	183, 184	oveq12d 6622	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴)))
186		df-neg 10213	. . . . . . 7 ⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴))
187	185, 186	syl6eqr 2673	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴))
188		negex 10223	. . . . . 6 ⊢ -(𝐹‘𝐴) ∈ V
189	187, 170, 188	fvmpt 6239	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
190	176, 189	syl 17	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴))
191	10, 174, 190	3eqtr3d 2663	. . 3 ⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴))
192	191	oveq2d 6620	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴)))
193	115, 7	ffvelrnd 6316	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
194	54	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
195	194, 57	itgcl 23456	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
196	193, 195	pncan3d 10339	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
197	115, 176	ffvelrnd 6316	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
198	193, 197	negsubd 10342	. 2 ⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
199	192, 196, 198	3eqtr3d 2663	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∃wrex 2908  Vcvv 3186  ⦋csb 3514   ⊆ wss 3555  ∅c0 3891  ifcif 4058  𝒫 cpw 4130  {csn 4148  {cpr 4150  ⟨cop 4154   class class class wbr 4613   ↦ cmpt 4673   × cxp 5072  dom cdm 5074  ran crn 5075   ↾ cres 5076   “ cima 5077  Fun wfun 5841  ⟶wf 5843  ‘cfv 5847  (class class class)co 6604  1^st c1st 7111  2^nd c2nd 7112  ℂcc 9878  ℝcr 9879  0cc0 9880   + caddc 9883   · cmul 9885  ℝ^*cxr 10017   ≤ cle 10019   − cmin 10210  -cneg 10211  (,)cioo 12117  [,]cicc 12120  ∗ccj 13770  abscabs 13908  TopOpenctopn 16003  topGenctg 16019  ℂ_fldccnfld 19665  intcnt 20731   Cn ccn 20938   ×_t ctx 21273  –cn→ccncf 22587  volcvol 23139  MblFncmbf 23289  ∫₂citg2 23291  𝐿¹cibl 23292  ∫citg 23293   D cdv 23533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-ofr 6851  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-omul 7510  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-acn 8712  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-rlim 14154  df-sum 14351  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-haus 21029  df-cmp 21100  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295  df-itg2 23296  df-ibl 23297  df-itg 23298  df-0p 23343  df-limc 23536  df-dv 23537

This theorem is referenced by:  areacirc  33137