Proof of Theorem voliccico
Step | Hyp | Ref
| Expression |
1 | | iftrue 4465 |
. . . . . 6
⊢ (𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
2 | 1 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
3 | | voliccico.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | recnd 11003 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
5 | 4 | subidd 11320 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
6 | 5 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → 0 = (𝐵 − 𝐵)) |
7 | 6 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 0 = (𝐵 − 𝐵)) |
8 | | iffalse 4468 |
. . . . . . 7
⊢ (¬
𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
9 | 8 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0) |
10 | | simpll 764 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝜑) |
11 | | voliccico.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
13 | 10, 3 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
14 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) |
15 | 14 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
16 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → ¬ 𝐴 < 𝐵) |
17 | 12, 13, 15, 16 | lenlteq 42903 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → 𝐴 = 𝐵) |
18 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
19 | 18 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
20 | 10, 17, 19 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → (𝐵 − 𝐴) = (𝐵 − 𝐵)) |
21 | 7, 9, 20 | 3eqtr4d 2788 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ ¬ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
22 | 2, 21 | pm2.61dan 810 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴)) |
23 | 22 | eqcomd 2744 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
24 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
25 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
26 | | volicc 43539 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) |
27 | 24, 25, 14, 26 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) |
28 | | volico 43524 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
29 | 11, 3, 28 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
30 | 29 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) |
31 | 23, 27, 30 | 3eqtr4d 2788 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴[,)𝐵))) |
32 | | simpl 483 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝜑) |
33 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → ¬ 𝐴 ≤ 𝐵) |
34 | 32, 3 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
35 | 32, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
36 | 34, 35 | ltnled 11122 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → (𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵)) |
37 | 33, 36 | mpbird 256 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → 𝐵 < 𝐴) |
38 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
39 | 11 | rexrd 11025 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
40 | 3 | rexrd 11025 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
41 | | icc0 13127 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
42 | 39, 40, 41 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
44 | 38, 43 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅) |
45 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈ ℝ) |
46 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈ ℝ) |
47 | 45, 46, 38 | ltled 11123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ≤ 𝐴) |
48 | 46 | rexrd 11025 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈
ℝ*) |
49 | 45 | rexrd 11025 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈
ℝ*) |
50 | | ico0 13125 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
51 | 48, 49, 50 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |
52 | 47, 51 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,)𝐵) = ∅) |
53 | 44, 52 | eqtr4d 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = (𝐴[,)𝐵)) |
54 | 53 | fveq2d 6778 |
. . 3
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴[,)𝐵))) |
55 | 32, 37, 54 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴[,)𝐵))) |
56 | 31, 55 | pm2.61dan 810 |
1
⊢ (𝜑 → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴[,)𝐵))) |