Proof of Theorem volico
Step | Hyp | Ref
| Expression |
1 | | rexr 10085 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
2 | 1 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈
ℝ*) |
3 | | rexr 10085 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
4 | 3 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈
ℝ*) |
5 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
6 | | snunioo1 39738 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) |
7 | 2, 4, 5, 6 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) |
8 | 7 | eqcomd 2628 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,)𝐵) = ((𝐴(,)𝐵) ∪ {𝐴})) |
9 | 8 | fveq2d 6195 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (vol‘((𝐴(,)𝐵) ∪ {𝐴}))) |
10 | | ioombl 23333 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol) |
12 | | snmbl 40179 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ dom
vol) |
13 | 12 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → {𝐴} ∈ dom vol) |
14 | | lbioo 12206 |
. . . . . . . 8
⊢ ¬
𝐴 ∈ (𝐴(,)𝐵) |
15 | | disjsn 4246 |
. . . . . . . 8
⊢ (((𝐴(,)𝐵) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝐵)) |
16 | 14, 15 | mpbir 221 |
. . . . . . 7
⊢ ((𝐴(,)𝐵) ∩ {𝐴}) = ∅ |
17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∩ {𝐴}) = ∅) |
18 | | ioovolcl 23338 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
19 | 18 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
20 | | volsn 40183 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(vol‘{𝐴}) =
0) |
21 | | 0red 10041 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 0 ∈
ℝ) |
22 | 20, 21 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(vol‘{𝐴}) ∈
ℝ) |
23 | 22 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐴}) ∈ ℝ) |
24 | | volun 23313 |
. . . . . 6
⊢ ((((𝐴(,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol ∧ ((𝐴(,)𝐵) ∩ {𝐴}) = ∅) ∧ ((vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ (vol‘{𝐴}) ∈ ℝ)) →
(vol‘((𝐴(,)𝐵) ∪ {𝐴})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴}))) |
25 | 11, 13, 17, 19, 23, 24 | syl32anc 1334 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴}))) |
26 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
27 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
28 | 26, 27, 5 | ltled 10185 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
29 | | volioo 23337 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
30 | 26, 27, 28, 29 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
31 | 20 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐴}) = 0) |
32 | 30, 31 | oveq12d 6668 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})) = ((𝐵 − 𝐴) + 0)) |
33 | 27 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
34 | | recn 10026 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
35 | 34 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
36 | 33, 35 | subcld 10392 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℂ) |
37 | 36 | addid1d 10236 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐵 − 𝐴) + 0) = (𝐵 − 𝐴)) |
38 | 32, 37 | eqtrd 2656 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})) = (𝐵 − 𝐴)) |
39 | 9, 25, 38 | 3eqtrd 2660 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴)) |
40 | 39 | 3expa 1265 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴)) |
41 | | iftrue 4092 |
. . . 4
⊢ (𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
42 | 41 | adantl 482 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
43 | 40, 42 | eqtr4d 2659 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
44 | | simpl 473 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
45 | | simpr 477 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → ¬ 𝐴 < 𝐵) |
46 | 44 | simprd 479 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
47 | 44 | simpld 475 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
48 | 46, 47 | lenltd 10183 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
49 | 45, 48 | mpbird 247 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → 𝐵 ≤ 𝐴) |
50 | | simpr 477 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐵 ≤ 𝐴) |
51 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐴 ∈
ℝ*) |
52 | 3 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐵 ∈
ℝ*) |
53 | | ico0 12221 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
54 | 51, 52, 53 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
55 | 50, 54 | mpbird 247 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (𝐴[,)𝐵) = ∅) |
56 | 55 | fveq2d 6195 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘(𝐴[,)𝐵)) = (vol‘∅)) |
57 | | vol0 40175 |
. . . . . 6
⊢
(vol‘∅) = 0 |
58 | 57 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘∅) =
0) |
59 | 56, 58 | eqtrd 2656 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘(𝐴[,)𝐵)) = 0) |
60 | 44, 49, 59 | syl2anc 693 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = 0) |
61 | | iffalse 4095 |
. . . 4
⊢ (¬
𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
62 | 61 | adantl 482 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
63 | 60, 62 | eqtr4d 2659 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬
𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
64 | 43, 63 | pm2.61dan 832 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |