Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmv1lelem2 Structured version   Visualization version   GIF version

Theorem hoidmv1lelem2 43656
Description: This is the contradiction proven in step (c) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmv1lelem2.a (𝜑𝐴 ∈ ℝ)
hoidmv1lelem2.b (𝜑𝐵 ∈ ℝ)
hoidmv1lelem2.c (𝜑𝐶:ℕ⟶ℝ)
hoidmv1lelem2.d (𝜑𝐷:ℕ⟶ℝ)
hoidmv1lelem2.r (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
hoidmv1lelem2.u 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
hoidmv1lelem2.e (𝜑𝑆𝑈)
hoidmv1lelem2.g (𝜑𝐴𝑆)
hoidmv1lelem2.l (𝜑𝑆 < 𝐵)
hoidmv1lelem2.k (𝜑𝐾 ∈ ℕ)
hoidmv1lelem2.s (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
hoidmv1lelem2.m 𝑀 = if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵)
Assertion
Ref Expression
hoidmv1lelem2 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝐶,𝑗,𝑧   𝐷,𝑗,𝑧   𝑗,𝐾   𝑗,𝑀,𝑧   𝑢,𝑀   𝑆,𝑗,𝑧   𝑢,𝑆   𝑢,𝑈   𝜑,𝑗
Allowed substitution hints:   𝜑(𝑧,𝑢)   𝐴(𝑢,𝑗)   𝐵(𝑢,𝑗)   𝐶(𝑢)   𝐷(𝑢)   𝑈(𝑧,𝑗)   𝐾(𝑧,𝑢)

Proof of Theorem hoidmv1lelem2
StepHypRef Expression
1 hoidmv1lelem2.a . . . . . 6 (𝜑𝐴 ∈ ℝ)
2 hoidmv1lelem2.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
3 hoidmv1lelem2.m . . . . . . . 8 𝑀 = if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵)
43a1i 11 . . . . . . 7 (𝜑𝑀 = if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
5 hoidmv1lelem2.d . . . . . . . . 9 (𝜑𝐷:ℕ⟶ℝ)
6 hoidmv1lelem2.k . . . . . . . . 9 (𝜑𝐾 ∈ ℕ)
75, 6ffvelrnd 6856 . . . . . . . 8 (𝜑 → (𝐷𝐾) ∈ ℝ)
87, 2ifcld 4457 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ∈ ℝ)
94, 8eqeltrd 2833 . . . . . 6 (𝜑𝑀 ∈ ℝ)
10 hoidmv1lelem2.c . . . . . . . . . . 11 (𝜑𝐶:ℕ⟶ℝ)
1110, 6ffvelrnd 6856 . . . . . . . . . 10 (𝜑 → (𝐶𝐾) ∈ ℝ)
127rexrd 10762 . . . . . . . . . 10 (𝜑 → (𝐷𝐾) ∈ ℝ*)
13 icossre 12895 . . . . . . . . . 10 (((𝐶𝐾) ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ*) → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
1411, 12, 13syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
15 hoidmv1lelem2.s . . . . . . . . 9 (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
1614, 15sseldd 3876 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
17 hoidmv1lelem2.g . . . . . . . 8 (𝜑𝐴𝑆)
1811rexrd 10762 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐾) ∈ ℝ*)
19 icoltub 42570 . . . . . . . . . . . 12 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → 𝑆 < (𝐷𝐾))
2018, 12, 15, 19syl3anc 1372 . . . . . . . . . . 11 (𝜑𝑆 < (𝐷𝐾))
2116, 7, 20ltled 10859 . . . . . . . . . 10 (𝜑𝑆 ≤ (𝐷𝐾))
22 hoidmv1lelem2.l . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
2316, 2, 22ltled 10859 . . . . . . . . . 10 (𝜑𝑆𝐵)
2421, 23jca 515 . . . . . . . . 9 (𝜑 → (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵))
25 lemin 12661 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2616, 7, 2, 25syl3anc 1372 . . . . . . . . 9 (𝜑 → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2724, 26mpbird 260 . . . . . . . 8 (𝜑𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
281, 16, 8, 17, 27letrd 10868 . . . . . . 7 (𝜑𝐴 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
294eqcomd 2744 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) = 𝑀)
3028, 29breqtrd 5053 . . . . . 6 (𝜑𝐴𝑀)
31 min2 12659 . . . . . . . 8 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
327, 2, 31syl2anc 587 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
334, 32eqbrtrd 5049 . . . . . 6 (𝜑𝑀𝐵)
341, 2, 9, 30, 33eliccd 42566 . . . . 5 (𝜑𝑀 ∈ (𝐴[,]𝐵))
359recnd 10740 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3616recnd 10740 . . . . . . . 8 (𝜑𝑆 ∈ ℂ)
371recnd 10740 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3835, 36, 37npncand 11092 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) = (𝑀𝐴))
3938eqcomd 2744 . . . . . 6 (𝜑 → (𝑀𝐴) = ((𝑀𝑆) + (𝑆𝐴)))
409, 16resubcld 11139 . . . . . . . 8 (𝜑 → (𝑀𝑆) ∈ ℝ)
4116, 1resubcld 11139 . . . . . . . 8 (𝜑 → (𝑆𝐴) ∈ ℝ)
4240, 41readdcld 10741 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ∈ ℝ)
43 nnex 11715 . . . . . . . . . . . . 13 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ ∈ V)
45 volf 24274 . . . . . . . . . . . . . . 15 vol:dom vol⟶(0[,]+∞)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
4710ffvelrnda 6855 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
485ffvelrnda 6855 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
4916adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
5048, 49ifcld 4457 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ)
5150rexrd 10762 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*)
52 icombl 24309 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5347, 51, 52syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5446, 53ffvelrnd 6856 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
55 eqid 2738 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
5654, 55fmptd 6882 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
5744, 56sge0xrcl 43449 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ*)
58 pnfxr 10766 . . . . . . . . . . . 12 +∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
60 hoidmv1lelem2.r . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
6160rexrd 10762 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
62 nfv 1920 . . . . . . . . . . . . 13 𝑗𝜑
6348rexrd 10762 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
64 icombl 24309 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6547, 63, 64syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6646, 65ffvelrnd 6856 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
6747rexrd 10762 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
6847leidd 11277 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
69 min1 12658 . . . . . . . . . . . . . . . 16 (((𝐷𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
7048, 49, 69syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
71 icossico 12884 . . . . . . . . . . . . . . 15 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
7267, 63, 68, 70, 71syl22anc 838 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
73 volss 24278 . . . . . . . . . . . . . 14 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7453, 65, 72, 73syl3anc 1372 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7562, 44, 54, 66, 74sge0lempt 43474 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
7660ltpnfd 12592 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
7757, 61, 59, 75, 76xrlelttrd 12629 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) < +∞)
7857, 59, 77xrltned 42418 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≠ +∞)
7978neneqd 2939 . . . . . . . . 9 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞)
8044, 56sge0repnf 43450 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞))
8179, 80mpbird 260 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
8240, 81readdcld 10741 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ∈ ℝ)
839adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℝ)
8448, 83ifcld 4457 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
8584rexrd 10762 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
86 icombl 24309 . . . . . . . . . . . . . 14 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8747, 85, 86syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8846, 87ffvelrnd 6856 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
89 eqid 2738 . . . . . . . . . . . 12 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
9088, 89fmptd 6882 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))):ℕ⟶(0[,]+∞))
9144, 90sge0xrcl 43449 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
92 min1 12658 . . . . . . . . . . . . . . 15 (((𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
9348, 83, 92syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
94 icossico 12884 . . . . . . . . . . . . . 14 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
9567, 63, 68, 93, 94syl22anc 838 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
96 volss 24278 . . . . . . . . . . . . 13 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9787, 65, 95, 96syl3anc 1372 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9862, 44, 88, 66, 97sge0lempt 43474 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
9991, 61, 59, 98, 76xrlelttrd 12629 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
10091, 59, 99xrltned 42418 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
101100neneqd 2939 . . . . . . . 8 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
10244, 90sge0repnf 43450 . . . . . . . 8 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
103101, 102mpbird 260 . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
104 hoidmv1lelem2.e . . . . . . . . . . 11 (𝜑𝑆𝑈)
105 hoidmv1lelem2.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
106104, 105eleqtrdi 2843 . . . . . . . . . 10 (𝜑𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
107 oveq1 7171 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝑧𝐴) = (𝑆𝐴))
108 simpl 486 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑆𝑗 ∈ ℕ) → 𝑧 = 𝑆)
109108breq2d 5039 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑆))
110109, 108ifbieq2d 4437 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑆𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))
111110oveq2d 7180 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))
112111fveq2d 6672 . . . . . . . . . . . . . 14 ((𝑧 = 𝑆𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
113112mpteq2dva 5122 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
114113fveq2d 6672 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
115107, 114breq12d 5040 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
116115elrab 3585 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
117106, 116sylib 221 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
118117simprd 499 . . . . . . . 8 (𝜑 → (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
11941, 81, 40, 118leadd2dd 11326 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
120 difssd 4021 . . . . . . . . . 10 (𝜑 → (ℕ ∖ {𝐾}) ⊆ ℕ)
12162, 44, 54, 81, 120sge0ssrempt 43469 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
122 difexg 5192 . . . . . . . . . . . . . . 15 (ℕ ∈ V → (ℕ ∖ {𝐾}) ∈ V)
12343, 122ax-mp 5 . . . . . . . . . . . . . 14 (ℕ ∖ {𝐾}) ∈ V
124123a1i 11 . . . . . . . . . . . . 13 (𝜑 → (ℕ ∖ {𝐾}) ∈ V)
12545a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → vol:dom vol⟶(0[,]+∞))
126 simpl 486 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝜑)
127 eldifi 4015 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ)
128127adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ)
129126, 128, 47syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ)
130128, 85syldan 594 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
131129, 130, 86syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
132125, 131ffvelrnd 6856 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
13362, 124, 132sge0xrclmpt 43492 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
13444, 88, 120sge0lessmpt 43463 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
135133, 91, 59, 134, 99xrlelttrd 12629 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
136133, 59, 135xrltned 42418 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
137136neneqd 2939 . . . . . . . . . 10 (𝜑 → ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
13862, 124, 132sge0repnfmpt 43503 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
139137, 138mpbird 260 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
1409, 11resubcld 11139 . . . . . . . . 9 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℝ)
141128, 54syldan 594 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
142128, 53syldan 594 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
143128, 67syldan 594 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ*)
144128, 68syldan 594 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ≤ (𝐶𝑗))
145 iftrue 4417 . . . . . . . . . . . . . . . 16 ((𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
146145adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
14748leidd 11277 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ≤ (𝐷𝑗))
148147adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ (𝐷𝑗))
14948adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
15083adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
15149adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
152 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑆)
15320, 22jca 515 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵))
154 ltmin 12663 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
15516, 7, 2, 154syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
156153, 155mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
157156, 29breqtrd 5053 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 < 𝑀)
158157ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
159149, 151, 150, 152, 158lelttrd 10869 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) < 𝑀)
160149, 150, 159ltled 10859 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑀)
161148, 160jca 515 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀))
162 lemin 12661 . . . . . . . . . . . . . . . . 17 (((𝐷𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
163149, 149, 150, 162syl3anc 1372 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
164161, 163mpbird 260 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
165146, 164eqbrtrd 5049 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
166 iffalse 4420 . . . . . . . . . . . . . . . 16 (¬ (𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
167166adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
16849adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
16984adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
170 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → ¬ (𝐷𝑗) ≤ 𝑆)
17148adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
172168, 171ltnled 10858 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ↔ ¬ (𝐷𝑗) ≤ 𝑆))
173170, 172mpbird 260 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < (𝐷𝑗))
174157ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
175173, 174jca 515 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀))
17683adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
177 ltmin 12663 . . . . . . . . . . . . . . . . . 18 ((𝑆 ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
178168, 171, 176, 177syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
179175, 178mpbird 260 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
180168, 169, 179ltled 10859 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
181167, 180eqbrtrd 5049 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
182165, 181pm2.61dan 813 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
183128, 182syldan 594 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
184 icossico 12884 . . . . . . . . . . . 12 ((((𝐶𝑗) ∈ ℝ* ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
185143, 130, 144, 183, 184syl22anc 838 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
186 volss 24278 . . . . . . . . . . 11 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
187142, 131, 185, 186syl3anc 1372 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
18862, 124, 141, 132, 187sge0lempt 43474 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
189121, 139, 140, 188leadd2dd 11326 . . . . . . . 8 (𝜑 → ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
190 difsnid 4695 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
1916, 190syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
192191eqcomd 2744 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℕ ∖ {𝐾}) ∪ {𝐾}))
193192mpteq1d 5116 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
194193fveq2d 6672 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
195 neldifsnd 4678 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾}))
196 fveq2 6668 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → (𝐶𝑗) = (𝐶𝐾))
197 fveq2 6668 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐾 → (𝐷𝑗) = (𝐷𝐾))
198197breq1d 5037 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑆 ↔ (𝐷𝐾) ≤ 𝑆))
199198, 197ifbieq1d 4435 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))
200196, 199oveq12d 7182 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))
201200fveq2d 6672 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))))
20245a1i 11 . . . . . . . . . . . . . 14 (𝜑 → vol:dom vol⟶(0[,]+∞))
2037, 16ifcld 4457 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ)
204203rexrd 10762 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*)
205 icombl 24309 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
20611, 204, 205syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
207202, 206ffvelrnd 6856 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ (0[,]+∞))
20862, 124, 6, 195, 141, 201, 207sge0splitsn 43505 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
209 volicore 43645 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
21011, 203, 209syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
211 rexadd 12701 . . . . . . . . . . . . . 14 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
212121, 210, 211syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
213 volico 43050 . . . . . . . . . . . . . . . 16 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21411, 203, 213syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21516, 7ltnled 10858 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐷𝐾) ↔ ¬ (𝐷𝐾) ≤ 𝑆))
21620, 215mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐷𝐾) ≤ 𝑆)
217216iffalsed 4422 . . . . . . . . . . . . . . . . 17 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) = 𝑆)
218217breq2d 5039 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ↔ (𝐶𝐾) < 𝑆))
219218ifbid 4434 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
220217oveq1d 7179 . . . . . . . . . . . . . . . . 17 (𝜑 → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
221220adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐶𝐾) < 𝑆) → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
222217, 204eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ∈ ℝ*)
223222adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ*)
22418adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ*)
225 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ¬ (𝐶𝐾) < 𝑆)
22616adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ)
22711adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ)
228226, 227lenltd 10857 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 ≤ (𝐶𝐾) ↔ ¬ (𝐶𝐾) < 𝑆))
229225, 228mpbird 260 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ≤ (𝐶𝐾))
230 icogelb 12865 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → (𝐶𝐾) ≤ 𝑆)
23118, 12, 15, 230syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶𝐾) ≤ 𝑆)
232231adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ≤ 𝑆)
233223, 224, 229, 232xrletrid 12624 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 = (𝐶𝐾))
234233oveq1d 7179 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 − (𝐶𝐾)) = ((𝐶𝐾) − (𝐶𝐾)))
235227recnd 10740 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℂ)
236235subidd 11056 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ((𝐶𝐾) − (𝐶𝐾)) = 0)
237234, 236eqtr2d 2774 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 0 = (𝑆 − (𝐶𝐾)))
238221, 237ifeqda 4447 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = (𝑆 − (𝐶𝐾)))
239214, 219, 2383eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = (𝑆 − (𝐶𝐾)))
240239oveq2d 7180 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))))
241121recnd 10740 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℂ)
24211recnd 10740 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐾) ∈ ℂ)
24336, 242subcld 11068 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 − (𝐶𝐾)) ∈ ℂ)
244241, 243addcomd 10913 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
245212, 240, 2443eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
246194, 208, 2453eqtrd 2777 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
247246oveq2d 7180 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
24840recnd 10740 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑆) ∈ ℂ)
249248, 243, 241addassd 10734 . . . . . . . . . . 11 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
250249eqcomd 2744 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))) = (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
25135, 36, 242npncand 11092 . . . . . . . . . . 11 (𝜑 → ((𝑀𝑆) + (𝑆 − (𝐶𝐾))) = (𝑀 − (𝐶𝐾)))
252251oveq1d 7179 . . . . . . . . . 10 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
253247, 250, 2523eqtrd 2777 . . . . . . . . 9 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
254192mpteq1d 5116 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
255254fveq2d 6672 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
256197breq1d 5037 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑀 ↔ (𝐷𝐾) ≤ 𝑀))
257256, 197ifbieq1d 4435 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) = if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
258196, 257oveq12d 7182 . . . . . . . . . . . 12 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))
259258fveq2d 6672 . . . . . . . . . . 11 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))))
2607, 9ifcld 4457 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ)
261260rexrd 10762 . . . . . . . . . . . . 13 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*)
262 icombl 24309 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
26311, 261, 262syl2anc 587 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
264202, 263ffvelrnd 6856 . . . . . . . . . . 11 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ (0[,]+∞))
26562, 124, 6, 195, 132, 259, 264sge0splitsn 43505 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
266 volicore 43645 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
26711, 260, 266syl2anc 587 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
268 rexadd 12701 . . . . . . . . . . . 12 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
269139, 267, 268syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
270 volico 43050 . . . . . . . . . . . . . 14 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27111, 260, 270syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27220, 157jca 515 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀))
273 ltmin 12663 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
27416, 7, 9, 273syl3anc 1372 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
275272, 274mpbird 260 . . . . . . . . . . . . . . 15 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
27611, 16, 260, 231, 275lelttrd 10869 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
277276iftrued 4419 . . . . . . . . . . . . 13 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0) = (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)))
278 iftrue 4417 . . . . . . . . . . . . . . . . 17 ((𝐷𝐾) ≤ 𝑀 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
279278adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
28012adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ∈ ℝ*)
2819rexrd 10762 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ*)
282281adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ∈ ℝ*)
283 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ≤ 𝑀)
284 min1 12658 . . . . . . . . . . . . . . . . . . . 20 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2857, 2, 284syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2864, 285eqbrtrd 5049 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ≤ (𝐷𝐾))
287286adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷𝐾))
288280, 282, 283, 287xrletrid 12624 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) = 𝑀)
289279, 288eqtrd 2773 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
290 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → ¬ (𝐷𝐾) ≤ 𝑀)
291290iffalsed 4422 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
292289, 291pm2.61dan 813 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
293292oveq1d 7179 . . . . . . . . . . . . 13 (𝜑 → (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)) = (𝑀 − (𝐶𝐾)))
294271, 277, 2933eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = (𝑀 − (𝐶𝐾)))
295294oveq2d 7180 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))))
296139recnd 10740 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℂ)
29735, 242subcld 11068 . . . . . . . . . . . 12 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℂ)
298296, 297addcomd 10913 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
299269, 295, 2983eqtrd 2777 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
300255, 265, 2993eqtrd 2777 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
301253, 300breq12d 5040 . . . . . . . 8 (𝜑 → (((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))))
302189, 301mpbird 260 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30342, 82, 103, 119, 302letrd 10868 . . . . . 6 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30439, 303eqbrtrd 5049 . . . . 5 (𝜑 → (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30534, 304jca 515 . . . 4 (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
306 oveq1 7171 . . . . . 6 (𝑧 = 𝑀 → (𝑧𝐴) = (𝑀𝐴))
307 breq2 5031 . . . . . . . . . . 11 (𝑧 = 𝑀 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑀))
308 id 22 . . . . . . . . . . 11 (𝑧 = 𝑀𝑧 = 𝑀)
309307, 308ifbieq2d 4437 . . . . . . . . . 10 (𝑧 = 𝑀 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
310309oveq2d 7180 . . . . . . . . 9 (𝑧 = 𝑀 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
311310fveq2d 6672 . . . . . . . 8 (𝑧 = 𝑀 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
312311mpteq2dv 5123 . . . . . . 7 (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
313312fveq2d 6672 . . . . . 6 (𝑧 = 𝑀 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
314306, 313breq12d 5040 . . . . 5 (𝑧 = 𝑀 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
315314elrab 3585 . . . 4 (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
316305, 315sylibr 237 . . 3 (𝜑𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
317316, 105eleqtrrdi 2844 . 2 (𝜑𝑀𝑈)
318272simprd 499 . 2 (𝜑𝑆 < 𝑀)
319 breq2 5031 . . 3 (𝑢 = 𝑀 → (𝑆 < 𝑢𝑆 < 𝑀))
320319rspcev 3524 . 2 ((𝑀𝑈𝑆 < 𝑀) → ∃𝑢𝑈 𝑆 < 𝑢)
321317, 318, 320syl2anc 587 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1542  wcel 2113  wrex 3054  {crab 3057  Vcvv 3397  cdif 3838  cun 3839  wss 3841  ifcif 4411  {csn 4513   class class class wbr 5027  cmpt 5107  dom cdm 5519  wf 6329  cfv 6333  (class class class)co 7164  cr 10607  0cc0 10608   + caddc 10611  +∞cpnf 10743  *cxr 10745   < clt 10746  cle 10747  cmin 10941  cn 11709   +𝑒 cxad 12581  [,)cico 12816  [,]cicc 12817  volcvol 24208  Σ^csumge0 43426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-inf2 9170  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-of 7419  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-2o 8125  df-er 8313  df-map 8432  df-pm 8433  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-fi 8941  df-sup 8972  df-inf 8973  df-oi 9040  df-dju 9396  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-div 11369  df-nn 11710  df-2 11772  df-3 11773  df-n0 11970  df-z 12056  df-uz 12318  df-q 12424  df-rp 12466  df-xneg 12583  df-xadd 12584  df-xmul 12585  df-ioo 12818  df-ico 12820  df-icc 12821  df-fz 12975  df-fzo 13118  df-fl 13246  df-seq 13454  df-exp 13515  df-hash 13776  df-cj 14541  df-re 14542  df-im 14543  df-sqrt 14677  df-abs 14678  df-clim 14928  df-rlim 14929  df-sum 15129  df-rest 16792  df-topgen 16813  df-psmet 20202  df-xmet 20203  df-met 20204  df-bl 20205  df-mopn 20206  df-top 21638  df-topon 21655  df-bases 21690  df-cmp 22131  df-ovol 24209  df-vol 24210  df-sumge0 43427
This theorem is referenced by:  hoidmv1lelem3  43657
  Copyright terms: Public domain W3C validator