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 23844 |
. 2
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
10 | | fvexd 6241 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑤 ∈ 𝐷) → (𝐹‘𝑤) ∈ V) |
11 | 8 | feqmptd 6288 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤))) |
12 | 11, 7 | eqeltrrd 2731 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
14 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
15 | 10, 13, 14 | itgcn 23654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
16 | | oveq12 6699 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (𝑠 − 𝑟) = (𝑧 − 𝑦)) |
17 | 16 | fveq2d 6233 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑧 − 𝑦))) |
18 | 17 | breq1d 4695 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑑)) |
19 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
20 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
21 | 19, 20 | oveqan12d 6709 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑧) − (𝐺‘𝑦))) |
22 | 21 | fveq2d 6233 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑧) − (𝐺‘𝑦)))) |
23 | 22 | breq1d 4695 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
24 | 18, 23 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
25 | 24 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑦 ∧ 𝑠 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
26 | | oveq12 6699 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (𝑠 − 𝑟) = (𝑦 − 𝑧)) |
27 | 26 | fveq2d 6233 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑦 − 𝑧))) |
28 | 27 | breq1d 4695 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
29 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑦 → (𝐺‘𝑠) = (𝐺‘𝑦)) |
30 | | fveq2 6229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑧 → (𝐺‘𝑟) = (𝐺‘𝑧)) |
31 | 29, 30 | oveqan12d 6709 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑦) − (𝐺‘𝑧))) |
32 | 31 | fveq2d 6233 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
33 | 32 | breq1d 4695 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
34 | 28, 33 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
35 | 34 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑧 ∧ 𝑠 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
36 | | iccssre 12293 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
37 | 2, 3, 36 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
38 | 37 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → (𝐴[,]𝐵) ⊆ ℝ) |
39 | 37 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐴[,]𝐵) ⊆ ℝ) |
40 | | simprr 811 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ (𝐴[,]𝐵)) |
41 | 39, 40 | sseldd 3637 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℝ) |
42 | 41 | recnd 10106 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℂ) |
43 | | simprl 809 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ (𝐴[,]𝐵)) |
44 | 39, 43 | sseldd 3637 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ) |
45 | 44 | recnd 10106 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ) |
46 | 42, 45 | abssubd 14236 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
47 | 46 | breq1d 4695 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
48 | 9 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
49 | 48, 40 | ffvelrnd 6400 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑧) ∈ ℂ) |
50 | 48, 43 | ffvelrnd 6400 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑦) ∈ ℂ) |
51 | 49, 50 | abssubd 14236 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
52 | 51 | breq1d 4695 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
53 | 47, 52 | imbi12d 333 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
54 | | simpr3 1089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧) |
55 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ ℝ) |
56 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ) |
57 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ≤ 𝐵) |
58 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → (𝐴(,)𝐵) ⊆ 𝐷) |
59 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐷 ⊆ ℝ) |
60 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹 ∈
𝐿1) |
61 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹:𝐷⟶ℂ) |
62 | | simpr1 1087 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ (𝐴[,]𝐵)) |
63 | | simpr2 1088 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ (𝐴[,]𝐵)) |
64 | 1, 55, 56, 57, 58, 59, 60, 61, 62, 63 | ftc1lem1 23843 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝑧) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
65 | 54, 64 | mpdan 703 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
66 | 65 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
67 | 66 | ad2ant2r 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
68 | 67 | fveq2d 6233 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)) |
69 | | fvexd 6241 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ V) |
70 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈ ℝ) |
71 | 70 | rexrd 10127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈
ℝ*) |
72 | | simprl1 1126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ (𝐴[,]𝐵)) |
73 | 3 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈ ℝ) |
74 | | elicc2 12276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
75 | 70, 73, 74 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
76 | 72, 75 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
77 | 76 | simp2d 1094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ≤ 𝑦) |
78 | | iooss1 12248 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑦) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
79 | 71, 77, 78 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
80 | 73 | rexrd 10127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈
ℝ*) |
81 | | simprl2 1127 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ (𝐴[,]𝐵)) |
82 | | elicc2 12276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
83 | 70, 73, 82 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
84 | 81, 83 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
85 | 84 | simp3d 1095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ≤ 𝐵) |
86 | | iooss2 12249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
87 | 80, 85, 86 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
88 | 79, 87 | sstrd 3646 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝐵)) |
89 | 5 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝐵) ⊆ 𝐷) |
90 | 88, 89 | sstrd 3646 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ 𝐷) |
91 | | ioombl 23379 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦(,)𝑧) ∈ dom vol |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ∈ dom vol) |
93 | | fvexd 6241 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V) |
94 | 8 | feqmptd 6288 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
95 | 94, 7 | eqeltrrd 2731 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
96 | 95 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
97 | 90, 92, 93, 96 | iblss 23616 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
98 | 69, 97 | itgcl 23595 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
99 | 98 | abscld 14219 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ∈ ℝ) |
100 | | iblmbf 23579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ 𝐿1 → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
101 | 97, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
102 | 101, 69 | mbfmptcl 23449 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ ℂ) |
103 | 102 | abscld 14219 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
104 | 69, 97 | iblabs 23640 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (abs‘(𝐹‘𝑡))) ∈
𝐿1) |
105 | 103, 104 | itgrecl 23609 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 ∈ ℝ) |
106 | | simprl 809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑒 ∈
ℝ+) |
107 | 106 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ+) |
108 | 107 | rpred 11910 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ) |
109 | 69, 97 | itgabs 23646 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ≤ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
110 | | simplr 807 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
111 | | mblvol 23344 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦(,)𝑧) ∈ dom vol → (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧))) |
112 | 91, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧)) |
113 | | ioossre 12273 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦(,)𝑧) ⊆ ℝ |
114 | | ovolcl 23292 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦(,)𝑧) ⊆ ℝ → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
115 | 113, 114 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
116 | 84 | simp1d 1093 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ ℝ) |
117 | 76 | simp1d 1093 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ ℝ) |
118 | 116, 117 | resubcld 10496 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈ ℝ) |
119 | 118 | rexrd 10127 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈
ℝ*) |
120 | | simprr 811 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑑 ∈
ℝ+) |
121 | 120 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ+) |
122 | 121 | rpxrd 11911 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ*) |
123 | | ioossicc 12297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) |
124 | | iccssre 12293 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ) |
125 | 117, 116,
124 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦[,]𝑧) ⊆ ℝ) |
126 | | ovolss 23299 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) ∧ (𝑦[,]𝑧) ⊆ ℝ) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
127 | 123, 125,
126 | sylancr 696 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
128 | | simprl3 1128 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ≤ 𝑧) |
129 | | ovolicc 23337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
130 | 117, 116,
128, 129 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
131 | 127, 130 | breqtrd 4711 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (𝑧 − 𝑦)) |
132 | 117, 116,
128 | abssubge0d 14214 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
133 | | simprr 811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) < 𝑑) |
134 | 132, 133 | eqbrtrrd 4709 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) < 𝑑) |
135 | 115, 119,
122, 131, 134 | xrlelttrd 12029 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) < 𝑑) |
136 | 112, 135 | syl5eqbr 4720 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol‘(𝑦(,)𝑧)) < 𝑑) |
137 | 90, 136 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑)) |
138 | | sseq1 3659 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → (𝑢 ⊆ 𝐷 ↔ (𝑦(,)𝑧) ⊆ 𝐷)) |
139 | | fveq2 6229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → (vol‘𝑢) = (vol‘(𝑦(,)𝑧))) |
140 | 139 | breq1d 4695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ((vol‘𝑢) < 𝑑 ↔ (vol‘(𝑦(,)𝑧)) < 𝑑)) |
141 | 138, 140 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → ((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) ↔ ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑))) |
142 | | fveq2 6229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑡 → (𝐹‘𝑤) = (𝐹‘𝑡)) |
143 | 142 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑡 → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘𝑡))) |
144 | 143 | cbvitgv 23588 |
. . . . . . . . . . . . . . . . . . 19
⊢
∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 |
145 | | itgeq1 23584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
146 | 144, 145 | syl5eq 2697 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
147 | 146 | breq1d 4695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → (∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒 ↔ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)) |
148 | 141, 147 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑦(,)𝑧) → (((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) ↔ (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))) |
149 | 148 | rspcv 3336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦(,)𝑧) ∈ dom vol → (∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))) |
150 | 92, 110, 137, 149 | syl3c 66 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒) |
151 | 99, 105, 108, 109, 150 | lelttrd 10233 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) < 𝑒) |
152 | 68, 151 | eqbrtrd 4707 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) |
153 | 152 | expr 642 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
154 | 25, 35, 38, 53, 153 | wlogle 10599 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
155 | 154 | ralrimivva 3000 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
156 | 155 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
157 | 156 | anassrs 681 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
158 | 157 | reximdva 3046 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
159 | 15, 158 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
160 | | r19.12 3092 |
. . . . 5
⊢
(∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
161 | 159, 160 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
162 | 161 | ralrimiva 2995 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
163 | | ralcom 3127 |
. . 3
⊢
(∀𝑒 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
164 | 162, 163 | sylib 208 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
165 | | ax-resscn 10031 |
. . . 4
⊢ ℝ
⊆ ℂ |
166 | 37, 165 | syl6ss 3648 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
167 | | ssid 3657 |
. . 3
⊢ ℂ
⊆ ℂ |
168 | | elcncf2 22740 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝐺 ∈
((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
169 | 166, 167,
168 | sylancl 695 |
. 2
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
170 | 9, 164, 169 | mpbir2and 977 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |