Step | Hyp | Ref
| Expression |
1 | | simpll 785 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ dom
vol) |
2 | | iccmbl 23732 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol) |
3 | 2 | adantll 707 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol) |
4 | | inmbl 23708 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑥) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol) |
5 | 1, 3, 4 | syl2anc 581 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol) |
6 | | mblvol 23696 |
. . . . 5
⊢ ((𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥)))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥)))) |
8 | | inss2 4058 |
. . . . . 6
⊢ (𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥) |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥)) |
10 | | mblss 23697 |
. . . . . 6
⊢ ((𝐵[,]𝑥) ∈ dom vol → (𝐵[,]𝑥) ⊆ ℝ) |
11 | 3, 10 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ⊆ ℝ) |
12 | | mblvol 23696 |
. . . . . . 7
⊢ ((𝐵[,]𝑥) ∈ dom vol → (vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥))) |
13 | 3, 12 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥))) |
14 | | iccvolcl 23733 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) ∈
ℝ) |
15 | 14 | adantll 707 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) ∈
ℝ) |
16 | 13, 15 | eqeltrrd 2907 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol*‘(𝐵[,]𝑥)) ∈
ℝ) |
17 | | ovolsscl 23652 |
. . . . 5
⊢ (((𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥) ∧ (𝐵[,]𝑥) ⊆ ℝ ∧ (vol*‘(𝐵[,]𝑥)) ∈ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
18 | 9, 11, 16, 17 | syl3anc 1496 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
19 | 7, 18 | eqeltrd 2906 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
20 | | volcn.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥)))) |
21 | 19, 20 | fmptd 6633 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹:ℝ⟶ℝ) |
22 | | simprr 791 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ 𝑒 ∈
ℝ+) |
23 | | oveq12 6914 |
. . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑦) → (𝑣 − 𝑢) = (𝑧 − 𝑦)) |
24 | 23 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 − 𝑢) = (𝑧 − 𝑦)) |
25 | 24 | fveq2d 6437 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (abs‘(𝑣 − 𝑢)) = (abs‘(𝑧 − 𝑦))) |
26 | 25 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((abs‘(𝑣 − 𝑢)) < 𝑒 ↔ (abs‘(𝑧 − 𝑦)) < 𝑒)) |
27 | | fveq2 6433 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑧 → (𝐹‘𝑣) = (𝐹‘𝑧)) |
28 | | fveq2 6433 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑦 → (𝐹‘𝑢) = (𝐹‘𝑦)) |
29 | 27, 28 | oveqan12rd 6925 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝐹‘𝑣) − (𝐹‘𝑢)) = ((𝐹‘𝑧) − (𝐹‘𝑦))) |
30 | 29 | fveq2d 6437 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) = (abs‘((𝐹‘𝑧) − (𝐹‘𝑦)))) |
31 | 30 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒 ↔ (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
32 | 26, 31 | imbi12d 336 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (((abs‘(𝑣 − 𝑢)) < 𝑒 → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
33 | | oveq12 6914 |
. . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑦 ∧ 𝑢 = 𝑧) → (𝑣 − 𝑢) = (𝑦 − 𝑧)) |
34 | 33 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (𝑣 − 𝑢) = (𝑦 − 𝑧)) |
35 | 34 | fveq2d 6437 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (abs‘(𝑣 − 𝑢)) = (abs‘(𝑦 − 𝑧))) |
36 | 35 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((abs‘(𝑣 − 𝑢)) < 𝑒 ↔ (abs‘(𝑦 − 𝑧)) < 𝑒)) |
37 | | fveq2 6433 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦)) |
38 | | fveq2 6433 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → (𝐹‘𝑢) = (𝐹‘𝑧)) |
39 | 37, 38 | oveqan12rd 6925 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((𝐹‘𝑣) − (𝐹‘𝑢)) = ((𝐹‘𝑦) − (𝐹‘𝑧))) |
40 | 39 | fveq2d 6437 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
41 | 40 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒)) |
42 | 36, 41 | imbi12d 336 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (((abs‘(𝑣 − 𝑢)) < 𝑒 → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑒 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒))) |
43 | | ssidd 3849 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ ℝ ⊆ ℝ) |
44 | | recn 10342 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) |
45 | | recn 10342 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
46 | | abssub 14443 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
47 | 44, 45, 46 | syl2anr 592 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
48 | 47 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (abs‘(𝑧
− 𝑦)) =
(abs‘(𝑦 − 𝑧))) |
49 | 48 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘(𝑧
− 𝑦)) < 𝑒 ↔ (abs‘(𝑦 − 𝑧)) < 𝑒)) |
50 | 21 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ 𝐹:ℝ⟶ℝ) |
51 | | ffvelrn 6606 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶ℝ ∧
𝑦 ∈ ℝ) →
(𝐹‘𝑦) ∈ ℝ) |
52 | | ffvelrn 6606 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶ℝ ∧
𝑧 ∈ ℝ) →
(𝐹‘𝑧) ∈ ℝ) |
53 | 51, 52 | anim12dan 614 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑦 ∈ ℝ ∧
𝑧 ∈ ℝ)) →
((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ)) |
54 | 50, 53 | sylan 577 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ)) |
55 | | recn 10342 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) ∈ ℂ) |
56 | | recn 10342 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ ℝ → (𝐹‘𝑦) ∈ ℂ) |
57 | | abssub 14443 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
58 | 55, 56, 57 | syl2anr 592 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
59 | 54, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
60 | 59 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒)) |
61 | 49, 60 | imbi12d 336 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑒 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒))) |
62 | | simpr2 1256 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ ℝ) |
63 | | oveq2 6913 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝐵[,]𝑥) = (𝐵[,]𝑧)) |
64 | 63 | ineq2d 4041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑧))) |
65 | 64 | fveq2d 6437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
66 | | fvex 6446 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝐴 ∩
(𝐵[,]𝑧))) ∈ V |
67 | 65, 20, 66 | fvmpt 6529 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝐹‘𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
68 | 62, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
69 | | simplll 793 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ dom vol) |
70 | | simplr 787 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
71 | 70 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ) |
72 | | iccmbl 23732 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐵[,]𝑧) ∈ dom vol) |
73 | 71, 62, 72 | syl2anc 581 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑧) ∈ dom vol) |
74 | | inmbl 23708 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑧) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol) |
75 | 69, 73, 74 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol) |
76 | | mblvol 23696 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
78 | 68, 77 | eqtrd 2861 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
79 | | simpr1 1254 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ ℝ) |
80 | | oveq2 6913 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐵[,]𝑥) = (𝐵[,]𝑦)) |
81 | 80 | ineq2d 4041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑦))) |
82 | 81 | fveq2d 6437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
83 | | fvex 6446 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝐴 ∩
(𝐵[,]𝑦))) ∈ V |
84 | 82, 20, 83 | fvmpt 6529 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝐹‘𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
85 | 79, 84 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
86 | | simp1 1172 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → 𝑦 ∈ ℝ) |
87 | | iccmbl 23732 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐵[,]𝑦) ∈ dom vol) |
88 | 70, 86, 87 | syl2an 591 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ∈ dom vol) |
89 | | inmbl 23708 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑦) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol) |
90 | 69, 88, 89 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol) |
91 | | mblvol 23696 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
93 | 85, 92 | eqtrd 2861 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
94 | 78, 93 | oveq12d 6923 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦))))) |
95 | 50 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐹:ℝ⟶ℝ) |
96 | 95, 62 | ffvelrnd 6609 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) ∈ ℝ) |
97 | 78, 96 | eqeltrrd 2907 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ∈ ℝ) |
98 | 71 | leidd 10918 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐵 ≤ 𝐵) |
99 | | simpr3 1258 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧) |
100 | | iccss 12529 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝐵 ≤ 𝐵 ∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧)) |
101 | 71, 62, 98, 99, 100 | syl22anc 874 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧)) |
102 | | sslin 4063 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵[,]𝑦) ⊆ (𝐵[,]𝑧) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧))) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧))) |
104 | | mblss 23697 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) |
105 | 75, 104 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) |
106 | 103, 105 | sstrd 3837 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ) |
107 | | iccssre 12543 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ) |
108 | 79, 62, 107 | syl2anc 581 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑦[,]𝑧) ⊆ ℝ) |
109 | 106, 108 | unssd 4016 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ) |
110 | 95, 79 | ffvelrnd 6609 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) ∈ ℝ) |
111 | 93, 110 | eqeltrrd 2907 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ) |
112 | 62, 79 | resubcld 10782 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑧 − 𝑦) ∈ ℝ) |
113 | 111, 112 | readdcld 10386 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)) ∈ ℝ) |
114 | | ovolicc 23689 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
115 | 114 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
116 | 115, 112 | eqeltrd 2906 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝑦[,]𝑧)) ∈ ℝ) |
117 | | ovolun 23665 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ) ∧ ((𝑦[,]𝑧) ⊆ ℝ ∧ (vol*‘(𝑦[,]𝑧)) ∈ ℝ)) →
(vol*‘((𝐴 ∩
(𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧)))) |
118 | 106, 111,
108, 116, 117 | syl22anc 874 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧)))) |
119 | 115 | oveq2d 6921 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧))) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
120 | 118, 119 | breqtrd 4899 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
121 | | ovollecl 23649 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ ∧ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)) ∈ ℝ ∧ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ) |
122 | 109, 113,
120, 121 | syl3anc 1496 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ) |
123 | 71 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝐵 ∈ ℝ) |
124 | 62 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑧 ∈ ℝ) |
125 | 79 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ∈ ℝ) |
126 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝐵 ≤ 𝑦) |
127 | 99 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ≤ 𝑧) |
128 | | simp2 1173 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → 𝑧 ∈ ℝ) |
129 | | elicc2 12526 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
130 | 70, 128, 129 | syl2an 591 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
131 | 130 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
132 | 125, 126,
127, 131 | mpbir3and 1448 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ∈ (𝐵[,]𝑧)) |
133 | | iccsplit 12598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ∈ (𝐵[,]𝑧)) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
134 | 123, 124,
132, 133 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
135 | | eqimss 3882 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
137 | 79 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑦 ∈ ℝ) |
138 | 62 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑧 ∈ ℝ) |
139 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑦 ≤ 𝐵) |
140 | 138 | leidd 10918 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑧 ≤ 𝑧) |
141 | | iccss 12529 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ≤ 𝐵 ∧ 𝑧 ≤ 𝑧)) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧)) |
142 | 137, 138,
139, 140, 141 | syl22anc 874 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧)) |
143 | | ssun4 4006 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵[,]𝑧) ⊆ (𝑦[,]𝑧) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
145 | 71, 79, 136, 144 | lecasei 10462 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
146 | | sslin 4063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))) |
148 | | indi 4103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) = ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) |
149 | | inss2 4058 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧) |
150 | | unss2 4011 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) |
152 | 148, 151 | eqsstri 3860 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) |
153 | 147, 152 | syl6ss 3839 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) |
154 | | ovolss 23651 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ∧ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))) |
155 | 153, 109,
154 | syl2anc 581 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))) |
156 | 97, 122, 113, 155, 120 | letrd 10513 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
157 | 97, 111, 112 | lesubadd2d 10951 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧 − 𝑦) ↔ (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)))) |
158 | 156, 157 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧 − 𝑦)) |
159 | 94, 158 | eqbrtrd 4895 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦)) |
160 | 96, 110 | resubcld 10782 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) ∈ ℝ) |
161 | | simplr 787 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑒 ∈ ℝ+) |
162 | 161 | rpred 12156 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑒 ∈ ℝ) |
163 | | lelttr 10447 |
. . . . . . . . . . . 12
⊢ ((((𝐹‘𝑧) − (𝐹‘𝑦)) ∈ ℝ ∧ (𝑧 − 𝑦) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦) ∧ (𝑧 − 𝑦) < 𝑒) → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
164 | 160, 112,
162, 163 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦) ∧ (𝑧 − 𝑦) < 𝑒) → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
165 | 159, 164 | mpand 688 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝑧 − 𝑦) < 𝑒 → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
166 | | abssubge0 14444 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
167 | 166 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
168 | 167 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑒 ↔ (𝑧 − 𝑦) < 𝑒)) |
169 | | ovolss 23651 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧)) ∧ (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
170 | 103, 105,
169 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
171 | 170, 93, 78 | 3brtr4d 4905 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) ≤ (𝐹‘𝑧)) |
172 | 110, 96, 171 | abssubge0d 14547 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = ((𝐹‘𝑧) − (𝐹‘𝑦))) |
173 | 172 | breq1d 4883 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒 ↔ ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
174 | 165, 168,
173 | 3imtr4d 286 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
175 | 32, 42, 43, 61, 174 | wlogle 10885 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
176 | 175 | anassrs 461 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
177 | 176 | ralrimiva 3175 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ ℝ)
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
178 | 177 | anasss 460 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑒 ∈ ℝ+
∧ 𝑦 ∈ ℝ))
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
179 | 178 | ancom2s 642 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
180 | | breq2 4877 |
. . . . 5
⊢ (𝑑 = 𝑒 → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑒)) |
181 | 180 | rspceaimv 3534 |
. . . 4
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ ℝ
((abs‘(𝑧 −
𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
182 | 22, 179, 181 | syl2anc 581 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ ∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
183 | 182 | ralrimivva 3180 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) →
∀𝑦 ∈ ℝ
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ ℝ
((abs‘(𝑧 −
𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
184 | | ax-resscn 10309 |
. . 3
⊢ ℝ
⊆ ℂ |
185 | | elcncf2 23063 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)))) |
186 | 184, 184,
185 | mp2an 685 |
. 2
⊢ (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
187 | 21, 183, 186 | sylanbrc 580 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ)) |