Theorem ftc1a 23521

Description: The Fundamental Theorem of Calculus, part one. The function 𝐺 formed by varying the right endpoint of an integral of 𝐹 is continuous if 𝐹 is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.)

Hypotheses

Ref	Expression
ftc1.g	⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
ftc1.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc1.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc1.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc1.s	⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1.d	⊢ (𝜑 → 𝐷 ⊆ ℝ)
ftc1.i	⊢ (𝜑 → 𝐹 ∈ 𝐿1)
ftc1a.f	⊢ (𝜑 → 𝐹:𝐷⟶ℂ)

Assertion

Ref	Expression
ftc1a	⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

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

Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1a

Dummy variables 𝑠 𝑢 𝑤 𝑦 𝑧 𝑟 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ftc1.g	. . 3 ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
2		ftc1.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ftc1.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ftc1.le	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
5		ftc1.s	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
6		ftc1.d	. . 3 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
7		ftc1.i	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
8		ftc1a.f	. . 3 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
9	1, 2, 3, 4, 5, 6, 7, 8	ftc1lem2 23520	. 2 ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
10		fvex 6098	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
11	10	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑤 ∈ 𝐷) → (𝐹‘𝑤) ∈ V)
12	8	feqmptd 6144	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)))
13	12, 7	eqeltrrd 2688	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈ 𝐿1)
14	13	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈ 𝐿1)
15		simpr 475	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ+)
16	11, 14, 15	itgcn 23332	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒))
17		oveq12 6536	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (𝑠 − 𝑟) = (𝑧 − 𝑦))
18	17	fveq2d 6092	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑧 − 𝑦)))
19	18	breq1d 4587	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑑))
20		fveq2 6088	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧))
21		fveq2 6088	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦))
22	20, 21	oveqan12d 6546	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑧) − (𝐺‘𝑦)))
23	22	fveq2d 6092	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))))
24	23	breq1d 4587	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
25	19, 24	imbi12d 332	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))
26	25	ancoms 467	. . . . . . . . . . 11 ⊢ ((𝑟 = 𝑦 ∧ 𝑠 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))
27		oveq12 6536	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (𝑠 − 𝑟) = (𝑦 − 𝑧))
28	27	fveq2d 6092	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑦 − 𝑧)))
29	28	breq1d 4587	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑))
30		fveq2 6088	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑦 → (𝐺‘𝑠) = (𝐺‘𝑦))
31		fveq2 6088	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑧 → (𝐺‘𝑟) = (𝐺‘𝑧))
32	30, 31	oveqan12d 6546	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑦) − (𝐺‘𝑧)))
33	32	fveq2d 6092	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))))
34	33	breq1d 4587	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))
35	29, 34	imbi12d 332	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)))
36	35	ancoms 467	. . . . . . . . . . 11 ⊢ ((𝑟 = 𝑧 ∧ 𝑠 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)))
37		iccssre 12082	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
38	2, 3, 37	syl2anc 690	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
39	38	ad2antrr 757	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → (𝐴[,]𝐵) ⊆ ℝ)
40	38	ad3antrrr 761	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐴[,]𝐵) ⊆ ℝ)
41		simprr 791	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ (𝐴[,]𝐵))
42	40, 41	sseldd 3568	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℝ)
43	42	recnd 9924	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℂ)
44		simprl 789	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ (𝐴[,]𝐵))
45	40, 44	sseldd 3568	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ)
46	45	recnd 9924	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ)
47	43, 46	abssubd 13986	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧)))
48	47	breq1d 4587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑))
49	9	ad3antrrr 761	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
50	49, 41	ffvelrnd 6253	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑧) ∈ ℂ)
51	49, 44	ffvelrnd 6253	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑦) ∈ ℂ)
52	50, 51	abssubd 13986	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))))
53	52	breq1d 4587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))
54	48, 53	imbi12d 332	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)))
55		simpr3 1061	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧)
56	2	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ ℝ)
57	3	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ)
58	4	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ≤ 𝐵)
59	5	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → (𝐴(,)𝐵) ⊆ 𝐷)
60	6	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐷 ⊆ ℝ)
61	7	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹 ∈ 𝐿1)
62	8	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹:𝐷⟶ℂ)
63		simpr1 1059	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ (𝐴[,]𝐵))
64		simpr2 1060	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ (𝐴[,]𝐵))
65	1, 56, 57, 58, 59, 60, 61, 62, 63, 64	ftc1lem1 23519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝑧) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)
66	55, 65	mpdan 698	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)
67	66	adantlr 746	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)
68	67	ad2ant2r 778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)
69	68	fveq2d 6092	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡))
70		fvex 6098	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑡) ∈ V
71	70	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ V)
72	2	ad3antrrr 761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈ ℝ)
73	72	rexrd 9945	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈ ℝ*)
74		simprl1 1098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ (𝐴[,]𝐵))
75	3	ad3antrrr 761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈ ℝ)
76		elicc2 12065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
77	72, 75, 76	syl2anc 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
78	74, 77	mpbid 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))
79	78	simp2d 1066	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ≤ 𝑦)
80		iooss1 12037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑦) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧))
81	73, 79, 80	syl2anc 690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧))
82	75	rexrd 9945	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈ ℝ*)
83		simprl2 1099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ (𝐴[,]𝐵))
84		elicc2 12065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
85	72, 75, 84	syl2anc 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
86	83, 85	mpbid 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))
87	86	simp3d 1067	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ≤ 𝐵)
88		iooss2 12038	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
89	82, 87, 88	syl2anc 690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
90	81, 89	sstrd 3577	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝐵))
91	5	ad3antrrr 761	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝐵) ⊆ 𝐷)
92	90, 91	sstrd 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ 𝐷)
93		ioombl 23057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦(,)𝑧) ∈ dom vol
94	93	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ∈ dom vol)
95	70	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V)
96	8	feqmptd 6144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
97	96, 7	eqeltrrd 2688	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
98	97	ad3antrrr 761	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
99	92, 94, 95, 98	iblss 23294	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
100	71, 99	itgcl 23273	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡 ∈ ℂ)
101	100	abscld 13969	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ∈ ℝ)
102		iblmbf 23257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ 𝐿1 → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn)
103	99, 102	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn)
104	103, 71	mbfmptcl 23127	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ ℂ)
105	104	abscld 13969	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (abs‘(𝐹‘𝑡)) ∈ ℝ)
106	71, 99	iblabs 23318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (abs‘(𝐹‘𝑡))) ∈ 𝐿1)
107	105, 106	itgrecl 23287	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 ∈ ℝ)
108		simprl 789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) → 𝑒 ∈ ℝ+)
109	108	ad2antrr 757	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ+)
110	109	rpred 11704	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ)
111	71, 99	itgabs 23324	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ≤ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡)
112		simplr 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒))
113		mblvol 23022	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦(,)𝑧) ∈ dom vol → (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧)))
114	93, 113	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧))
115		ioossre 12062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦(,)𝑧) ⊆ ℝ
116		ovolcl 22970	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦(,)𝑧) ⊆ ℝ → (vol*‘(𝑦(,)𝑧)) ∈ ℝ*)
117	115, 116	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ∈ ℝ*)
118	86	simp1d 1065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ ℝ)
119	78	simp1d 1065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ ℝ)
120	118, 119	resubcld 10309	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈ ℝ)
121	120	rexrd 9945	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈ ℝ*)
122		simprr 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) → 𝑑 ∈ ℝ+)
123	122	ad2antrr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ+)
124	123	rpxrd 11705	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ*)
125		ioossicc 12086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦(,)𝑧) ⊆ (𝑦[,]𝑧)
126		iccssre 12082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ)
127	119, 118, 126	syl2anc 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦[,]𝑧) ⊆ ℝ)
128		ovolss 22977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) ∧ (𝑦[,]𝑧) ⊆ ℝ) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧)))
129	125, 127, 128	sylancr 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧)))
130		simprl3 1100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ≤ 𝑧)
131		ovolicc 23015	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦))
132	119, 118, 130, 131	syl3anc 1317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦))
133	129, 132	breqtrd 4603	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (𝑧 − 𝑦))
134	119, 118, 130	abssubge0d 13964	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦))
135		simprr 791	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) < 𝑑)
136	134, 135	eqbrtrrd 4601	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) < 𝑑)
137	117, 121, 124, 133, 136	xrlelttrd 11826	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) < 𝑑)
138	114, 137	syl5eqbr 4612	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol‘(𝑦(,)𝑧)) < 𝑑)
139	92, 138	jca 552	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑))
140		sseq1 3588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = (𝑦(,)𝑧) → (𝑢 ⊆ 𝐷 ↔ (𝑦(,)𝑧) ⊆ 𝐷))
141		fveq2 6088	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = (𝑦(,)𝑧) → (vol‘𝑢) = (vol‘(𝑦(,)𝑧)))
142	141	breq1d 4587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = (𝑦(,)𝑧) → ((vol‘𝑢) < 𝑑 ↔ (vol‘(𝑦(,)𝑧)) < 𝑑))
143	140, 142	anbi12d 742	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑦(,)𝑧) → ((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) ↔ ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑)))
144		fveq2 6088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑡 → (𝐹‘𝑤) = (𝐹‘𝑡))
145	144	fveq2d 6092	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑡 → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘𝑡)))
146	145	cbvitgv 23266	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡
147		itgeq1 23262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡)
148	146, 147	syl5eq 2655	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡)
149	148	breq1d 4587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑦(,)𝑧) → (∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒 ↔ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))
150	143, 149	imbi12d 332	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑦(,)𝑧) → (((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) ↔ (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)))
151	150	rspcv 3277	. . . . . . . . . . . . . . 15 ⊢ ((𝑦(,)𝑧) ∈ dom vol → (∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)))
152	94, 112, 139, 151	syl3c 63	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)
153	101, 107, 110, 111, 152	lelttrd 10046	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) < 𝑒)
154	69, 153	eqbrtrd 4599	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)
155	154	expr 640	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
156	26, 36, 39, 54, 155	wlogle 10410	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
157	156	ralrimivva 2953	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
158	157	ex 448	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+)) → (∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))
159	158	anassrs 677	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))
160	159	reximdva 2999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))
161	16, 160	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
162		r19.12 3044	. . . . 5 ⊢ (∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
163	161, 162	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
164	163	ralrimiva 2948	. . 3 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
165		ralcom 3078	. . 3 ⊢ (∀𝑒 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
166	164, 165	sylib 206	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))
167		ax-resscn 9849	. . . 4 ⊢ ℝ ⊆ ℂ
168	38, 167	syl6ss 3579	. . 3 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
169		ssid 3586	. . 3 ⊢ ℂ ⊆ ℂ
170		elcncf2 22432	. . 3 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))))
171	168, 169, 170	sylancl 692	. 2 ⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))))
172	9, 166, 171	mpbir2and 958	1 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   ∧ w3a 1030   = wceq 1474   ∈ wcel 1976  ∀wral 2895  ∃wrex 2896  Vcvv 3172   ⊆ wss 3539   class class class wbr 4577   ↦ cmpt 4637  dom cdm 5028  ⟶wf 5786  ‘cfv 5790  (class class class)co 6527  ℂcc 9790  ℝcr 9791  ℝ^*cxr 9929   < clt 9930   ≤ cle 9931   − cmin 10117  ℝ⁺crp 11664  (,)cioo 12002  [,]cicc 12005  abscabs 13768  –cn→ccncf 22418  vol*covol 22955  volcvol 22956  MblFncmbf 23106  𝐿¹cibl 23109  ∫citg 23110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cc 9117  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-ofr 6773  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-omul 7429  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-acn 8628  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-hash 12935  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-clim 14013  df-rlim 14014  df-sum 14211  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cn 20783  df-cnp 20784  df-cmp 20942  df-tx 21117  df-hmeo 21310  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-ovol 22957  df-vol 22958  df-mbf 23111  df-itg1 23112  df-itg2 23113  df-ibl 23114  df-itg 23115  df-0p 23160

This theorem is referenced by:  ftc2  23528