Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ dom
vol) |
2 | | iccmbl 23141 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol) |
3 | 2 | adantll 746 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol) |
4 | | inmbl 23117 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑥) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol) |
5 | 1, 3, 4 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol) |
6 | | mblvol 23105 |
. . . . 5
⊢ ((𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥)))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥)))) |
8 | | inss2 3796 |
. . . . . 6
⊢ (𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥) |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥)) |
10 | | mblss 23106 |
. . . . . 6
⊢ ((𝐵[,]𝑥) ∈ dom vol → (𝐵[,]𝑥) ⊆ ℝ) |
11 | 3, 10 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ⊆ ℝ) |
12 | | mblvol 23105 |
. . . . . . 7
⊢ ((𝐵[,]𝑥) ∈ dom vol → (vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥))) |
13 | 3, 12 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥))) |
14 | | iccvolcl 23142 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) ∈
ℝ) |
15 | 14 | adantll 746 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐵[,]𝑥)) ∈
ℝ) |
16 | 13, 15 | eqeltrrd 2689 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol*‘(𝐵[,]𝑥)) ∈
ℝ) |
17 | | ovolsscl 23061 |
. . . . 5
⊢ (((𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥) ∧ (𝐵[,]𝑥) ⊆ ℝ ∧ (vol*‘(𝐵[,]𝑥)) ∈ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
18 | 9, 11, 16, 17 | syl3anc 1318 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
19 | 7, 18 | eqeltrd 2688 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(vol‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ) |
20 | | volcn.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥)))) |
21 | 19, 20 | fmptd 6292 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹:ℝ⟶ℝ) |
22 | | simprr 792 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ 𝑒 ∈
ℝ+) |
23 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑦) → (𝑣 − 𝑢) = (𝑧 − 𝑦)) |
24 | 23 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 − 𝑢) = (𝑧 − 𝑦)) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (abs‘(𝑣 − 𝑢)) = (abs‘(𝑧 − 𝑦))) |
26 | 25 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((abs‘(𝑣 − 𝑢)) < 𝑒 ↔ (abs‘(𝑧 − 𝑦)) < 𝑒)) |
27 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑧 → (𝐹‘𝑣) = (𝐹‘𝑧)) |
28 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑦 → (𝐹‘𝑢) = (𝐹‘𝑦)) |
29 | 27, 28 | oveqan12rd 6569 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝐹‘𝑣) − (𝐹‘𝑢)) = ((𝐹‘𝑧) − (𝐹‘𝑦))) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) = (abs‘((𝐹‘𝑧) − (𝐹‘𝑦)))) |
31 | 30 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → ((abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒 ↔ (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
32 | 26, 31 | imbi12d 333 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑧) → (((abs‘(𝑣 − 𝑢)) < 𝑒 → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
33 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑣 = 𝑦 ∧ 𝑢 = 𝑧) → (𝑣 − 𝑢) = (𝑦 − 𝑧)) |
34 | 33 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (𝑣 − 𝑢) = (𝑦 − 𝑧)) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (abs‘(𝑣 − 𝑢)) = (abs‘(𝑦 − 𝑧))) |
36 | 35 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((abs‘(𝑣 − 𝑢)) < 𝑒 ↔ (abs‘(𝑦 − 𝑧)) < 𝑒)) |
37 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦)) |
38 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → (𝐹‘𝑢) = (𝐹‘𝑧)) |
39 | 37, 38 | oveqan12rd 6569 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((𝐹‘𝑣) − (𝐹‘𝑢)) = ((𝐹‘𝑦) − (𝐹‘𝑧))) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
41 | 40 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → ((abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒)) |
42 | 36, 41 | imbi12d 333 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑧 ∧ 𝑣 = 𝑦) → (((abs‘(𝑣 − 𝑢)) < 𝑒 → (abs‘((𝐹‘𝑣) − (𝐹‘𝑢))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑒 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒))) |
43 | | ssid 3587 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ ℝ ⊆ ℝ) |
45 | | recn 9905 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) |
46 | | recn 9905 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
47 | | abssub 13914 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
48 | 45, 46, 47 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
49 | 48 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (abs‘(𝑧
− 𝑦)) =
(abs‘(𝑦 − 𝑧))) |
50 | 49 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘(𝑧
− 𝑦)) < 𝑒 ↔ (abs‘(𝑦 − 𝑧)) < 𝑒)) |
51 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ 𝐹:ℝ⟶ℝ) |
52 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶ℝ ∧
𝑦 ∈ ℝ) →
(𝐹‘𝑦) ∈ ℝ) |
53 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶ℝ ∧
𝑧 ∈ ℝ) →
(𝐹‘𝑧) ∈ ℝ) |
54 | 52, 53 | anim12dan 878 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑦 ∈ ℝ ∧
𝑧 ∈ ℝ)) →
((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ)) |
55 | 51, 54 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ)) |
56 | | recn 9905 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) ∈ ℝ → (𝐹‘𝑧) ∈ ℂ) |
57 | | recn 9905 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ ℝ → (𝐹‘𝑦) ∈ ℂ) |
58 | | abssub 13914 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
59 | 56, 57, 58 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑧)))) |
61 | 60 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒)) |
62 | 50, 61 | imbi12d 333 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ (((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒) ↔ ((abs‘(𝑦 − 𝑧)) < 𝑒 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑧))) < 𝑒))) |
63 | | simpr2 1061 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑧 ∈ ℝ) |
64 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝐵[,]𝑥) = (𝐵[,]𝑧)) |
65 | 64 | ineq2d 3776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑧))) |
66 | 65 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
67 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝐴 ∩
(𝐵[,]𝑧))) ∈ V |
68 | 66, 20, 67 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝐹‘𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
69 | 63, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧)))) |
70 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐴 ∈ dom vol) |
71 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐵 ∈ ℝ) |
73 | | iccmbl 23141 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐵[,]𝑧) ∈ dom vol) |
74 | 72, 63, 73 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑧) ∈ dom vol) |
75 | | inmbl 23117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑧) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol) |
76 | 70, 74, 75 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol) |
77 | | mblvol 23105 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
79 | 69, 78 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
80 | | simpr1 1060 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑦 ∈ ℝ) |
81 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐵[,]𝑥) = (𝐵[,]𝑦)) |
82 | 81 | ineq2d 3776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑦))) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
84 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝐴 ∩
(𝐵[,]𝑦))) ∈ V |
85 | 83, 20, 84 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝐹‘𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
86 | 80, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦)))) |
87 | | simp1 1054 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → 𝑦 ∈ ℝ) |
88 | | iccmbl 23141 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐵[,]𝑦) ∈ dom vol) |
89 | 71, 87, 88 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ∈ dom vol) |
90 | | inmbl 23117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑦) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol) |
91 | 70, 89, 90 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol) |
92 | | mblvol 23105 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
94 | 86, 93 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) |
95 | 79, 94 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦))))) |
96 | 51 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐹:ℝ⟶ℝ) |
97 | 96, 63 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑧) ∈ ℝ) |
98 | 79, 97 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ∈ ℝ) |
99 | 72 | leidd 10473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝐵 ≤ 𝐵) |
100 | | simpr3 1062 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑦 ≤ 𝑧) |
101 | | iccss 12112 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝐵 ≤ 𝐵 ∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧)) |
102 | 72, 63, 99, 100, 101 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧)) |
103 | | sslin 3801 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵[,]𝑦) ⊆ (𝐵[,]𝑧) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧))) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧))) |
105 | | mblss 23106 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) |
106 | 76, 105 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) |
107 | 104, 106 | sstrd 3578 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ) |
108 | | iccssre 12126 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ) |
109 | 80, 63, 108 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑦[,]𝑧) ⊆ ℝ) |
110 | 107, 109 | unssd 3751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ) |
111 | 96, 80 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) ∈ ℝ) |
112 | 94, 111 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ) |
113 | 63, 80 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑧 − 𝑦) ∈ ℝ) |
114 | 112, 113 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)) ∈ ℝ) |
115 | | ovolicc 23098 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝑦[,]𝑧)) = (𝑧 − 𝑦)) |
117 | 116, 113 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝑦[,]𝑧)) ∈ ℝ) |
118 | | ovolun 23074 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ) ∧ ((𝑦[,]𝑧) ⊆ ℝ ∧ (vol*‘(𝑦[,]𝑧)) ∈ ℝ)) →
(vol*‘((𝐴 ∩
(𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧)))) |
119 | 107, 112,
109, 117, 118 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧)))) |
120 | 116 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧))) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
121 | 119, 120 | breqtrd 4609 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
122 | | ovollecl 23058 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ ∧ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)) ∈ ℝ ∧ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ) |
123 | 110, 114,
121, 122 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ) |
124 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝐵 ∈ ℝ) |
125 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑧 ∈ ℝ) |
126 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ∈ ℝ) |
127 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝐵 ≤ 𝑦) |
128 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ≤ 𝑧) |
129 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → 𝑧 ∈ ℝ) |
130 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
131 | 71, 129, 130 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
133 | 126, 127,
128, 132 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → 𝑦 ∈ (𝐵[,]𝑧)) |
134 | | iccsplit 12176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ∈ (𝐵[,]𝑧)) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
135 | 124, 125,
133, 134 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
136 | | eqimss 3620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝐵 ≤ 𝑦) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
138 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑦 ∈ ℝ) |
139 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑧 ∈ ℝ) |
140 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑦 ≤ 𝐵) |
141 | 139 | leidd 10473 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → 𝑧 ≤ 𝑧) |
142 | | iccss 12112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝑦 ≤ 𝐵 ∧ 𝑧 ≤ 𝑧)) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧)) |
143 | 138, 139,
140, 141, 142 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧)) |
144 | | ssun4 3741 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵[,]𝑧) ⊆ (𝑦[,]𝑧) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧)) ∧ 𝑦 ≤ 𝐵) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
146 | 72, 80, 137, 145 | lecasei 10022 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) |
147 | | sslin 3801 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))) |
149 | | indi 3832 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) = ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) |
150 | | inss2 3796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧) |
151 | | unss2 3746 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) |
153 | 149, 152 | eqsstri 3598 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) |
154 | 148, 153 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) |
155 | | ovolss 23060 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ∧ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))) |
156 | 154, 110,
155 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))) |
157 | 98, 123, 114, 156, 121 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦))) |
158 | 98, 112, 113 | lesubadd2d 10505 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧 − 𝑦) ↔ (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧 − 𝑦)))) |
159 | 157, 158 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧 − 𝑦)) |
160 | 95, 159 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦)) |
161 | 97, 111 | resubcld 10337 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝐹‘𝑧) − (𝐹‘𝑦)) ∈ ℝ) |
162 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑒 ∈ ℝ+) |
163 | 162 | rpred 11748 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → 𝑒 ∈ ℝ) |
164 | | lelttr 10007 |
. . . . . . . . . . . 12
⊢ ((((𝐹‘𝑧) − (𝐹‘𝑦)) ∈ ℝ ∧ (𝑧 − 𝑦) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦) ∧ (𝑧 − 𝑦) < 𝑒) → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
165 | 161, 113,
163, 164 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((((𝐹‘𝑧) − (𝐹‘𝑦)) ≤ (𝑧 − 𝑦) ∧ (𝑧 − 𝑦) < 𝑒) → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
166 | 160, 165 | mpand 707 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((𝑧 − 𝑦) < 𝑒 → ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
167 | | abssubge0 13915 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
168 | 167 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (abs‘(𝑧 − 𝑦)) = (𝑧 − 𝑦)) |
169 | 168 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑒 ↔ (𝑧 − 𝑦) < 𝑒)) |
170 | | ovolss 23060 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧)) ∧ (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
171 | 104, 106,
170 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧)))) |
172 | 171, 94, 79 | 3brtr4d 4615 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (𝐹‘𝑦) ≤ (𝐹‘𝑧)) |
173 | 111, 97, 172 | abssubge0d 14018 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) = ((𝐹‘𝑧) − (𝐹‘𝑦))) |
174 | 173 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒 ↔ ((𝐹‘𝑧) − (𝐹‘𝑦)) < 𝑒)) |
175 | 166, 169,
174 | 3imtr4d 282 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ
∧ 𝑦 ≤ 𝑧)) → ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
176 | 32, 42, 44, 62, 175 | wlogle 10440 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ (𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ))
→ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
177 | 176 | anassrs 678 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈ ℝ)
∧ 𝑒 ∈
ℝ+) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
178 | 177 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ ℝ)
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
179 | 178 | anasss 677 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑒 ∈ ℝ+
∧ 𝑦 ∈ ℝ))
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
180 | 179 | ancom2s 840 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
181 | | breq2 4587 |
. . . . . . 7
⊢ (𝑑 = 𝑒 → ((abs‘(𝑧 − 𝑦)) < 𝑑 ↔ (abs‘(𝑧 − 𝑦)) < 𝑒)) |
182 | 181 | imbi1d 330 |
. . . . . 6
⊢ (𝑑 = 𝑒 → (((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒) ↔ ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
183 | 182 | ralbidv 2969 |
. . . . 5
⊢ (𝑑 = 𝑒 → (∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒) ↔ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
184 | 183 | rspcev 3282 |
. . . 4
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑧 ∈
ℝ ((abs‘(𝑧
− 𝑦)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ ℝ
((abs‘(𝑧 −
𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
185 | 22, 180, 184 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+))
→ ∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
186 | 185 | ralrimivva 2954 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) →
∀𝑦 ∈ ℝ
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ ℝ
((abs‘(𝑧 −
𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)) |
187 | | ax-resscn 9872 |
. . 3
⊢ ℝ
⊆ ℂ |
188 | | elcncf2 22501 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒)))) |
189 | 187, 187,
188 | mp2an 704 |
. 2
⊢ (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ ℝ ((abs‘(𝑧 − 𝑦)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑦))) < 𝑒))) |
190 | 21, 186, 189 | sylanbrc 695 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ)) |