Proof of Theorem voliooico
Step | Hyp | Ref
| Expression |
1 | | iftrue 4042 |
. . . . . 6
⊢ (𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
2 | 1 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
3 | | voliooico.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
5 | 4 | subidd 10259 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
6 | 5 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → 0 = (𝐵 − 𝐵)) |
7 | 6 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 0 = (𝐵 − 𝐵)) |
8 | | iffalse 4045 |
. . . . . . 7
⊢ (¬
𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
9 | 8 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
10 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝜑) |
11 | | voliooico.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
13 | 10, 3 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
14 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
16 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → ¬ 𝐴 < 𝐵) |
17 | 12, 13, 15, 16 | lenlteq 38521 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 = 𝐵) |
18 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
20 | 10, 17, 19 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
21 | 7, 9, 20 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
22 | 2, 21 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
23 | 22 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
24 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
25 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
26 | | volioo 38840 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
27 | 24, 25, 14, 26 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
28 | | volico 38876 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
29 | 11, 3, 28 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
30 | 29 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
31 | 23, 27, 30 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (vol‘(𝐴[,)𝐵))) |
32 | | simpl 472 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝜑) |
33 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → ¬ 𝐴 ≤ 𝐵) |
34 | 32, 3 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
35 | 32, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
36 | 34, 35 | ltnled 10063 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → (𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵)) |
37 | 33, 36 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐵 < 𝐴) |
38 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈ ℝ) |
39 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈ ℝ) |
40 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
41 | 38, 39, 40 | ltled 10064 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ≤ 𝐴) |
42 | 39 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈
ℝ*) |
43 | 38 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈
ℝ*) |
44 | | ioo0 12071 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
45 | 42, 43, 44 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
46 | 41, 45 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴(,)𝐵) = ∅) |
47 | | ico0 12092 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
48 | 42, 43, 47 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
49 | 41, 48 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,)𝐵) = ∅) |
50 | 46, 49 | eqtr4d 2647 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴(,)𝐵) = (𝐴[,)𝐵)) |
51 | 50 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (vol‘(𝐴(,)𝐵)) = (vol‘(𝐴[,)𝐵))) |
52 | 32, 37, 51 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (vol‘(𝐴[,)𝐵))) |
53 | 31, 52 | pm2.61dan 828 |
1
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (vol‘(𝐴[,)𝐵))) |