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 23603 |
. 2
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
10 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘𝑤) ∈ V |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑤 ∈ 𝐷) → (𝐹‘𝑤) ∈ V) |
12 | 8 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤))) |
13 | 12, 7 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
15 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
16 | 11, 14, 15 | itgcn 23415 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
17 | | oveq12 6558 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (𝑠 − 𝑟) = (𝑧 − 𝑦)) |
18 | 17 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑧 − 𝑦))) |
19 | 18 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑑)) |
20 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
22 | 20, 21 | oveqan12d 6568 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑧) − (𝐺‘𝑦))) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑧) − (𝐺‘𝑦)))) |
24 | 23 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
25 | 19, 24 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
26 | 25 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑦 ∧ 𝑠 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
27 | | oveq12 6558 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (𝑠 − 𝑟) = (𝑦 − 𝑧)) |
28 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑦 − 𝑧))) |
29 | 28 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑦 → (𝐺‘𝑠) = (𝐺‘𝑦)) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑧 → (𝐺‘𝑟) = (𝐺‘𝑧)) |
32 | 30, 31 | oveqan12d 6568 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑦) − (𝐺‘𝑧))) |
33 | 32 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
34 | 33 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
35 | 29, 34 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
36 | 35 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑧 ∧ 𝑠 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
37 | | iccssre 12126 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
38 | 2, 3, 37 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → (𝐴[,]𝐵) ⊆ ℝ) |
40 | 38 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐴[,]𝐵) ⊆ ℝ) |
41 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ (𝐴[,]𝐵)) |
42 | 40, 41 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℝ) |
43 | 42 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℂ) |
44 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ (𝐴[,]𝐵)) |
45 | 40, 44 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ) |
46 | 45 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ) |
47 | 43, 46 | abssubd 14040 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
48 | 47 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
49 | 9 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
50 | 49, 41 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑧) ∈ ℂ) |
51 | 49, 44 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑦) ∈ ℂ) |
52 | 50, 51 | abssubd 14040 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
53 | 52 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
54 | 48, 53 | imbi12d 333 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
55 | | simpr3 1062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧) |
56 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ ℝ) |
57 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ) |
58 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ≤ 𝐵) |
59 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → (𝐴(,)𝐵) ⊆ 𝐷) |
60 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐷 ⊆ ℝ) |
61 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹 ∈
𝐿1) |
62 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹:𝐷⟶ℂ) |
63 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ (𝐴[,]𝐵)) |
64 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ (𝐴[,]𝐵)) |
65 | 1, 56, 57, 58, 59, 60, 61, 62, 63, 64 | ftc1lem1 23602 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝑧) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
66 | 55, 65 | mpdan 699 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
67 | 66 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
68 | 67 | ad2ant2r 779 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)) |
70 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑡) ∈ V |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ V) |
72 | 2 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈ ℝ) |
73 | 72 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈
ℝ*) |
74 | | simprl1 1099 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ (𝐴[,]𝐵)) |
75 | 3 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈ ℝ) |
76 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
77 | 72, 75, 76 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
78 | 74, 77 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
79 | 78 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ≤ 𝑦) |
80 | | iooss1 12081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑦) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
81 | 73, 79, 80 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
82 | 75 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈
ℝ*) |
83 | | simprl2 1100 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ (𝐴[,]𝐵)) |
84 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
85 | 72, 75, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
86 | 83, 85 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
87 | 86 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ≤ 𝐵) |
88 | | iooss2 12082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
89 | 82, 87, 88 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
90 | 81, 89 | sstrd 3578 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝐵)) |
91 | 5 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝐵) ⊆ 𝐷) |
92 | 90, 91 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ 𝐷) |
93 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . 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 6159 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
97 | 96, 7 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
98 | 97 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
99 | 92, 94, 95, 98 | iblss 23377 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
100 | 71, 99 | itgcl 23356 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
101 | 100 | abscld 14023 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ∈ ℝ) |
102 | | iblmbf 23340 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ 𝐿1 → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
104 | 103, 71 | mbfmptcl 23210 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ ℂ) |
105 | 104 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
106 | 71, 99 | iblabs 23401 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (abs‘(𝐹‘𝑡))) ∈
𝐿1) |
107 | 105, 106 | itgrecl 23370 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 ∈ ℝ) |
108 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑒 ∈
ℝ+) |
109 | 108 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ+) |
110 | 109 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ) |
111 | 71, 99 | itgabs 23407 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ≤ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
112 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
113 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦(,)𝑧) ∈ dom vol → (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧))) |
114 | 93, 113 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧)) |
115 | | ioossre 12106 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦(,)𝑧) ⊆ ℝ |
116 | | ovolcl 23053 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦(,)𝑧) ⊆ ℝ → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
117 | 115, 116 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
118 | 86 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ ℝ) |
119 | 78 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ ℝ) |
120 | 118, 119 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈ ℝ) |
121 | 120 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈
ℝ*) |
122 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑑 ∈
ℝ+) |
123 | 122 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ+) |
124 | 123 | rpxrd 11749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ*) |
125 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) |
126 | | iccssre 12126 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ) |
127 | 119, 118,
126 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦[,]𝑧) ⊆ ℝ) |
128 | | ovolss 23060 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) ∧ (𝑦[,]𝑧) ⊆ ℝ) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
129 | 125, 127,
128 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
130 | | simprl3 1101 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ≤ 𝑧) |
131 | | ovolicc 23098 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
132 | 119, 118,
130, 131 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
133 | 129, 132 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (𝑧 − 𝑦)) |
134 | 119, 118,
130 | abssubge0d 14018 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
135 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) < 𝑑) |
136 | 134, 135 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) < 𝑑) |
137 | 117, 121,
124, 133, 136 | xrlelttrd 11867 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) < 𝑑) |
138 | 114, 137 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol‘(𝑦(,)𝑧)) < 𝑑) |
139 | 92, 138 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑)) |
140 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → (𝑢 ⊆ 𝐷 ↔ (𝑦(,)𝑧) ⊆ 𝐷)) |
141 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → (vol‘𝑢) = (vol‘(𝑦(,)𝑧))) |
142 | 141 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ((vol‘𝑢) < 𝑑 ↔ (vol‘(𝑦(,)𝑧)) < 𝑑)) |
143 | 140, 142 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → ((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) ↔ ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑))) |
144 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑡 → (𝐹‘𝑤) = (𝐹‘𝑡)) |
145 | 144 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑡 → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘𝑡))) |
146 | 145 | cbvitgv 23349 |
. . . . . . . . . . . . . . . . . . 19
⊢
∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 |
147 | | itgeq1 23345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
148 | 146, 147 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
149 | 148 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → (∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒 ↔ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)) |
150 | 143, 149 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑦(,)𝑧) → (((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) ↔ (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))) |
151 | 150 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦(,)𝑧) ∈ dom vol → (∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))) |
152 | 94, 112, 139, 151 | syl3c 64 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒) |
153 | 101, 107,
110, 111, 152 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) < 𝑒) |
154 | 69, 153 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) |
155 | 154 | expr 641 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
156 | 26, 36, 39, 54, 155 | wlogle 10440 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
157 | 156 | ralrimivva 2954 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
158 | 157 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
159 | 158 | anassrs 678 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
160 | 159 | reximdva 3000 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
161 | 16, 160 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
162 | | r19.12 3045 |
. . . . 5
⊢
(∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
163 | 161, 162 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
164 | 163 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
165 | | ralcom 3079 |
. . 3
⊢
(∀𝑒 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
166 | 164, 165 | sylib 207 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
167 | | ax-resscn 9872 |
. . . 4
⊢ ℝ
⊆ ℂ |
168 | 38, 167 | syl6ss 3580 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
169 | | ssid 3587 |
. . 3
⊢ ℂ
⊆ ℂ |
170 | | elcncf2 22501 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝐺 ∈
((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
171 | 168, 169,
170 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
172 | 9, 166, 171 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |