Proof of Theorem hoidmv1lelem2
Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem2.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | hoidmv1lelem2.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | hoidmv1lelem2.m |
. . . . . . . 8
⊢ 𝑀 = if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵)) |
5 | | hoidmv1lelem2.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷:ℕ⟶ℝ) |
6 | | hoidmv1lelem2.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℕ) |
7 | 5, 6 | ffvelrnd 6856 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐾) ∈ ℝ) |
8 | 7, 2 | ifcld 4457 |
. . . . . . 7
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ∈ ℝ) |
9 | 4, 8 | eqeltrd 2833 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
10 | | hoidmv1lelem2.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶:ℕ⟶ℝ) |
11 | 10, 6 | ffvelrnd 6856 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶‘𝐾) ∈ ℝ) |
12 | 7 | rexrd 10762 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝐾) ∈
ℝ*) |
13 | | icossre 12895 |
. . . . . . . . . 10
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ (𝐷‘𝐾) ∈ ℝ*) → ((𝐶‘𝐾)[,)(𝐷‘𝐾)) ⊆ ℝ) |
14 | 11, 12, 13 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶‘𝐾)[,)(𝐷‘𝐾)) ⊆ ℝ) |
15 | | hoidmv1lelem2.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ((𝐶‘𝐾)[,)(𝐷‘𝐾))) |
16 | 14, 15 | sseldd 3876 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
17 | | hoidmv1lelem2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ 𝑆) |
18 | 11 | rexrd 10762 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘𝐾) ∈
ℝ*) |
19 | | icoltub 42570 |
. . . . . . . . . . . 12
⊢ (((𝐶‘𝐾) ∈ ℝ* ∧ (𝐷‘𝐾) ∈ ℝ* ∧ 𝑆 ∈ ((𝐶‘𝐾)[,)(𝐷‘𝐾))) → 𝑆 < (𝐷‘𝐾)) |
20 | 18, 12, 15, 19 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < (𝐷‘𝐾)) |
21 | 16, 7, 20 | ltled 10859 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≤ (𝐷‘𝐾)) |
22 | | hoidmv1lelem2.l |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < 𝐵) |
23 | 16, 2, 22 | ltled 10859 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≤ 𝐵) |
24 | 21, 23 | jca 515 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ≤ (𝐷‘𝐾) ∧ 𝑆 ≤ 𝐵)) |
25 | | lemin 12661 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ (𝐷‘𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷‘𝐾) ∧ 𝑆 ≤ 𝐵))) |
26 | 16, 7, 2, 25 | syl3anc 1372 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ≤ if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷‘𝐾) ∧ 𝑆 ≤ 𝐵))) |
27 | 24, 26 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≤ if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵)) |
28 | 1, 16, 8, 17, 27 | letrd 10868 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵)) |
29 | 4 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) = 𝑀) |
30 | 28, 29 | breqtrd 5053 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝑀) |
31 | | min2 12659 |
. . . . . . . 8
⊢ (((𝐷‘𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ≤ 𝐵) |
32 | 7, 2, 31 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ≤ 𝐵) |
33 | 4, 32 | eqbrtrd 5049 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐵) |
34 | 1, 2, 9, 30, 33 | eliccd 42566 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵)) |
35 | 9 | recnd 10740 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℂ) |
36 | 16 | recnd 10740 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℂ) |
37 | 1 | recnd 10740 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
38 | 35, 36, 37 | npncand 11092 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 − 𝑆) + (𝑆 − 𝐴)) = (𝑀 − 𝐴)) |
39 | 38 | eqcomd 2744 |
. . . . . 6
⊢ (𝜑 → (𝑀 − 𝐴) = ((𝑀 − 𝑆) + (𝑆 − 𝐴))) |
40 | 9, 16 | resubcld 11139 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 − 𝑆) ∈ ℝ) |
41 | 16, 1 | resubcld 11139 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − 𝐴) ∈ ℝ) |
42 | 40, 41 | readdcld 10741 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 − 𝑆) + (𝑆 − 𝐴)) ∈ ℝ) |
43 | | nnex 11715 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ ∈
V) |
45 | | volf 24274 |
. . . . . . . . . . . . . . 15
⊢ vol:dom
vol⟶(0[,]+∞) |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
47 | 10 | ffvelrnda 6855 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ) |
48 | 5 | ffvelrnda 6855 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ) |
49 | 16 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
50 | 48, 49 | ifcld 4457 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ) |
51 | 50 | rexrd 10762 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈
ℝ*) |
52 | | icombl 24309 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
53 | 47, 51, 52 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
54 | 46, 53 | ffvelrnd 6856 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞)) |
55 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
56 | 54, 55 | fmptd 6882 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞)) |
57 | 44, 56 | sge0xrcl 43449 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈
ℝ*) |
58 | | pnfxr 10766 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → +∞ ∈
ℝ*) |
60 | | hoidmv1lelem2.r |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) |
61 | 60 | rexrd 10762 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈
ℝ*) |
62 | | nfv 1920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝜑 |
63 | 48 | rexrd 10762 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈
ℝ*) |
64 | | icombl 24309 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
65 | 47, 63, 64 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
66 | 46, 65 | ffvelrnd 6856 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞)) |
67 | 47 | rexrd 10762 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈
ℝ*) |
68 | 47 | leidd 11277 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
69 | | min1 12658 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗)) |
70 | 48, 49, 69 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗)) |
71 | | icossico 12884 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
72 | 67, 63, 68, 70, 71 | syl22anc 838 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
73 | | volss 24278 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
74 | 53, 65, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
75 | 62, 44, 54, 66, 74 | sge0lempt 43474 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
76 | 60 | ltpnfd 12592 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞) |
77 | 57, 61, 59, 75, 76 | xrlelttrd 12629 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞) |
78 | 57, 59, 77 | xrltned 42418 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞) |
79 | 78 | neneqd 2939 |
. . . . . . . . 9
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞) |
80 | 44, 56 | sge0repnf 43450 |
. . . . . . . . 9
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)) |
81 | 79, 80 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ) |
82 | 40, 81 | readdcld 10741 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) ∈ ℝ) |
83 | 9 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑀 ∈ ℝ) |
84 | 48, 83 | ifcld 4457 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈ ℝ) |
85 | 84 | rexrd 10762 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈
ℝ*) |
86 | | icombl 24309 |
. . . . . . . . . . . . . 14
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ∈ dom vol) |
87 | 47, 85, 86 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ∈ dom vol) |
88 | 46, 87 | ffvelrnd 6856 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) ∈ (0[,]+∞)) |
89 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) |
90 | 88, 89 | fmptd 6882 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))):ℕ⟶(0[,]+∞)) |
91 | 44, 90 | sge0xrcl 43449 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈
ℝ*) |
92 | | min1 12658 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ≤ (𝐷‘𝑗)) |
93 | 48, 83, 92 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ≤ (𝐷‘𝑗)) |
94 | | icossico 12884 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
95 | 67, 63, 68, 93, 94 | syl22anc 838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
96 | | volss 24278 |
. . . . . . . . . . . . 13
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
97 | 87, 65, 95, 96 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
98 | 62, 44, 88, 66, 97 | sge0lempt 43474 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
99 | 91, 61, 59, 98, 76 | xrlelttrd 12629 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) < +∞) |
100 | 91, 59, 99 | xrltned 42418 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ≠ +∞) |
101 | 100 | neneqd 2939 |
. . . . . . . 8
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) = +∞) |
102 | 44, 90 | sge0repnf 43450 |
. . . . . . . 8
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) = +∞)) |
103 | 101, 102 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℝ) |
104 | | hoidmv1lelem2.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
105 | | hoidmv1lelem2.u |
. . . . . . . . . . 11
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} |
106 | 104, 105 | eleqtrdi 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
107 | | oveq1 7171 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴)) |
108 | | simpl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ) → 𝑧 = 𝑆) |
109 | 108 | breq2d 5039 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆)) |
110 | 109, 108 | ifbieq2d 4437 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) |
111 | 110 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) |
112 | 111 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) |
113 | 112 | mpteq2dva 5122 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) |
114 | 113 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
115 | 107, 114 | breq12d 5040 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
116 | 115 | elrab 3585 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
117 | 106, 116 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
118 | 117 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
119 | 41, 81, 40, 118 | leadd2dd 11326 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 − 𝑆) + (𝑆 − 𝐴)) ≤ ((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
120 | | difssd 4021 |
. . . . . . . . . 10
⊢ (𝜑 → (ℕ ∖ {𝐾}) ⊆
ℕ) |
121 | 62, 44, 54, 81, 120 | sge0ssrempt 43469 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ) |
122 | | difexg 5192 |
. . . . . . . . . . . . . . 15
⊢ (ℕ
∈ V → (ℕ ∖ {𝐾}) ∈ V) |
123 | 43, 122 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (ℕ
∖ {𝐾}) ∈
V |
124 | 123 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℕ ∖ {𝐾}) ∈ V) |
125 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → vol:dom
vol⟶(0[,]+∞)) |
126 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → 𝜑) |
127 | | eldifi 4015 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ) |
128 | 127 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ) |
129 | 126, 128,
47 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶‘𝑗) ∈ ℝ) |
130 | 128, 85 | syldan 594 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈
ℝ*) |
131 | 129, 130,
86 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ∈ dom vol) |
132 | 125, 131 | ffvelrnd 6856 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) ∈ (0[,]+∞)) |
133 | 62, 124, 132 | sge0xrclmpt 43492 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈
ℝ*) |
134 | 44, 88, 120 | sge0lessmpt 43463 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
135 | 133, 91, 59, 134, 99 | xrlelttrd 12629 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) < +∞) |
136 | 133, 59, 135 | xrltned 42418 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ≠ +∞) |
137 | 136 | neneqd 2939 |
. . . . . . . . . 10
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) = +∞) |
138 | 62, 124, 132 | sge0repnfmpt 43503 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) = +∞)) |
139 | 137, 138 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℝ) |
140 | 9, 11 | resubcld 11139 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − (𝐶‘𝐾)) ∈ ℝ) |
141 | 128, 54 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞)) |
142 | 128, 53 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol) |
143 | 128, 67 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶‘𝑗) ∈
ℝ*) |
144 | 128, 68 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
145 | | iftrue 4417 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗)) |
146 | 145 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗)) |
147 | 48 | leidd 11277 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ≤ (𝐷‘𝑗)) |
148 | 147 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ≤ (𝐷‘𝑗)) |
149 | 48 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ∈ ℝ) |
150 | 83 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ) |
151 | 49 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ) |
152 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ≤ 𝑆) |
153 | 20, 22 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝐵)) |
154 | | ltmin 12663 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℝ ∧ (𝐷‘𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ↔ (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝐵))) |
155 | 16, 7, 2, 154 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ↔ (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝐵))) |
156 | 153, 155 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑆 < if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵)) |
157 | 156, 29 | breqtrd 5053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 < 𝑀) |
158 | 157 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 < 𝑀) |
159 | 149, 151,
150, 152, 158 | lelttrd 10869 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) < 𝑀) |
160 | 149, 150,
159 | ltled 10859 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ≤ 𝑀) |
161 | 148, 160 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → ((𝐷‘𝑗) ≤ (𝐷‘𝑗) ∧ (𝐷‘𝑗) ≤ 𝑀)) |
162 | | lemin 12661 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷‘𝑗) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ↔ ((𝐷‘𝑗) ≤ (𝐷‘𝑗) ∧ (𝐷‘𝑗) ≤ 𝑀))) |
163 | 149, 149,
150, 162 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → ((𝐷‘𝑗) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ↔ ((𝐷‘𝑗) ≤ (𝐷‘𝑗) ∧ (𝐷‘𝑗) ≤ 𝑀))) |
164 | 161, 163 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
165 | 146, 164 | eqbrtrd 5049 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
166 | | iffalse 4420 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆) |
167 | 166 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆) |
168 | 49 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ) |
169 | 84 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈ ℝ) |
170 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → ¬ (𝐷‘𝑗) ≤ 𝑆) |
171 | 48 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (𝐷‘𝑗) ∈ ℝ) |
172 | 168, 171 | ltnled 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (𝑆 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑆)) |
173 | 170, 172 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 < (𝐷‘𝑗)) |
174 | 157 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 < 𝑀) |
175 | 173, 174 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (𝑆 < (𝐷‘𝑗) ∧ 𝑆 < 𝑀)) |
176 | 83 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ) |
177 | | ltmin 12663 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ↔ (𝑆 < (𝐷‘𝑗) ∧ 𝑆 < 𝑀))) |
178 | 168, 171,
176, 177 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (𝑆 < if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ↔ (𝑆 < (𝐷‘𝑗) ∧ 𝑆 < 𝑀))) |
179 | 175, 178 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 < if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
180 | 168, 169,
179 | ltled 10859 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
181 | 167, 180 | eqbrtrd 5049 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
182 | 165, 181 | pm2.61dan 813 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
183 | 128, 182 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
184 | | icossico 12884 |
. . . . . . . . . . . 12
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) |
185 | 143, 130,
144, 183, 184 | syl22anc 838 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) |
186 | | volss 24278 |
. . . . . . . . . . 11
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) |
187 | 142, 131,
185, 186 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) |
188 | 62, 124, 141, 132, 187 | sge0lempt 43474 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
189 | 121, 139,
140, 188 | leadd2dd 11326 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
190 | | difsnid 4695 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → ((ℕ
∖ {𝐾}) ∪ {𝐾}) = ℕ) |
191 | 6, 190 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ) |
192 | 191 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ = ((ℕ
∖ {𝐾}) ∪ {𝐾})) |
193 | 192 | mpteq1d 5116 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) |
194 | 193 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) =
(Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) |
195 | | neldifsnd 4678 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾})) |
196 | | fveq2 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐾 → (𝐶‘𝑗) = (𝐶‘𝐾)) |
197 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝐾 → (𝐷‘𝑗) = (𝐷‘𝐾)) |
198 | 197 | breq1d 5037 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐾 → ((𝐷‘𝑗) ≤ 𝑆 ↔ (𝐷‘𝐾) ≤ 𝑆)) |
199 | 198, 197 | ifbieq1d 4435 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐾 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)) |
200 | 196, 199 | oveq12d 7182 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐾 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) = ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) |
201 | 200 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐾 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) = (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)))) |
202 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → vol:dom
vol⟶(0[,]+∞)) |
203 | 7, 16 | ifcld 4457 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ∈ ℝ) |
204 | 203 | rexrd 10762 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ∈
ℝ*) |
205 | | icombl 24309 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ∈ ℝ*) → ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)) ∈ dom vol) |
206 | 11, 204, 205 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)) ∈ dom vol) |
207 | 202, 206 | ffvelrnd 6856 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) ∈ (0[,]+∞)) |
208 | 62, 124, 6, 195, 141, 201, 207 | sge0splitsn 43505 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))))) |
209 | | volicore 43645 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) ∈ ℝ) |
210 | 11, 203, 209 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) ∈ ℝ) |
211 | | rexadd 12701 |
. . . . . . . . . . . . . 14
⊢
(((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ∧
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))))) |
212 | 121, 210,
211 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))))) |
213 | | volico 43050 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) = if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆), (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)), 0)) |
214 | 11, 203, 213 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) = if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆), (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)), 0)) |
215 | 16, 7 | ltnled 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (𝐷‘𝐾) ↔ ¬ (𝐷‘𝐾) ≤ 𝑆)) |
216 | 20, 215 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝐷‘𝐾) ≤ 𝑆) |
217 | 216 | iffalsed 4422 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) = 𝑆) |
218 | 217 | breq2d 5039 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) ↔ (𝐶‘𝐾) < 𝑆)) |
219 | 218 | ifbid 4434 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆), (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)), 0) = if((𝐶‘𝐾) < 𝑆, (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)), 0)) |
220 | 217 | oveq1d 7179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)) = (𝑆 − (𝐶‘𝐾))) |
221 | 220 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐶‘𝐾) < 𝑆) → (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)) = (𝑆 − (𝐶‘𝐾))) |
222 | 217, 204 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
223 | 222 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → 𝑆 ∈
ℝ*) |
224 | 18 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝐶‘𝐾) ∈
ℝ*) |
225 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → ¬ (𝐶‘𝐾) < 𝑆) |
226 | 16 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → 𝑆 ∈ ℝ) |
227 | 11 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝐶‘𝐾) ∈ ℝ) |
228 | 226, 227 | lenltd 10857 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝑆 ≤ (𝐶‘𝐾) ↔ ¬ (𝐶‘𝐾) < 𝑆)) |
229 | 225, 228 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → 𝑆 ≤ (𝐶‘𝐾)) |
230 | | icogelb 12865 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶‘𝐾) ∈ ℝ* ∧ (𝐷‘𝐾) ∈ ℝ* ∧ 𝑆 ∈ ((𝐶‘𝐾)[,)(𝐷‘𝐾))) → (𝐶‘𝐾) ≤ 𝑆) |
231 | 18, 12, 15, 230 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐶‘𝐾) ≤ 𝑆) |
232 | 231 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝐶‘𝐾) ≤ 𝑆) |
233 | 223, 224,
229, 232 | xrletrid 12624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → 𝑆 = (𝐶‘𝐾)) |
234 | 233 | oveq1d 7179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝑆 − (𝐶‘𝐾)) = ((𝐶‘𝐾) − (𝐶‘𝐾))) |
235 | 227 | recnd 10740 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → (𝐶‘𝐾) ∈ ℂ) |
236 | 235 | subidd 11056 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → ((𝐶‘𝐾) − (𝐶‘𝐾)) = 0) |
237 | 234, 236 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ (𝐶‘𝐾) < 𝑆) → 0 = (𝑆 − (𝐶‘𝐾))) |
238 | 221, 237 | ifeqda 4447 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if((𝐶‘𝐾) < 𝑆, (if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆) − (𝐶‘𝐾)), 0) = (𝑆 − (𝐶‘𝐾))) |
239 | 214, 219,
238 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆))) = (𝑆 − (𝐶‘𝐾))) |
240 | 239 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + (𝑆 − (𝐶‘𝐾)))) |
241 | 121 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℂ) |
242 | 11 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘𝐾) ∈ ℂ) |
243 | 36, 242 | subcld 11068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 − (𝐶‘𝐾)) ∈ ℂ) |
244 | 241, 243 | addcomd 10913 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + (𝑆 − (𝐶‘𝐾))) = ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
245 | 212, 240,
244 | 3eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑆, (𝐷‘𝐾), 𝑆)))) = ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
246 | 194, 208,
245 | 3eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
247 | 246 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) = ((𝑀 − 𝑆) + ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))) |
248 | 40 | recnd 10740 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 𝑆) ∈ ℂ) |
249 | 248, 243,
241 | addassd 10734 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑀 − 𝑆) + (𝑆 − (𝐶‘𝐾))) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) = ((𝑀 − 𝑆) + ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))) |
250 | 249 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − 𝑆) + ((𝑆 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) = (((𝑀 − 𝑆) + (𝑆 − (𝐶‘𝐾))) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
251 | 35, 36, 242 | npncand 11092 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 𝑆) + (𝑆 − (𝐶‘𝐾))) = (𝑀 − (𝐶‘𝐾))) |
252 | 251 | oveq1d 7179 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑀 − 𝑆) + (𝑆 − (𝐶‘𝐾))) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) = ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
253 | 247, 250,
252 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) = ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))) |
254 | 192 | mpteq1d 5116 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) |
255 | 254 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) =
(Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
256 | 197 | breq1d 5037 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐾 → ((𝐷‘𝑗) ≤ 𝑀 ↔ (𝐷‘𝐾) ≤ 𝑀)) |
257 | 256, 197 | ifbieq1d 4435 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐾 → if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀) = if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)) |
258 | 196, 257 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝐾 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) = ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) |
259 | 258 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝐾 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) = (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)))) |
260 | 7, 9 | ifcld 4457 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ∈ ℝ) |
261 | 260 | rexrd 10762 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ∈
ℝ*) |
262 | | icombl 24309 |
. . . . . . . . . . . . 13
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ∈ ℝ*) → ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)) ∈ dom vol) |
263 | 11, 261, 262 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)) ∈ dom vol) |
264 | 202, 263 | ffvelrnd 6856 |
. . . . . . . . . . 11
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) ∈ (0[,]+∞)) |
265 | 62, 124, 6, 195, 132, 259, 264 | sge0splitsn 43505 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))))) |
266 | | volicore 43645 |
. . . . . . . . . . . . 13
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) ∈ ℝ) |
267 | 11, 260, 266 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) ∈ ℝ) |
268 | | rexadd 12701 |
. . . . . . . . . . . 12
⊢
(((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℝ ∧
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))))) |
269 | 139, 267,
268 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))))) |
270 | | volico 43050 |
. . . . . . . . . . . . . 14
⊢ (((𝐶‘𝐾) ∈ ℝ ∧ if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) = if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀), (if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) − (𝐶‘𝐾)), 0)) |
271 | 11, 260, 270 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) = if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀), (if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) − (𝐶‘𝐾)), 0)) |
272 | 20, 157 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝑀)) |
273 | | ltmin 12663 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℝ ∧ (𝐷‘𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ↔ (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝑀))) |
274 | 16, 7, 9, 273 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) ↔ (𝑆 < (𝐷‘𝐾) ∧ 𝑆 < 𝑀))) |
275 | 272, 274 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)) |
276 | 11, 16, 260, 231, 275 | lelttrd 10869 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)) |
277 | 276 | iftrued 4419 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝐶‘𝐾) < if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀), (if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) − (𝐶‘𝐾)), 0) = (if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) − (𝐶‘𝐾))) |
278 | | iftrue 4417 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷‘𝐾) ≤ 𝑀 → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) = (𝐷‘𝐾)) |
279 | 278 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) = (𝐷‘𝐾)) |
280 | 12 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → (𝐷‘𝐾) ∈
ℝ*) |
281 | 9 | rexrd 10762 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
282 | 281 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → 𝑀 ∈
ℝ*) |
283 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → (𝐷‘𝐾) ≤ 𝑀) |
284 | | min1 12658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷‘𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ≤ (𝐷‘𝐾)) |
285 | 7, 2, 284 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ≤ (𝐷‘𝐾)) |
286 | 4, 285 | eqbrtrd 5049 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ≤ (𝐷‘𝐾)) |
287 | 286 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷‘𝐾)) |
288 | 280, 282,
283, 287 | xrletrid 12624 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → (𝐷‘𝐾) = 𝑀) |
289 | 279, 288 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐷‘𝐾) ≤ 𝑀) → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) = 𝑀) |
290 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ (𝐷‘𝐾) ≤ 𝑀) → ¬ (𝐷‘𝐾) ≤ 𝑀) |
291 | 290 | iffalsed 4422 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ (𝐷‘𝐾) ≤ 𝑀) → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) = 𝑀) |
292 | 289, 291 | pm2.61dan 813 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) = 𝑀) |
293 | 292 | oveq1d 7179 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀) − (𝐶‘𝐾)) = (𝑀 − (𝐶‘𝐾))) |
294 | 271, 277,
293 | 3eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀))) = (𝑀 − (𝐶‘𝐾))) |
295 | 294 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) + (vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)))) =
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) + (𝑀 − (𝐶‘𝐾)))) |
296 | 139 | recnd 10740 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ∈ ℂ) |
297 | 35, 242 | subcld 11068 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − (𝐶‘𝐾)) ∈ ℂ) |
298 | 296, 297 | addcomd 10913 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) + (𝑀 − (𝐶‘𝐾))) = ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
299 | 269, 295,
298 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) +𝑒
(vol‘((𝐶‘𝐾)[,)if((𝐷‘𝐾) ≤ 𝑀, (𝐷‘𝐾), 𝑀)))) = ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
300 | 255, 265,
299 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) = ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
301 | 253, 300 | breq12d 5040 |
. . . . . . . 8
⊢ (𝜑 → (((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶‘𝐾)) +
(Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))))) |
302 | 189, 301 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 − 𝑆) +
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
303 | 42, 82, 103, 119, 302 | letrd 10868 |
. . . . . 6
⊢ (𝜑 → ((𝑀 − 𝑆) + (𝑆 − 𝐴)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
304 | 39, 303 | eqbrtrd 5049 |
. . . . 5
⊢ (𝜑 → (𝑀 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
305 | 34, 304 | jca 515 |
. . . 4
⊢ (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
306 | | oveq1 7171 |
. . . . . 6
⊢ (𝑧 = 𝑀 → (𝑧 − 𝐴) = (𝑀 − 𝐴)) |
307 | | breq2 5031 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑀)) |
308 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → 𝑧 = 𝑀) |
309 | 307, 308 | ifbieq2d 4437 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)) |
310 | 309 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))) |
311 | 310 | fveq2d 6672 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))) |
312 | 311 | mpteq2dv 5123 |
. . . . . . 7
⊢ (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))) |
313 | 312 | fveq2d 6672 |
. . . . . 6
⊢ (𝑧 = 𝑀 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀)))))) |
314 | 306, 313 | breq12d 5040 |
. . . . 5
⊢ (𝑧 = 𝑀 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑀 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
315 | 314 | elrab 3585 |
. . . 4
⊢ (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑀, (𝐷‘𝑗), 𝑀))))))) |
316 | 305, 315 | sylibr 237 |
. . 3
⊢ (𝜑 → 𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
317 | 316, 105 | eleqtrrdi 2844 |
. 2
⊢ (𝜑 → 𝑀 ∈ 𝑈) |
318 | 272 | simprd 499 |
. 2
⊢ (𝜑 → 𝑆 < 𝑀) |
319 | | breq2 5031 |
. . 3
⊢ (𝑢 = 𝑀 → (𝑆 < 𝑢 ↔ 𝑆 < 𝑀)) |
320 | 319 | rspcev 3524 |
. 2
⊢ ((𝑀 ∈ 𝑈 ∧ 𝑆 < 𝑀) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
321 | 317, 318,
320 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |