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

Theorem hoidmv1lelem2 42442
 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 6722 . . . . . . . 8 (𝜑 → (𝐷𝐾) ∈ ℝ)
87, 2ifcld 4430 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ∈ ℝ)
94, 8eqeltrd 2883 . . . . . 6 (𝜑𝑀 ∈ ℝ)
10 hoidmv1lelem2.c . . . . . . . . . . 11 (𝜑𝐶:ℕ⟶ℝ)
1110, 6ffvelrnd 6722 . . . . . . . . . 10 (𝜑 → (𝐶𝐾) ∈ ℝ)
127rexrd 10542 . . . . . . . . . 10 (𝜑 → (𝐷𝐾) ∈ ℝ*)
13 icossre 12672 . . . . . . . . . 10 (((𝐶𝐾) ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ*) → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
1411, 12, 13syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
15 hoidmv1lelem2.s . . . . . . . . 9 (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
1614, 15sseldd 3894 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
17 hoidmv1lelem2.g . . . . . . . 8 (𝜑𝐴𝑆)
1811rexrd 10542 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐾) ∈ ℝ*)
19 icoltub 41351 . . . . . . . . . . . 12 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → 𝑆 < (𝐷𝐾))
2018, 12, 15, 19syl3anc 1364 . . . . . . . . . . 11 (𝜑𝑆 < (𝐷𝐾))
2116, 7, 20ltled 10640 . . . . . . . . . 10 (𝜑𝑆 ≤ (𝐷𝐾))
22 hoidmv1lelem2.l . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
2316, 2, 22ltled 10640 . . . . . . . . . 10 (𝜑𝑆𝐵)
2421, 23jca 512 . . . . . . . . 9 (𝜑 → (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵))
25 lemin 12440 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2616, 7, 2, 25syl3anc 1364 . . . . . . . . 9 (𝜑 → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2724, 26mpbird 258 . . . . . . . 8 (𝜑𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
281, 16, 8, 17, 27letrd 10649 . . . . . . 7 (𝜑𝐴 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
294eqcomd 2801 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) = 𝑀)
3028, 29breqtrd 4992 . . . . . 6 (𝜑𝐴𝑀)
31 min2 12438 . . . . . . . 8 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
327, 2, 31syl2anc 584 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
334, 32eqbrtrd 4988 . . . . . 6 (𝜑𝑀𝐵)
341, 2, 9, 30, 33eliccd 41346 . . . . 5 (𝜑𝑀 ∈ (𝐴[,]𝐵))
359recnd 10520 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3616recnd 10520 . . . . . . . 8 (𝜑𝑆 ∈ ℂ)
371recnd 10520 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3835, 36, 37npncand 10874 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) = (𝑀𝐴))
3938eqcomd 2801 . . . . . 6 (𝜑 → (𝑀𝐴) = ((𝑀𝑆) + (𝑆𝐴)))
409, 16resubcld 10921 . . . . . . . 8 (𝜑 → (𝑀𝑆) ∈ ℝ)
4116, 1resubcld 10921 . . . . . . . 8 (𝜑 → (𝑆𝐴) ∈ ℝ)
4240, 41readdcld 10521 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ∈ ℝ)
43 nnex 11497 . . . . . . . . . . . . 13 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ ∈ V)
45 volf 23818 . . . . . . . . . . . . . . 15 vol:dom vol⟶(0[,]+∞)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
4710ffvelrnda 6721 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
485ffvelrnda 6721 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
4916adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
5048, 49ifcld 4430 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ)
5150rexrd 10542 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*)
52 icombl 23853 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5347, 51, 52syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5446, 53ffvelrnd 6722 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
55 eqid 2795 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
5654, 55fmptd 6746 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
5744, 56sge0xrcl 42235 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ*)
58 pnfxr 10546 . . . . . . . . . . . 12 +∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
60 hoidmv1lelem2.r . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
6160rexrd 10542 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
62 nfv 1892 . . . . . . . . . . . . 13 𝑗𝜑
6348rexrd 10542 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
64 icombl 23853 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6547, 63, 64syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6646, 65ffvelrnd 6722 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
6747rexrd 10542 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
6847leidd 11059 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
69 min1 12437 . . . . . . . . . . . . . . . 16 (((𝐷𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
7048, 49, 69syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
71 icossico 12661 . . . . . . . . . . . . . . 15 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
7267, 63, 68, 70, 71syl22anc 835 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
73 volss 23822 . . . . . . . . . . . . . 14 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7453, 65, 72, 73syl3anc 1364 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7562, 44, 54, 66, 74sge0lempt 42260 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
7660ltpnfd 12371 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
7757, 61, 59, 75, 76xrlelttrd 12408 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) < +∞)
7857, 59, 77xrltned 41191 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≠ +∞)
7978neneqd 2989 . . . . . . . . 9 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞)
8044, 56sge0repnf 42236 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞))
8179, 80mpbird 258 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
8240, 81readdcld 10521 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ∈ ℝ)
839adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℝ)
8448, 83ifcld 4430 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
8584rexrd 10542 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
86 icombl 23853 . . . . . . . . . . . . . 14 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8747, 85, 86syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8846, 87ffvelrnd 6722 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
89 eqid 2795 . . . . . . . . . . . 12 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
9088, 89fmptd 6746 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))):ℕ⟶(0[,]+∞))
9144, 90sge0xrcl 42235 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
92 min1 12437 . . . . . . . . . . . . . . 15 (((𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
9348, 83, 92syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
94 icossico 12661 . . . . . . . . . . . . . 14 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
9567, 63, 68, 93, 94syl22anc 835 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
96 volss 23822 . . . . . . . . . . . . 13 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9787, 65, 95, 96syl3anc 1364 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9862, 44, 88, 66, 97sge0lempt 42260 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
9991, 61, 59, 98, 76xrlelttrd 12408 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
10091, 59, 99xrltned 41191 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
101100neneqd 2989 . . . . . . . 8 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
10244, 90sge0repnf 42236 . . . . . . . 8 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
103101, 102mpbird 258 . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
104 hoidmv1lelem2.e . . . . . . . . . . 11 (𝜑𝑆𝑈)
105 hoidmv1lelem2.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
106104, 105syl6eleq 2893 . . . . . . . . . 10 (𝜑𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
107 oveq1 7028 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝑧𝐴) = (𝑆𝐴))
108 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑆𝑗 ∈ ℕ) → 𝑧 = 𝑆)
109108breq2d 4978 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑆))
110109, 108ifbieq2d 4410 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑆𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))
111110oveq2d 7037 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))
112111fveq2d 6547 . . . . . . . . . . . . . 14 ((𝑧 = 𝑆𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
113112mpteq2dva 5060 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
114113fveq2d 6547 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
115107, 114breq12d 4979 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
116115elrab 3619 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
117106, 116sylib 219 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
118117simprd 496 . . . . . . . 8 (𝜑 → (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
11941, 81, 40, 118leadd2dd 11108 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
120 difssd 4034 . . . . . . . . . 10 (𝜑 → (ℕ ∖ {𝐾}) ⊆ ℕ)
12162, 44, 54, 81, 120sge0ssrempt 42255 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
122 difexg 5127 . . . . . . . . . . . . . . 15 (ℕ ∈ V → (ℕ ∖ {𝐾}) ∈ V)
12343, 122ax-mp 5 . . . . . . . . . . . . . 14 (ℕ ∖ {𝐾}) ∈ V
124123a1i 11 . . . . . . . . . . . . 13 (𝜑 → (ℕ ∖ {𝐾}) ∈ V)
12545a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → vol:dom vol⟶(0[,]+∞))
126 simpl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝜑)
127 eldifi 4028 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ)
128127adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ)
129126, 128, 47syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ)
130128, 85syldan 591 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
131129, 130, 86syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
132125, 131ffvelrnd 6722 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
13362, 124, 132sge0xrclmpt 42278 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
13444, 88, 120sge0lessmpt 42249 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
135133, 91, 59, 134, 99xrlelttrd 12408 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
136133, 59, 135xrltned 41191 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
137136neneqd 2989 . . . . . . . . . 10 (𝜑 → ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
13862, 124, 132sge0repnfmpt 42289 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
139137, 138mpbird 258 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
1409, 11resubcld 10921 . . . . . . . . 9 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℝ)
141128, 54syldan 591 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
142128, 53syldan 591 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
143128, 67syldan 591 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ*)
144128, 68syldan 591 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ≤ (𝐶𝑗))
145 iftrue 4391 . . . . . . . . . . . . . . . 16 ((𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
146145adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
14748leidd 11059 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ≤ (𝐷𝑗))
148147adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ (𝐷𝑗))
14948adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
15083adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
15149adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
152 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑆)
15320, 22jca 512 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵))
154 ltmin 12442 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
15516, 7, 2, 154syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
156153, 155mpbird 258 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
157156, 29breqtrd 4992 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 < 𝑀)
158157ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
159149, 151, 150, 152, 158lelttrd 10650 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) < 𝑀)
160149, 150, 159ltled 10640 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑀)
161148, 160jca 512 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀))
162 lemin 12440 . . . . . . . . . . . . . . . . 17 (((𝐷𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
163149, 149, 150, 162syl3anc 1364 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
164161, 163mpbird 258 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
165146, 164eqbrtrd 4988 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
166 iffalse 4394 . . . . . . . . . . . . . . . 16 (¬ (𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
167166adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
16849adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
16984adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
170 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → ¬ (𝐷𝑗) ≤ 𝑆)
17148adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
172168, 171ltnled 10639 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ↔ ¬ (𝐷𝑗) ≤ 𝑆))
173170, 172mpbird 258 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < (𝐷𝑗))
174157ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
175173, 174jca 512 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀))
17683adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
177 ltmin 12442 . . . . . . . . . . . . . . . . . 18 ((𝑆 ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
178168, 171, 176, 177syl3anc 1364 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
179175, 178mpbird 258 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
180168, 169, 179ltled 10640 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
181167, 180eqbrtrd 4988 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
182165, 181pm2.61dan 809 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
183128, 182syldan 591 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
184 icossico 12661 . . . . . . . . . . . 12 ((((𝐶𝑗) ∈ ℝ* ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
185143, 130, 144, 183, 184syl22anc 835 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
186 volss 23822 . . . . . . . . . . 11 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
187142, 131, 185, 186syl3anc 1364 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
18862, 124, 141, 132, 187sge0lempt 42260 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
189121, 139, 140, 188leadd2dd 11108 . . . . . . . 8 (𝜑 → ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
190 difsnid 4654 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
1916, 190syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
192191eqcomd 2801 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℕ ∖ {𝐾}) ∪ {𝐾}))
193192mpteq1d 5054 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
194193fveq2d 6547 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
195 neldifsnd 4637 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾}))
196 fveq2 6543 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → (𝐶𝑗) = (𝐶𝐾))
197 fveq2 6543 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐾 → (𝐷𝑗) = (𝐷𝐾))
198197breq1d 4976 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑆 ↔ (𝐷𝐾) ≤ 𝑆))
199198, 197ifbieq1d 4408 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))
200196, 199oveq12d 7039 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))
201200fveq2d 6547 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))))
20245a1i 11 . . . . . . . . . . . . . 14 (𝜑 → vol:dom vol⟶(0[,]+∞))
2037, 16ifcld 4430 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ)
204203rexrd 10542 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*)
205 icombl 23853 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
20611, 204, 205syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
207202, 206ffvelrnd 6722 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ (0[,]+∞))
20862, 124, 6, 195, 141, 201, 207sge0splitsn 42291 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
209 volicore 42431 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
21011, 203, 209syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
211 rexadd 12480 . . . . . . . . . . . . . 14 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
212121, 210, 211syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
213 volico 41836 . . . . . . . . . . . . . . . 16 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21411, 203, 213syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21516, 7ltnled 10639 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐷𝐾) ↔ ¬ (𝐷𝐾) ≤ 𝑆))
21620, 215mpbid 233 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐷𝐾) ≤ 𝑆)
217216iffalsed 4396 . . . . . . . . . . . . . . . . 17 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) = 𝑆)
218217breq2d 4978 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ↔ (𝐶𝐾) < 𝑆))
219218ifbid 4407 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
220217oveq1d 7036 . . . . . . . . . . . . . . . . 17 (𝜑 → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
221220adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐶𝐾) < 𝑆) → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
222217, 204eqeltrrd 2884 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ∈ ℝ*)
223222adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ*)
22418adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ*)
225 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ¬ (𝐶𝐾) < 𝑆)
22616adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ)
22711adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ)
228226, 227lenltd 10638 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 ≤ (𝐶𝐾) ↔ ¬ (𝐶𝐾) < 𝑆))
229225, 228mpbird 258 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ≤ (𝐶𝐾))
230 icogelb 12643 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → (𝐶𝐾) ≤ 𝑆)
23118, 12, 15, 230syl3anc 1364 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶𝐾) ≤ 𝑆)
232231adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ≤ 𝑆)
233223, 224, 229, 232xrletrid 12403 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 = (𝐶𝐾))
234233oveq1d 7036 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 − (𝐶𝐾)) = ((𝐶𝐾) − (𝐶𝐾)))
235227recnd 10520 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℂ)
236235subidd 10838 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ((𝐶𝐾) − (𝐶𝐾)) = 0)
237234, 236eqtr2d 2832 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 0 = (𝑆 − (𝐶𝐾)))
238221, 237ifeqda 4420 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = (𝑆 − (𝐶𝐾)))
239214, 219, 2383eqtrd 2835 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = (𝑆 − (𝐶𝐾)))
240239oveq2d 7037 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))))
241121recnd 10520 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℂ)
24211recnd 10520 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐾) ∈ ℂ)
24336, 242subcld 10850 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 − (𝐶𝐾)) ∈ ℂ)
244241, 243addcomd 10694 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
245212, 240, 2443eqtrd 2835 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
246194, 208, 2453eqtrd 2835 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
247246oveq2d 7037 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
24840recnd 10520 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑆) ∈ ℂ)
249248, 243, 241addassd 10514 . . . . . . . . . . 11 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
250249eqcomd 2801 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))) = (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
25135, 36, 242npncand 10874 . . . . . . . . . . 11 (𝜑 → ((𝑀𝑆) + (𝑆 − (𝐶𝐾))) = (𝑀 − (𝐶𝐾)))
252251oveq1d 7036 . . . . . . . . . 10 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
253247, 250, 2523eqtrd 2835 . . . . . . . . 9 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
254192mpteq1d 5054 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
255254fveq2d 6547 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
256197breq1d 4976 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑀 ↔ (𝐷𝐾) ≤ 𝑀))
257256, 197ifbieq1d 4408 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) = if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
258196, 257oveq12d 7039 . . . . . . . . . . . 12 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))
259258fveq2d 6547 . . . . . . . . . . 11 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))))
2607, 9ifcld 4430 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ)
261260rexrd 10542 . . . . . . . . . . . . 13 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*)
262 icombl 23853 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
26311, 261, 262syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
264202, 263ffvelrnd 6722 . . . . . . . . . . 11 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ (0[,]+∞))
26562, 124, 6, 195, 132, 259, 264sge0splitsn 42291 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
266 volicore 42431 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
26711, 260, 266syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
268 rexadd 12480 . . . . . . . . . . . 12 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
269139, 267, 268syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
270 volico 41836 . . . . . . . . . . . . . 14 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27111, 260, 270syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27220, 157jca 512 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀))
273 ltmin 12442 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
27416, 7, 9, 273syl3anc 1364 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
275272, 274mpbird 258 . . . . . . . . . . . . . . 15 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
27611, 16, 260, 231, 275lelttrd 10650 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
277276iftrued 4393 . . . . . . . . . . . . 13 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0) = (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)))
278 iftrue 4391 . . . . . . . . . . . . . . . . 17 ((𝐷𝐾) ≤ 𝑀 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
279278adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
28012adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ∈ ℝ*)
2819rexrd 10542 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ*)
282281adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ∈ ℝ*)
283 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ≤ 𝑀)
284 min1 12437 . . . . . . . . . . . . . . . . . . . 20 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2857, 2, 284syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2864, 285eqbrtrd 4988 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ≤ (𝐷𝐾))
287286adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷𝐾))
288280, 282, 283, 287xrletrid 12403 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) = 𝑀)
289279, 288eqtrd 2831 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
290 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → ¬ (𝐷𝐾) ≤ 𝑀)
291290iffalsed 4396 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
292289, 291pm2.61dan 809 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
293292oveq1d 7036 . . . . . . . . . . . . 13 (𝜑 → (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)) = (𝑀 − (𝐶𝐾)))
294271, 277, 2933eqtrd 2835 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = (𝑀 − (𝐶𝐾)))
295294oveq2d 7037 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))))
296139recnd 10520 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℂ)
29735, 242subcld 10850 . . . . . . . . . . . 12 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℂ)
298296, 297addcomd 10694 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
299269, 295, 2983eqtrd 2835 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
300255, 265, 2993eqtrd 2835 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
301253, 300breq12d 4979 . . . . . . . 8 (𝜑 → (((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))))
302189, 301mpbird 258 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30342, 82, 103, 119, 302letrd 10649 . . . . . 6 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30439, 303eqbrtrd 4988 . . . . 5 (𝜑 → (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30534, 304jca 512 . . . 4 (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
306 oveq1 7028 . . . . . 6 (𝑧 = 𝑀 → (𝑧𝐴) = (𝑀𝐴))
307 breq2 4970 . . . . . . . . . . 11 (𝑧 = 𝑀 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑀))
308 id 22 . . . . . . . . . . 11 (𝑧 = 𝑀𝑧 = 𝑀)
309307, 308ifbieq2d 4410 . . . . . . . . . 10 (𝑧 = 𝑀 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
310309oveq2d 7037 . . . . . . . . 9 (𝑧 = 𝑀 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
311310fveq2d 6547 . . . . . . . 8 (𝑧 = 𝑀 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
312311mpteq2dv 5061 . . . . . . 7 (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
313312fveq2d 6547 . . . . . 6 (𝑧 = 𝑀 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
314306, 313breq12d 4979 . . . . 5 (𝑧 = 𝑀 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
315314elrab 3619 . . . 4 (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
316305, 315sylibr 235 . . 3 (𝜑𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
317316, 105syl6eleqr 2894 . 2 (𝜑𝑀𝑈)
318272simprd 496 . 2 (𝜑𝑆 < 𝑀)
319 breq2 4970 . . 3 (𝑢 = 𝑀 → (𝑆 < 𝑢𝑆 < 𝑀))
320319rspcev 3559 . 2 ((𝑀𝑈𝑆 < 𝑀) → ∃𝑢𝑈 𝑆 < 𝑢)
321317, 318, 320syl2anc 584 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∃wrex 3106  {crab 3109  Vcvv 3437   ∖ cdif 3860   ∪ cun 3861   ⊆ wss 3863  ifcif 4385  {csn 4476   class class class wbr 4966   ↦ cmpt 5045  dom cdm 5448  ⟶wf 6226  ‘cfv 6230  (class class class)co 7021  ℝcr 10387  0cc0 10388   + caddc 10391  +∞cpnf 10523  ℝ*cxr 10525   < clt 10526   ≤ cle 10527   − cmin 10722  ℕcn 11491   +𝑒 cxad 12360  [,)cico 12595  [,]cicc 12596  volcvol 23752  Σ^csumge0 42212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-inf2 8955  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465  ax-pre-sup 10466 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-se 5408  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-isom 6239  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-of 7272  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-1o 7958  df-2o 7959  df-oadd 7962  df-er 8144  df-map 8263  df-pm 8264  df-en 8363  df-dom 8364  df-sdom 8365  df-fin 8366  df-fi 8726  df-sup 8757  df-inf 8758  df-oi 8825  df-dju 9181  df-card 9219  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-div 11151  df-nn 11492  df-2 11553  df-3 11554  df-n0 11751  df-z 11835  df-uz 12099  df-q 12203  df-rp 12245  df-xneg 12362  df-xadd 12363  df-xmul 12364  df-ioo 12597  df-ico 12599  df-icc 12600  df-fz 12748  df-fzo 12889  df-fl 13017  df-seq 13225  df-exp 13285  df-hash 13546  df-cj 14297  df-re 14298  df-im 14299  df-sqrt 14433  df-abs 14434  df-clim 14684  df-rlim 14685  df-sum 14882  df-rest 16530  df-topgen 16551  df-psmet 20224  df-xmet 20225  df-met 20226  df-bl 20227  df-mopn 20228  df-top 21191  df-topon 21208  df-bases 21243  df-cmp 21684  df-ovol 23753  df-vol 23754  df-sumge0 42213 This theorem is referenced by:  hoidmv1lelem3  42443
 Copyright terms: Public domain W3C validator