Proof of Theorem volioc
Step | Hyp | Ref
| Expression |
1 | | vol0 43175 |
. . . 4
⊢
(vol‘∅) = 0 |
2 | | oveq2 7221 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴(,]𝐴) = (𝐴(,]𝐵)) |
3 | 2 | eqcomd 2743 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴(,]𝐵) = (𝐴(,]𝐴)) |
4 | | leid 10928 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴) |
5 | | rexr 10879 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
6 | | ioc0 12982 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → ((𝐴(,]𝐴) = ∅ ↔ 𝐴 ≤ 𝐴)) |
7 | 5, 5, 6 | syl2anc 587 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴(,]𝐴) = ∅ ↔ 𝐴 ≤ 𝐴)) |
8 | 4, 7 | mpbird 260 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴(,]𝐴) = ∅) |
9 | 3, 8 | sylan9eqr 2800 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → (𝐴(,]𝐵) = ∅) |
10 | 9 | fveq2d 6721 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → (vol‘(𝐴(,]𝐵)) = (vol‘∅)) |
11 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
12 | 11 | biimpi 219 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴) |
13 | 12 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐵 = 𝐴) |
14 | | recn 10819 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ∈ ℂ) |
16 | 13, 15 | eqeltrd 2838 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐵 ∈ ℂ) |
17 | 16, 13 | subeq0bd 11258 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → (𝐵 − 𝐴) = 0) |
18 | 1, 10, 17 | 3eqtr4a 2804 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) |
19 | 18 | 3ad2antl1 1187 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) |
20 | | simpl1 1193 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ ℝ) |
21 | | simpl2 1194 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ ℝ) |
22 | | simpl3 1195 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) |
23 | | eqcom 2744 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
24 | 23 | biimpi 219 |
. . . . . 6
⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵) |
25 | 24 | necon3bi 2967 |
. . . . 5
⊢ (¬
𝐴 = 𝐵 → 𝐵 ≠ 𝐴) |
26 | 25 | adantl 485 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 ≠ 𝐴) |
27 | 20, 21, 22, 26 | leneltd 10986 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐴 < 𝐵) |
28 | 5 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ*) |
29 | | rexr 10879 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
30 | 29 | 3ad2ant2 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ*) |
31 | | simp3 1140 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
32 | | ioounsn 13065 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) |
33 | 28, 30, 31, 32 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) |
34 | 33 | eqcomd 2743 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴(,]𝐵) = ((𝐴(,)𝐵) ∪ {𝐵})) |
35 | 34 | fveq2d 6721 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,]𝐵)) = (vol‘((𝐴(,)𝐵) ∪ {𝐵}))) |
36 | | ioombl 24462 |
. . . . . 6
⊢ (𝐴(,)𝐵) ∈ dom vol |
37 | 36 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol) |
38 | | snmbl 43179 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → {𝐵} ∈ dom
vol) |
39 | 38 | 3ad2ant2 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → {𝐵} ∈ dom vol) |
40 | | ubioo 12967 |
. . . . . . 7
⊢ ¬
𝐵 ∈ (𝐴(,)𝐵) |
41 | | disjsn 4627 |
. . . . . . 7
⊢ (((𝐴(,)𝐵) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (𝐴(,)𝐵)) |
42 | 40, 41 | mpbir 234 |
. . . . . 6
⊢ ((𝐴(,)𝐵) ∩ {𝐵}) = ∅ |
43 | 42 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∩ {𝐵}) = ∅) |
44 | | ioovolcl 24467 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
45 | 44 | 3adant3 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
46 | | volsn 43183 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ →
(vol‘{𝐵}) =
0) |
47 | | 0red 10836 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 0 ∈
ℝ) |
48 | 46, 47 | eqeltrd 2838 |
. . . . . 6
⊢ (𝐵 ∈ ℝ →
(vol‘{𝐵}) ∈
ℝ) |
49 | 48 | 3ad2ant2 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐵}) ∈ ℝ) |
50 | | volun 24442 |
. . . . 5
⊢ ((((𝐴(,)𝐵) ∈ dom vol ∧ {𝐵} ∈ dom vol ∧ ((𝐴(,)𝐵) ∩ {𝐵}) = ∅) ∧ ((vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ (vol‘{𝐵}) ∈ ℝ)) →
(vol‘((𝐴(,)𝐵) ∪ {𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐵}))) |
51 | 37, 39, 43, 45, 49, 50 | syl32anc 1380 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐵}))) |
52 | | simp1 1138 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
53 | | simp2 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
54 | 52, 53, 31 | ltled 10980 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
55 | | volioo 24466 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
56 | 52, 53, 54, 55 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
57 | 46 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐵}) = 0) |
58 | 56, 57 | oveq12d 7231 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐵})) = ((𝐵 − 𝐴) + 0)) |
59 | 53 | recnd 10861 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
60 | 14 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
61 | 59, 60 | subcld 11189 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℂ) |
62 | 61 | addid1d 11032 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐵 − 𝐴) + 0) = (𝐵 − 𝐴)) |
63 | 58, 62 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐵})) = (𝐵 − 𝐴)) |
64 | 35, 51, 63 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) |
65 | 20, 21, 27, 64 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 = 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) |
66 | 19, 65 | pm2.61dan 813 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) |