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 41288
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 6582 . . . . . . . 8 (𝜑 → (𝐷𝐾) ∈ ℝ)
87, 2ifcld 4324 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ∈ ℝ)
94, 8eqeltrd 2885 . . . . . 6 (𝜑𝑀 ∈ ℝ)
10 hoidmv1lelem2.c . . . . . . . . . . 11 (𝜑𝐶:ℕ⟶ℝ)
1110, 6ffvelrnd 6582 . . . . . . . . . 10 (𝜑 → (𝐶𝐾) ∈ ℝ)
127rexrd 10374 . . . . . . . . . 10 (𝜑 → (𝐷𝐾) ∈ ℝ*)
13 icossre 12472 . . . . . . . . . 10 (((𝐶𝐾) ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ*) → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
1411, 12, 13syl2anc 575 . . . . . . . . 9 (𝜑 → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
15 hoidmv1lelem2.s . . . . . . . . 9 (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
1614, 15sseldd 3799 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
17 hoidmv1lelem2.g . . . . . . . 8 (𝜑𝐴𝑆)
1811rexrd 10374 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐾) ∈ ℝ*)
19 icoltub 40215 . . . . . . . . . . . 12 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → 𝑆 < (𝐷𝐾))
2018, 12, 15, 19syl3anc 1483 . . . . . . . . . . 11 (𝜑𝑆 < (𝐷𝐾))
2116, 7, 20ltled 10470 . . . . . . . . . 10 (𝜑𝑆 ≤ (𝐷𝐾))
22 hoidmv1lelem2.l . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
2316, 2, 22ltled 10470 . . . . . . . . . 10 (𝜑𝑆𝐵)
2421, 23jca 503 . . . . . . . . 9 (𝜑 → (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵))
25 lemin 12241 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2616, 7, 2, 25syl3anc 1483 . . . . . . . . 9 (𝜑 → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2724, 26mpbird 248 . . . . . . . 8 (𝜑𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
281, 16, 8, 17, 27letrd 10479 . . . . . . 7 (𝜑𝐴 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
294eqcomd 2812 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) = 𝑀)
3028, 29breqtrd 4870 . . . . . 6 (𝜑𝐴𝑀)
31 min2 12239 . . . . . . . 8 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
327, 2, 31syl2anc 575 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
334, 32eqbrtrd 4866 . . . . . 6 (𝜑𝑀𝐵)
341, 2, 9, 30, 33eliccd 40210 . . . . 5 (𝜑𝑀 ∈ (𝐴[,]𝐵))
359recnd 10353 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3616recnd 10353 . . . . . . . 8 (𝜑𝑆 ∈ ℂ)
371recnd 10353 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3835, 36, 37npncand 10701 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) = (𝑀𝐴))
3938eqcomd 2812 . . . . . 6 (𝜑 → (𝑀𝐴) = ((𝑀𝑆) + (𝑆𝐴)))
409, 16resubcld 10743 . . . . . . . 8 (𝜑 → (𝑀𝑆) ∈ ℝ)
4116, 1resubcld 10743 . . . . . . . 8 (𝜑 → (𝑆𝐴) ∈ ℝ)
4240, 41readdcld 10354 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ∈ ℝ)
43 nnex 11311 . . . . . . . . . . . . 13 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ ∈ V)
45 volf 23510 . . . . . . . . . . . . . . 15 vol:dom vol⟶(0[,]+∞)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
4710ffvelrnda 6581 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
485ffvelrnda 6581 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
4916adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
5048, 49ifcld 4324 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ)
5150rexrd 10374 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*)
52 icombl 23545 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5347, 51, 52syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5446, 53ffvelrnd 6582 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
55 eqid 2806 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
5654, 55fmptd 6606 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
5744, 56sge0xrcl 41081 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ*)
58 pnfxr 10377 . . . . . . . . . . . 12 +∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
60 hoidmv1lelem2.r . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
6160rexrd 10374 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
62 nfv 2005 . . . . . . . . . . . . 13 𝑗𝜑
6348rexrd 10374 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
64 icombl 23545 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6547, 63, 64syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6646, 65ffvelrnd 6582 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
6747rexrd 10374 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
6847leidd 10879 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
69 min1 12238 . . . . . . . . . . . . . . . 16 (((𝐷𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
7048, 49, 69syl2anc 575 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
71 icossico 12461 . . . . . . . . . . . . . . 15 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
7267, 63, 68, 70, 71syl22anc 858 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
73 volss 23514 . . . . . . . . . . . . . 14 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7453, 65, 72, 73syl3anc 1483 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7562, 44, 54, 66, 74sge0lempt 41106 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
7660ltpnfd 12171 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
7757, 61, 59, 75, 76xrlelttrd 12209 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) < +∞)
7857, 59, 77xrltned 40053 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≠ +∞)
7978neneqd 2983 . . . . . . . . 9 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞)
8044, 56sge0repnf 41082 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞))
8179, 80mpbird 248 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
8240, 81readdcld 10354 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ∈ ℝ)
839adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℝ)
8448, 83ifcld 4324 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
8584rexrd 10374 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
86 icombl 23545 . . . . . . . . . . . . . 14 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8747, 85, 86syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8846, 87ffvelrnd 6582 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
89 eqid 2806 . . . . . . . . . . . 12 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
9088, 89fmptd 6606 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))):ℕ⟶(0[,]+∞))
9144, 90sge0xrcl 41081 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
92 min1 12238 . . . . . . . . . . . . . . 15 (((𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
9348, 83, 92syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
94 icossico 12461 . . . . . . . . . . . . . 14 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
9567, 63, 68, 93, 94syl22anc 858 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
96 volss 23514 . . . . . . . . . . . . 13 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9787, 65, 95, 96syl3anc 1483 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9862, 44, 88, 66, 97sge0lempt 41106 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
9991, 61, 59, 98, 76xrlelttrd 12209 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
10091, 59, 99xrltned 40053 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
101100neneqd 2983 . . . . . . . 8 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
10244, 90sge0repnf 41082 . . . . . . . 8 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
103101, 102mpbird 248 . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
104 hoidmv1lelem2.e . . . . . . . . . . 11 (𝜑𝑆𝑈)
105 hoidmv1lelem2.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
106104, 105syl6eleq 2895 . . . . . . . . . 10 (𝜑𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
107 oveq1 6881 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝑧𝐴) = (𝑆𝐴))
108 simpl 470 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑆𝑗 ∈ ℕ) → 𝑧 = 𝑆)
109108breq2d 4856 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑆))
110109, 108ifbieq2d 4304 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑆𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))
111110oveq2d 6890 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))
112111fveq2d 6412 . . . . . . . . . . . . . 14 ((𝑧 = 𝑆𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
113112mpteq2dva 4938 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
114113fveq2d 6412 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
115107, 114breq12d 4857 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
116115elrab 3559 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
117106, 116sylib 209 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
118117simprd 485 . . . . . . . 8 (𝜑 → (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
11941, 81, 40, 118leadd2dd 10927 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
120 difssd 3937 . . . . . . . . . 10 (𝜑 → (ℕ ∖ {𝐾}) ⊆ ℕ)
12162, 44, 54, 81, 120sge0ssrempt 41101 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
122 difexg 5003 . . . . . . . . . . . . . . 15 (ℕ ∈ V → (ℕ ∖ {𝐾}) ∈ V)
12343, 122ax-mp 5 . . . . . . . . . . . . . 14 (ℕ ∖ {𝐾}) ∈ V
124123a1i 11 . . . . . . . . . . . . 13 (𝜑 → (ℕ ∖ {𝐾}) ∈ V)
12545a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → vol:dom vol⟶(0[,]+∞))
126 simpl 470 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝜑)
127 eldifi 3931 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ)
128127adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ)
129126, 128, 47syl2anc 575 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ)
130128, 85syldan 581 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
131129, 130, 86syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
132125, 131ffvelrnd 6582 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
13362, 124, 132sge0xrclmpt 41124 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
13444, 88, 120sge0lessmpt 41095 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
135133, 91, 59, 134, 99xrlelttrd 12209 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
136133, 59, 135xrltned 40053 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
137136neneqd 2983 . . . . . . . . . 10 (𝜑 → ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
13862, 124, 132sge0repnfmpt 41135 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
139137, 138mpbird 248 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
1409, 11resubcld 10743 . . . . . . . . 9 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℝ)
141128, 54syldan 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
142128, 53syldan 581 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
143128, 67syldan 581 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ*)
144128, 68syldan 581 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ≤ (𝐶𝑗))
145 iftrue 4285 . . . . . . . . . . . . . . . 16 ((𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
146145adantl 469 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
14748leidd 10879 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ≤ (𝐷𝑗))
148147adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ (𝐷𝑗))
14948adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
15083adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
15149adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
152 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑆)
15320, 22jca 503 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵))
154 ltmin 12243 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
15516, 7, 2, 154syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
156153, 155mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
157156, 29breqtrd 4870 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 < 𝑀)
158157ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
159149, 151, 150, 152, 158lelttrd 10480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) < 𝑀)
160149, 150, 159ltled 10470 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑀)
161148, 160jca 503 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀))
162 lemin 12241 . . . . . . . . . . . . . . . . 17 (((𝐷𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
163149, 149, 150, 162syl3anc 1483 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
164161, 163mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
165146, 164eqbrtrd 4866 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
166 iffalse 4288 . . . . . . . . . . . . . . . 16 (¬ (𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
167166adantl 469 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
16849adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
16984adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
170 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → ¬ (𝐷𝑗) ≤ 𝑆)
17148adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
172168, 171ltnled 10469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ↔ ¬ (𝐷𝑗) ≤ 𝑆))
173170, 172mpbird 248 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < (𝐷𝑗))
174157ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
175173, 174jca 503 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀))
17683adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
177 ltmin 12243 . . . . . . . . . . . . . . . . . 18 ((𝑆 ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
178168, 171, 176, 177syl3anc 1483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
179175, 178mpbird 248 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
180168, 169, 179ltled 10470 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
181167, 180eqbrtrd 4866 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
182165, 181pm2.61dan 838 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
183128, 182syldan 581 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
184 icossico 12461 . . . . . . . . . . . 12 ((((𝐶𝑗) ∈ ℝ* ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
185143, 130, 144, 183, 184syl22anc 858 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
186 volss 23514 . . . . . . . . . . 11 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
187142, 131, 185, 186syl3anc 1483 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
18862, 124, 141, 132, 187sge0lempt 41106 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
189121, 139, 140, 188leadd2dd 10927 . . . . . . . 8 (𝜑 → ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
190 difsnid 4531 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
1916, 190syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
192191eqcomd 2812 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℕ ∖ {𝐾}) ∪ {𝐾}))
193192mpteq1d 4932 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
194193fveq2d 6412 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
195 neldifsnd 4514 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾}))
196 fveq2 6408 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → (𝐶𝑗) = (𝐶𝐾))
197 fveq2 6408 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐾 → (𝐷𝑗) = (𝐷𝐾))
198197breq1d 4854 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑆 ↔ (𝐷𝐾) ≤ 𝑆))
199198, 197ifbieq1d 4302 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))
200196, 199oveq12d 6892 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))
201200fveq2d 6412 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))))
20245a1i 11 . . . . . . . . . . . . . 14 (𝜑 → vol:dom vol⟶(0[,]+∞))
2037, 16ifcld 4324 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ)
204203rexrd 10374 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*)
205 icombl 23545 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
20611, 204, 205syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
207202, 206ffvelrnd 6582 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ (0[,]+∞))
20862, 124, 6, 195, 141, 201, 207sge0splitsn 41137 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
209 volicore 41277 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
21011, 203, 209syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
211 rexadd 12281 . . . . . . . . . . . . . 14 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
212121, 210, 211syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
213 volico 40679 . . . . . . . . . . . . . . . 16 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21411, 203, 213syl2anc 575 . . . . . . . . . . . . . . 15 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21516, 7ltnled 10469 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐷𝐾) ↔ ¬ (𝐷𝐾) ≤ 𝑆))
21620, 215mpbid 223 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐷𝐾) ≤ 𝑆)
217216iffalsed 4290 . . . . . . . . . . . . . . . . 17 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) = 𝑆)
218217breq2d 4856 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ↔ (𝐶𝐾) < 𝑆))
219218ifbid 4301 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
220217oveq1d 6889 . . . . . . . . . . . . . . . . 17 (𝜑 → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
221220adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐶𝐾) < 𝑆) → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
222217, 204eqeltrrd 2886 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ∈ ℝ*)
223222adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ*)
22418adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ*)
225 simpr 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ¬ (𝐶𝐾) < 𝑆)
22616adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ)
22711adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ)
228226, 227lenltd 10468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 ≤ (𝐶𝐾) ↔ ¬ (𝐶𝐾) < 𝑆))
229225, 228mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ≤ (𝐶𝐾))
230 icogelb 12443 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → (𝐶𝐾) ≤ 𝑆)
23118, 12, 15, 230syl3anc 1483 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶𝐾) ≤ 𝑆)
232231adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ≤ 𝑆)
233223, 224, 229, 232xrletrid 12204 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 = (𝐶𝐾))
234233oveq1d 6889 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 − (𝐶𝐾)) = ((𝐶𝐾) − (𝐶𝐾)))
235227recnd 10353 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℂ)
236235subidd 10665 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ((𝐶𝐾) − (𝐶𝐾)) = 0)
237234, 236eqtr2d 2841 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 0 = (𝑆 − (𝐶𝐾)))
238221, 237ifeqda 4314 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = (𝑆 − (𝐶𝐾)))
239214, 219, 2383eqtrd 2844 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = (𝑆 − (𝐶𝐾)))
240239oveq2d 6890 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))))
241121recnd 10353 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℂ)
24211recnd 10353 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐾) ∈ ℂ)
24336, 242subcld 10677 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 − (𝐶𝐾)) ∈ ℂ)
244241, 243addcomd 10523 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
245212, 240, 2443eqtrd 2844 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
246194, 208, 2453eqtrd 2844 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
247246oveq2d 6890 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
24840recnd 10353 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑆) ∈ ℂ)
249248, 243, 241addassd 10347 . . . . . . . . . . 11 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
250249eqcomd 2812 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))) = (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
25135, 36, 242npncand 10701 . . . . . . . . . . 11 (𝜑 → ((𝑀𝑆) + (𝑆 − (𝐶𝐾))) = (𝑀 − (𝐶𝐾)))
252251oveq1d 6889 . . . . . . . . . 10 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
253247, 250, 2523eqtrd 2844 . . . . . . . . 9 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
254192mpteq1d 4932 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
255254fveq2d 6412 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
256197breq1d 4854 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑀 ↔ (𝐷𝐾) ≤ 𝑀))
257256, 197ifbieq1d 4302 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) = if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
258196, 257oveq12d 6892 . . . . . . . . . . . 12 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))
259258fveq2d 6412 . . . . . . . . . . 11 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))))
2607, 9ifcld 4324 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ)
261260rexrd 10374 . . . . . . . . . . . . 13 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*)
262 icombl 23545 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
26311, 261, 262syl2anc 575 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
264202, 263ffvelrnd 6582 . . . . . . . . . . 11 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ (0[,]+∞))
26562, 124, 6, 195, 132, 259, 264sge0splitsn 41137 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
266 volicore 41277 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
26711, 260, 266syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
268 rexadd 12281 . . . . . . . . . . . 12 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
269139, 267, 268syl2anc 575 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
270 volico 40679 . . . . . . . . . . . . . 14 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27111, 260, 270syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27220, 157jca 503 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀))
273 ltmin 12243 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
27416, 7, 9, 273syl3anc 1483 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
275272, 274mpbird 248 . . . . . . . . . . . . . . 15 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
27611, 16, 260, 231, 275lelttrd 10480 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
277276iftrued 4287 . . . . . . . . . . . . 13 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0) = (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)))
278 iftrue 4285 . . . . . . . . . . . . . . . . 17 ((𝐷𝐾) ≤ 𝑀 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
279278adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
28012adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ∈ ℝ*)
2819rexrd 10374 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ*)
282281adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ∈ ℝ*)
283 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ≤ 𝑀)
284 min1 12238 . . . . . . . . . . . . . . . . . . . 20 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2857, 2, 284syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2864, 285eqbrtrd 4866 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ≤ (𝐷𝐾))
287286adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷𝐾))
288280, 282, 283, 287xrletrid 12204 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) = 𝑀)
289279, 288eqtrd 2840 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
290 simpr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → ¬ (𝐷𝐾) ≤ 𝑀)
291290iffalsed 4290 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
292289, 291pm2.61dan 838 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
293292oveq1d 6889 . . . . . . . . . . . . 13 (𝜑 → (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)) = (𝑀 − (𝐶𝐾)))
294271, 277, 2933eqtrd 2844 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = (𝑀 − (𝐶𝐾)))
295294oveq2d 6890 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))))
296139recnd 10353 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℂ)
29735, 242subcld 10677 . . . . . . . . . . . 12 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℂ)
298296, 297addcomd 10523 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
299269, 295, 2983eqtrd 2844 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
300255, 265, 2993eqtrd 2844 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
301253, 300breq12d 4857 . . . . . . . 8 (𝜑 → (((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))))
302189, 301mpbird 248 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30342, 82, 103, 119, 302letrd 10479 . . . . . 6 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30439, 303eqbrtrd 4866 . . . . 5 (𝜑 → (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30534, 304jca 503 . . . 4 (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
306 oveq1 6881 . . . . . 6 (𝑧 = 𝑀 → (𝑧𝐴) = (𝑀𝐴))
307 breq2 4848 . . . . . . . . . . 11 (𝑧 = 𝑀 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑀))
308 id 22 . . . . . . . . . . 11 (𝑧 = 𝑀𝑧 = 𝑀)
309307, 308ifbieq2d 4304 . . . . . . . . . 10 (𝑧 = 𝑀 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
310309oveq2d 6890 . . . . . . . . 9 (𝑧 = 𝑀 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
311310fveq2d 6412 . . . . . . . 8 (𝑧 = 𝑀 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
312311mpteq2dv 4939 . . . . . . 7 (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
313312fveq2d 6412 . . . . . 6 (𝑧 = 𝑀 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
314306, 313breq12d 4857 . . . . 5 (𝑧 = 𝑀 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
315314elrab 3559 . . . 4 (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
316305, 315sylibr 225 . . 3 (𝜑𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
317316, 105syl6eleqr 2896 . 2 (𝜑𝑀𝑈)
318272simprd 485 . 2 (𝜑𝑆 < 𝑀)
319 breq2 4848 . . 3 (𝑢 = 𝑀 → (𝑆 < 𝑢𝑆 < 𝑀))
320319rspcev 3502 . 2 ((𝑀𝑈𝑆 < 𝑀) → ∃𝑢𝑈 𝑆 < 𝑢)
321317, 318, 320syl2anc 575 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wrex 3097  {crab 3100  Vcvv 3391  cdif 3766  cun 3767  wss 3769  ifcif 4279  {csn 4370   class class class wbr 4844  cmpt 4923  dom cdm 5311  wf 6097  cfv 6101  (class class class)co 6874  cr 10220  0cc0 10221   + caddc 10224  +∞cpnf 10356  *cxr 10358   < clt 10359  cle 10360  cmin 10551  cn 11305   +𝑒 cxad 12160  [,)cico 12395  [,]cicc 12396  volcvol 23444  Σ^csumge0 41058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-n0 11560  df-z 11644  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioo 12397  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817  df-seq 13025  df-exp 13084  df-hash 13338  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-clim 14442  df-rlim 14443  df-sum 14640  df-rest 16288  df-topgen 16309  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-top 20912  df-topon 20929  df-bases 20964  df-cmp 21404  df-ovol 23445  df-vol 23446  df-sumge0 41059
This theorem is referenced by:  hoidmv1lelem3  41289
  Copyright terms: Public domain W3C validator