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 25200 |
. 2
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
10 | | fvexd 6789 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑤 ∈ 𝐷) → (𝐹‘𝑤) ∈ V) |
11 | 8 | feqmptd 6837 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤))) |
12 | 11, 7 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
13 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑤 ∈ 𝐷 ↦ (𝐹‘𝑤)) ∈
𝐿1) |
14 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
15 | 10, 13, 14 | itgcn 25009 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
16 | | oveq12 7284 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (𝑠 − 𝑟) = (𝑧 − 𝑦)) |
17 | 16 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑧 − 𝑦))) |
18 | 17 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑑)) |
19 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
20 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
21 | 19, 20 | oveqan12d 7294 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑧) − (𝐺‘𝑦))) |
22 | 21 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑧) − (𝐺‘𝑦)))) |
23 | 22 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
24 | 18, 23 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑧 ∧ 𝑟 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
25 | 24 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑦 ∧ 𝑠 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
26 | | oveq12 7284 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (𝑠 − 𝑟) = (𝑦 − 𝑧)) |
27 | 26 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘(𝑠 − 𝑟)) = (abs‘(𝑦 − 𝑧))) |
28 | 27 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘(𝑠 − 𝑟)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
29 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑦 → (𝐺‘𝑠) = (𝐺‘𝑦)) |
30 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑧 → (𝐺‘𝑟) = (𝐺‘𝑧)) |
31 | 29, 30 | oveqan12d 7294 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((𝐺‘𝑠) − (𝐺‘𝑟)) = ((𝐺‘𝑦) − (𝐺‘𝑧))) |
32 | 31 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
33 | 32 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → ((abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
34 | 28, 33 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑟 = 𝑧) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
35 | 34 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑧 ∧ 𝑠 = 𝑦) → (((abs‘(𝑠 − 𝑟)) < 𝑑 → (abs‘((𝐺‘𝑠) − (𝐺‘𝑟))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
36 | | iccssre 13161 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
37 | 2, 3, 36 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
38 | 37 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → (𝐴[,]𝐵) ⊆ ℝ) |
39 | 37 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐴[,]𝐵) ⊆ ℝ) |
40 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ (𝐴[,]𝐵)) |
41 | 39, 40 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℝ) |
42 | 41 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℂ) |
43 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ (𝐴[,]𝐵)) |
44 | 39, 43 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ) |
45 | 44 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ) |
46 | 42, 45 | abssubd 15165 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
47 | 46 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑦 − 𝑧)) < 𝑑)) |
48 | 9 | ad3antrrr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
49 | 48, 40 | ffvelrnd 6962 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑧) ∈ ℂ) |
50 | 48, 43 | ffvelrnd 6962 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺‘𝑦) ∈ ℂ) |
51 | 49, 50 | abssubd 15165 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑧)))) |
52 | 51 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒 ↔ (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒)) |
53 | 47, 52 | imbi12d 345 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑑 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑧))) < 𝑒))) |
54 | | simpr3 1195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧) |
55 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ ℝ) |
56 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ) |
57 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐴 ≤ 𝐵) |
58 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → (𝐴(,)𝐵) ⊆ 𝐷) |
59 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐷 ⊆ ℝ) |
60 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹 ∈
𝐿1) |
61 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝐹:𝐷⟶ℂ) |
62 | | simpr1 1193 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ (𝐴[,]𝐵)) |
63 | | simpr2 1194 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ (𝐴[,]𝐵)) |
64 | 1, 55, 56, 57, 58, 59, 60, 61, 62, 63 | ftc1lem1 25199 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝑧) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
65 | 54, 64 | mpdan 684 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
66 | 65 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
67 | 66 | ad2ant2r 744 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ((𝐺‘𝑧) − (𝐺‘𝑦)) = ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) |
68 | 67 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) = (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡)) |
69 | | fvexd 6789 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ V) |
70 | 2 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈ ℝ) |
71 | 70 | rexrd 11025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ∈
ℝ*) |
72 | | simprl1 1217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ (𝐴[,]𝐵)) |
73 | 3 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈ ℝ) |
74 | | elicc2 13144 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
75 | 70, 73, 74 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
76 | 72, 75 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
77 | 76 | simp2d 1142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐴 ≤ 𝑦) |
78 | | iooss1 13114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑦) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
79 | 71, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧)) |
80 | 73 | rexrd 11025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝐵 ∈
ℝ*) |
81 | | simprl2 1218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ (𝐴[,]𝐵)) |
82 | | elicc2 13144 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
83 | 70, 73, 82 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
84 | 81, 83 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
85 | 84 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ≤ 𝐵) |
86 | | iooss2 13115 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
87 | 80, 85, 86 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵)) |
88 | 79, 87 | sstrd 3931 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝐵)) |
89 | 5 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝐴(,)𝐵) ⊆ 𝐷) |
90 | 88, 89 | sstrd 3931 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ 𝐷) |
91 | | ioombl 24729 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦(,)𝑧) ∈ dom vol |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦(,)𝑧) ∈ dom vol) |
93 | | fvexd 6789 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V) |
94 | 8 | feqmptd 6837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
95 | 94, 7 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
96 | 95 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
97 | 90, 92, 93, 96 | iblss 24969 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
98 | 69, 97 | itgcl 24948 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
99 | 98 | abscld 15148 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ∈ ℝ) |
100 | | iblmbf 24932 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ 𝐿1 → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
101 | 97, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹‘𝑡)) ∈ MblFn) |
102 | 101, 69 | mbfmptcl 24800 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹‘𝑡) ∈ ℂ) |
103 | 102 | abscld 15148 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑒 ∈ ℝ+
∧ 𝑑 ∈
ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
104 | 69, 97 | iblabs 24993 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (abs‘(𝐹‘𝑡))) ∈
𝐿1) |
105 | 103, 104 | itgrecl 24962 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 ∈ ℝ) |
106 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑒 ∈
ℝ+) |
107 | 106 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ+) |
108 | 107 | rpred 12772 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑒 ∈ ℝ) |
109 | 69, 97 | itgabs 24999 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) ≤ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
110 | | mblvol 24694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦(,)𝑧) ∈ dom vol → (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧))) |
111 | 91, 110 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧)) |
112 | | ioossre 13140 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦(,)𝑧) ⊆ ℝ |
113 | | ovolcl 24642 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦(,)𝑧) ⊆ ℝ → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
114 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ∈
ℝ*) |
115 | 84 | simp1d 1141 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑧 ∈ ℝ) |
116 | 76 | simp1d 1141 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ∈ ℝ) |
117 | 115, 116 | resubcld 11403 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈ ℝ) |
118 | 117 | rexrd 11025 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) ∈
ℝ*) |
119 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ 𝑑 ∈
ℝ+) |
120 | 119 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ+) |
121 | 120 | rpxrd 12773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑑 ∈ ℝ*) |
122 | | ioossicc 13165 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) |
123 | | iccssre 13161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ) |
124 | 116, 115,
123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑦[,]𝑧) ⊆ ℝ) |
125 | | ovolss 24649 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) ∧ (𝑦[,]𝑧) ⊆ ℝ) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
126 | 122, 124,
125 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧))) |
127 | | simprl3 1219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → 𝑦 ≤ 𝑧) |
128 | | ovolicc 24687 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
129 | 116, 115,
127, 128 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
130 | 126, 129 | breqtrd 5100 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (𝑧 − 𝑦)) |
131 | 116, 115,
127 | abssubge0d 15143 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
132 | | simprr 770 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘(𝑧 − 𝑦)) < 𝑑) |
133 | 131, 132 | eqbrtrrd 5098 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (𝑧 − 𝑦) < 𝑑) |
134 | 114, 118,
121, 130, 133 | xrlelttrd 12894 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) < 𝑑) |
135 | 111, 134 | eqbrtrid 5109 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (vol‘(𝑦(,)𝑧)) < 𝑑) |
136 | | sseq1 3946 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → (𝑢 ⊆ 𝐷 ↔ (𝑦(,)𝑧) ⊆ 𝐷)) |
137 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → (vol‘𝑢) = (vol‘(𝑦(,)𝑧))) |
138 | 137 | breq1d 5084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ((vol‘𝑢) < 𝑑 ↔ (vol‘(𝑦(,)𝑧)) < 𝑑)) |
139 | 136, 138 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → ((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) ↔ ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑))) |
140 | | 2fveq3 6779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑡 → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘𝑡))) |
141 | 140 | cbvitgv 24941 |
. . . . . . . . . . . . . . . . . . 19
⊢
∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 |
142 | | itgeq1 24937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑡)) d𝑡 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
143 | 141, 142 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 = ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡) |
144 | 143 | breq1d 5084 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑦(,)𝑧) → (∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒 ↔ ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)) |
145 | 139, 144 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑦(,)𝑧) → (((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) ↔ (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒))) |
146 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) |
147 | 145, 146,
92 | rspcdva 3562 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒)) |
148 | 90, 135, 147 | mp2and 696 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹‘𝑡)) d𝑡 < 𝑒) |
149 | 99, 105, 108, 109, 148 | lelttrd 11133 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹‘𝑡) d𝑡) < 𝑒) |
150 | 68, 149 | eqbrtrd 5096 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧) ∧ (abs‘(𝑧 − 𝑦)) < 𝑑)) → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) |
151 | 150 | expr 457 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
152 | 25, 35, 38, 53, 151 | wlogle 11508 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
153 | 152 | ralrimivva 3123 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
∧ ∀𝑢 ∈ dom
vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒)) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
154 | 153 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+))
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
155 | 154 | anassrs 468 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+)
→ (∀𝑢 ∈
dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
156 | 155 | reximdva 3203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑑 ∈
ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹‘𝑤)) d𝑤 < 𝑒) → ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒))) |
157 | 15, 156 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
158 | | r19.12 3257 |
. . . . 5
⊢
(∃𝑑 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
159 | 157, 158 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
160 | 159 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
161 | | ralcom 3166 |
. . 3
⊢
(∀𝑒 ∈
ℝ+ ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+ ∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
162 | 160, 161 | sylib 217 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)) |
163 | | ax-resscn 10928 |
. . . 4
⊢ ℝ
⊆ ℂ |
164 | 37, 163 | sstrdi 3933 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
165 | | ssid 3943 |
. . 3
⊢ ℂ
⊆ ℂ |
166 | | elcncf2 24053 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝐺 ∈
((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
167 | 164, 165,
166 | sylancl 586 |
. 2
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐺‘𝑧) − (𝐺‘𝑦))) < 𝑒)))) |
168 | 9, 162, 167 | mpbir2and 710 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |