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 41127
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 6400 . . . . . . . 8 (𝜑 → (𝐷𝐾) ∈ ℝ)
87, 2ifcld 4164 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ∈ ℝ)
94, 8eqeltrd 2730 . . . . . 6 (𝜑𝑀 ∈ ℝ)
10 hoidmv1lelem2.c . . . . . . . . . . 11 (𝜑𝐶:ℕ⟶ℝ)
1110, 6ffvelrnd 6400 . . . . . . . . . 10 (𝜑 → (𝐶𝐾) ∈ ℝ)
127rexrd 10127 . . . . . . . . . 10 (𝜑 → (𝐷𝐾) ∈ ℝ*)
13 icossre 12292 . . . . . . . . . 10 (((𝐶𝐾) ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ*) → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
1411, 12, 13syl2anc 694 . . . . . . . . 9 (𝜑 → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
15 hoidmv1lelem2.s . . . . . . . . 9 (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
1614, 15sseldd 3637 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
17 hoidmv1lelem2.g . . . . . . . 8 (𝜑𝐴𝑆)
1811rexrd 10127 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐾) ∈ ℝ*)
19 icoltub 40050 . . . . . . . . . . . 12 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → 𝑆 < (𝐷𝐾))
2018, 12, 15, 19syl3anc 1366 . . . . . . . . . . 11 (𝜑𝑆 < (𝐷𝐾))
2116, 7, 20ltled 10223 . . . . . . . . . 10 (𝜑𝑆 ≤ (𝐷𝐾))
22 hoidmv1lelem2.l . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
2316, 2, 22ltled 10223 . . . . . . . . . 10 (𝜑𝑆𝐵)
2421, 23jca 553 . . . . . . . . 9 (𝜑 → (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵))
25 lemin 12061 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2616, 7, 2, 25syl3anc 1366 . . . . . . . . 9 (𝜑 → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2724, 26mpbird 247 . . . . . . . 8 (𝜑𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
281, 16, 8, 17, 27letrd 10232 . . . . . . 7 (𝜑𝐴 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
294eqcomd 2657 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) = 𝑀)
3028, 29breqtrd 4711 . . . . . 6 (𝜑𝐴𝑀)
31 min2 12059 . . . . . . . 8 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
327, 2, 31syl2anc 694 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
334, 32eqbrtrd 4707 . . . . . 6 (𝜑𝑀𝐵)
341, 2, 9, 30, 33eliccd 40044 . . . . 5 (𝜑𝑀 ∈ (𝐴[,]𝐵))
359recnd 10106 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3616recnd 10106 . . . . . . . 8 (𝜑𝑆 ∈ ℂ)
371recnd 10106 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3835, 36, 37npncand 10454 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) = (𝑀𝐴))
3938eqcomd 2657 . . . . . 6 (𝜑 → (𝑀𝐴) = ((𝑀𝑆) + (𝑆𝐴)))
409, 16resubcld 10496 . . . . . . . 8 (𝜑 → (𝑀𝑆) ∈ ℝ)
4116, 1resubcld 10496 . . . . . . . 8 (𝜑 → (𝑆𝐴) ∈ ℝ)
4240, 41readdcld 10107 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ∈ ℝ)
43 nnex 11064 . . . . . . . . . . . . 13 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ ∈ V)
45 volf 23343 . . . . . . . . . . . . . . 15 vol:dom vol⟶(0[,]+∞)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
4710ffvelrnda 6399 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
485ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
4916adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
5048, 49ifcld 4164 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ)
5150rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*)
52 icombl 23378 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5347, 51, 52syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5446, 53ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
55 eqid 2651 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
5654, 55fmptd 6425 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
5744, 56sge0xrcl 40920 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ*)
58 pnfxr 10130 . . . . . . . . . . . 12 +∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
60 hoidmv1lelem2.r . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
6160rexrd 10127 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
62 nfv 1883 . . . . . . . . . . . . 13 𝑗𝜑
6348rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
64 icombl 23378 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6547, 63, 64syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6646, 65ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
6747rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
6847leidd 10632 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
69 min1 12058 . . . . . . . . . . . . . . . 16 (((𝐷𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
7048, 49, 69syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
71 icossico 12281 . . . . . . . . . . . . . . 15 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
7267, 63, 68, 70, 71syl22anc 1367 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
73 volss 23347 . . . . . . . . . . . . . 14 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7453, 65, 72, 73syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7562, 44, 54, 66, 74sge0lempt 40945 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
7660ltpnfd 11993 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
7757, 61, 59, 75, 76xrlelttrd 12029 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) < +∞)
7857, 59, 77xrltned 39886 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≠ +∞)
7978neneqd 2828 . . . . . . . . 9 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞)
8044, 56sge0repnf 40921 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞))
8179, 80mpbird 247 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
8240, 81readdcld 10107 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ∈ ℝ)
839adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℝ)
8448, 83ifcld 4164 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
8584rexrd 10127 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
86 icombl 23378 . . . . . . . . . . . . . 14 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8747, 85, 86syl2anc 694 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8846, 87ffvelrnd 6400 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
89 eqid 2651 . . . . . . . . . . . 12 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
9088, 89fmptd 6425 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))):ℕ⟶(0[,]+∞))
9144, 90sge0xrcl 40920 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
92 min1 12058 . . . . . . . . . . . . . . 15 (((𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
9348, 83, 92syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
94 icossico 12281 . . . . . . . . . . . . . 14 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
9567, 63, 68, 93, 94syl22anc 1367 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
96 volss 23347 . . . . . . . . . . . . 13 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9787, 65, 95, 96syl3anc 1366 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9862, 44, 88, 66, 97sge0lempt 40945 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
9991, 61, 59, 98, 76xrlelttrd 12029 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
10091, 59, 99xrltned 39886 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
101100neneqd 2828 . . . . . . . 8 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
10244, 90sge0repnf 40921 . . . . . . . 8 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
103101, 102mpbird 247 . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
104 hoidmv1lelem2.e . . . . . . . . . . 11 (𝜑𝑆𝑈)
105 hoidmv1lelem2.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
106104, 105syl6eleq 2740 . . . . . . . . . 10 (𝜑𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
107 oveq1 6697 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝑧𝐴) = (𝑆𝐴))
108 simpl 472 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑆𝑗 ∈ ℕ) → 𝑧 = 𝑆)
109108breq2d 4697 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑆))
110109, 108ifbieq2d 4144 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑆𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))
111110oveq2d 6706 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))
112111fveq2d 6233 . . . . . . . . . . . . . 14 ((𝑧 = 𝑆𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
113112mpteq2dva 4777 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
114113fveq2d 6233 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
115107, 114breq12d 4698 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
116115elrab 3396 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
117106, 116sylib 208 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
118117simprd 478 . . . . . . . 8 (𝜑 → (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
11941, 81, 40, 118leadd2dd 10680 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
120 difssd 3771 . . . . . . . . . 10 (𝜑 → (ℕ ∖ {𝐾}) ⊆ ℕ)
12162, 44, 54, 81, 120sge0ssrempt 40940 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
122 difexg 4841 . . . . . . . . . . . . . . 15 (ℕ ∈ V → (ℕ ∖ {𝐾}) ∈ V)
12343, 122ax-mp 5 . . . . . . . . . . . . . 14 (ℕ ∖ {𝐾}) ∈ V
124123a1i 11 . . . . . . . . . . . . 13 (𝜑 → (ℕ ∖ {𝐾}) ∈ V)
12545a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → vol:dom vol⟶(0[,]+∞))
126 simpl 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝜑)
127 eldifi 3765 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ)
128127adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ)
129126, 128, 47syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ)
130128, 85syldan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
131129, 130, 86syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
132125, 131ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
13362, 124, 132sge0xrclmpt 40963 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
13444, 88, 120sge0lessmpt 40934 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
135133, 91, 59, 134, 99xrlelttrd 12029 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
136133, 59, 135xrltned 39886 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
137136neneqd 2828 . . . . . . . . . 10 (𝜑 → ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
13862, 124, 132sge0repnfmpt 40974 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
139137, 138mpbird 247 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
1409, 11resubcld 10496 . . . . . . . . 9 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℝ)
141128, 54syldan 486 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
142128, 53syldan 486 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
143128, 67syldan 486 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ*)
144128, 68syldan 486 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ≤ (𝐶𝑗))
145 iftrue 4125 . . . . . . . . . . . . . . . 16 ((𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
146145adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
14748leidd 10632 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ≤ (𝐷𝑗))
148147adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ (𝐷𝑗))
14948adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
15083adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
15149adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
152 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑆)
15320, 22jca 553 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵))
154 ltmin 12063 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
15516, 7, 2, 154syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
156153, 155mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
157156, 29breqtrd 4711 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 < 𝑀)
158157ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
159149, 151, 150, 152, 158lelttrd 10233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) < 𝑀)
160149, 150, 159ltled 10223 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑀)
161148, 160jca 553 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀))
162 lemin 12061 . . . . . . . . . . . . . . . . 17 (((𝐷𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
163149, 149, 150, 162syl3anc 1366 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
164161, 163mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
165146, 164eqbrtrd 4707 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
166 iffalse 4128 . . . . . . . . . . . . . . . 16 (¬ (𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
167166adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
16849adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
16984adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
170 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → ¬ (𝐷𝑗) ≤ 𝑆)
17148adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
172168, 171ltnled 10222 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ↔ ¬ (𝐷𝑗) ≤ 𝑆))
173170, 172mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < (𝐷𝑗))
174157ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
175173, 174jca 553 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀))
17683adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
177 ltmin 12063 . . . . . . . . . . . . . . . . . 18 ((𝑆 ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
178168, 171, 176, 177syl3anc 1366 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
179175, 178mpbird 247 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
180168, 169, 179ltled 10223 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
181167, 180eqbrtrd 4707 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
182165, 181pm2.61dan 849 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
183128, 182syldan 486 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
184 icossico 12281 . . . . . . . . . . . 12 ((((𝐶𝑗) ∈ ℝ* ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
185143, 130, 144, 183, 184syl22anc 1367 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
186 volss 23347 . . . . . . . . . . 11 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
187142, 131, 185, 186syl3anc 1366 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
18862, 124, 141, 132, 187sge0lempt 40945 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
189121, 139, 140, 188leadd2dd 10680 . . . . . . . 8 (𝜑 → ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
190 difsnid 4373 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
1916, 190syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
192191eqcomd 2657 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℕ ∖ {𝐾}) ∪ {𝐾}))
193192mpteq1d 4771 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
194193fveq2d 6233 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
195 neldifsnd 4355 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾}))
196 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → (𝐶𝑗) = (𝐶𝐾))
197 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐾 → (𝐷𝑗) = (𝐷𝐾))
198197breq1d 4695 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑆 ↔ (𝐷𝐾) ≤ 𝑆))
199198, 197ifbieq1d 4142 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))
200196, 199oveq12d 6708 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))
201200fveq2d 6233 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))))
20245a1i 11 . . . . . . . . . . . . . 14 (𝜑 → vol:dom vol⟶(0[,]+∞))
2037, 16ifcld 4164 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ)
204203rexrd 10127 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*)
205 icombl 23378 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
20611, 204, 205syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
207202, 206ffvelrnd 6400 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ (0[,]+∞))
20862, 124, 6, 195, 141, 201, 207sge0splitsn 40976 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
209 volicore 41116 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
21011, 203, 209syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
211 rexadd 12101 . . . . . . . . . . . . . 14 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
212121, 210, 211syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
213 volico 40518 . . . . . . . . . . . . . . . 16 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21411, 203, 213syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21516, 7ltnled 10222 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐷𝐾) ↔ ¬ (𝐷𝐾) ≤ 𝑆))
21620, 215mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐷𝐾) ≤ 𝑆)
217216iffalsed 4130 . . . . . . . . . . . . . . . . 17 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) = 𝑆)
218217breq2d 4697 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ↔ (𝐶𝐾) < 𝑆))
219218ifbid 4141 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
220217oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
221220adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐶𝐾) < 𝑆) → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
222217, 204eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ∈ ℝ*)
223222adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ*)
22418adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ*)
225 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ¬ (𝐶𝐾) < 𝑆)
22616adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ)
22711adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ)
228226, 227lenltd 10221 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 ≤ (𝐶𝐾) ↔ ¬ (𝐶𝐾) < 𝑆))
229225, 228mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ≤ (𝐶𝐾))
230 icogelb 12263 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → (𝐶𝐾) ≤ 𝑆)
23118, 12, 15, 230syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶𝐾) ≤ 𝑆)
232231adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ≤ 𝑆)
233223, 224, 229, 232xrletrid 12024 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 = (𝐶𝐾))
234233oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 − (𝐶𝐾)) = ((𝐶𝐾) − (𝐶𝐾)))
235227recnd 10106 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℂ)
236235subidd 10418 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ((𝐶𝐾) − (𝐶𝐾)) = 0)
237234, 236eqtr2d 2686 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 0 = (𝑆 − (𝐶𝐾)))
238221, 237ifeqda 4154 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = (𝑆 − (𝐶𝐾)))
239214, 219, 2383eqtrd 2689 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = (𝑆 − (𝐶𝐾)))
240239oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))))
241121recnd 10106 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℂ)
24211recnd 10106 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐾) ∈ ℂ)
24336, 242subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 − (𝐶𝐾)) ∈ ℂ)
244241, 243addcomd 10276 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
245212, 240, 2443eqtrd 2689 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
246194, 208, 2453eqtrd 2689 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
247246oveq2d 6706 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
24840recnd 10106 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑆) ∈ ℂ)
249248, 243, 241addassd 10100 . . . . . . . . . . 11 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
250249eqcomd 2657 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))) = (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
25135, 36, 242npncand 10454 . . . . . . . . . . 11 (𝜑 → ((𝑀𝑆) + (𝑆 − (𝐶𝐾))) = (𝑀 − (𝐶𝐾)))
252251oveq1d 6705 . . . . . . . . . 10 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
253247, 250, 2523eqtrd 2689 . . . . . . . . 9 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
254192mpteq1d 4771 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
255254fveq2d 6233 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
256197breq1d 4695 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑀 ↔ (𝐷𝐾) ≤ 𝑀))
257256, 197ifbieq1d 4142 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) = if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
258196, 257oveq12d 6708 . . . . . . . . . . . 12 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))
259258fveq2d 6233 . . . . . . . . . . 11 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))))
2607, 9ifcld 4164 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ)
261260rexrd 10127 . . . . . . . . . . . . 13 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*)
262 icombl 23378 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
26311, 261, 262syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
264202, 263ffvelrnd 6400 . . . . . . . . . . 11 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ (0[,]+∞))
26562, 124, 6, 195, 132, 259, 264sge0splitsn 40976 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
266 volicore 41116 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
26711, 260, 266syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
268 rexadd 12101 . . . . . . . . . . . 12 (((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ∧ (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
269139, 267, 268syl2anc 694 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
270 volico 40518 . . . . . . . . . . . . . 14 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27111, 260, 270syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0))
27220, 157jca 553 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀))
273 ltmin 12063 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
27416, 7, 9, 273syl3anc 1366 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
275272, 274mpbird 247 . . . . . . . . . . . . . . 15 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
27611, 16, 260, 231, 275lelttrd 10233 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
277276iftrued 4127 . . . . . . . . . . . . 13 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0) = (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)))
278 iftrue 4125 . . . . . . . . . . . . . . . . 17 ((𝐷𝐾) ≤ 𝑀 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
279278adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
28012adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ∈ ℝ*)
2819rexrd 10127 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ*)
282281adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ∈ ℝ*)
283 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ≤ 𝑀)
284 min1 12058 . . . . . . . . . . . . . . . . . . . 20 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2857, 2, 284syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2864, 285eqbrtrd 4707 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ≤ (𝐷𝐾))
287286adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷𝐾))
288280, 282, 283, 287xrletrid 12024 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) = 𝑀)
289279, 288eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
290 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → ¬ (𝐷𝐾) ≤ 𝑀)
291290iffalsed 4130 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
292289, 291pm2.61dan 849 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
293292oveq1d 6705 . . . . . . . . . . . . 13 (𝜑 → (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)) = (𝑀 − (𝐶𝐾)))
294271, 277, 2933eqtrd 2689 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = (𝑀 − (𝐶𝐾)))
295294oveq2d 6706 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))))
296139recnd 10106 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℂ)
29735, 242subcld 10430 . . . . . . . . . . . 12 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℂ)
298296, 297addcomd 10276 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
299269, 295, 2983eqtrd 2689 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
300255, 265, 2993eqtrd 2689 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
301253, 300breq12d 4698 . . . . . . . 8 (𝜑 → (((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))))
302189, 301mpbird 247 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30342, 82, 103, 119, 302letrd 10232 . . . . . 6 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30439, 303eqbrtrd 4707 . . . . 5 (𝜑 → (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30534, 304jca 553 . . . 4 (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
306 oveq1 6697 . . . . . 6 (𝑧 = 𝑀 → (𝑧𝐴) = (𝑀𝐴))
307 breq2 4689 . . . . . . . . . . 11 (𝑧 = 𝑀 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑀))
308 id 22 . . . . . . . . . . 11 (𝑧 = 𝑀𝑧 = 𝑀)
309307, 308ifbieq2d 4144 . . . . . . . . . 10 (𝑧 = 𝑀 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
310309oveq2d 6706 . . . . . . . . 9 (𝑧 = 𝑀 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
311310fveq2d 6233 . . . . . . . 8 (𝑧 = 𝑀 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
312311mpteq2dv 4778 . . . . . . 7 (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
313312fveq2d 6233 . . . . . 6 (𝑧 = 𝑀 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
314306, 313breq12d 4698 . . . . 5 (𝑧 = 𝑀 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
315314elrab 3396 . . . 4 (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
316305, 315sylibr 224 . . 3 (𝜑𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
317316, 105syl6eleqr 2741 . 2 (𝜑𝑀𝑈)
318272simprd 478 . 2 (𝜑𝑆 < 𝑀)
319 breq2 4689 . . 3 (𝑢 = 𝑀 → (𝑆 < 𝑢𝑆 < 𝑀))
320319rspcev 3340 . 2 ((𝑀𝑈𝑆 < 𝑀) → ∃𝑢𝑈 𝑆 < 𝑢)
321317, 318, 320syl2anc 694 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  wss 3607  ifcif 4119  {csn 4210   class class class wbr 4685  cmpt 4762  dom cdm 5143  wf 5922  cfv 5926  (class class class)co 6690  cr 9973  0cc0 9974   + caddc 9977  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113  cmin 10304  cn 11058   +𝑒 cxad 11982  [,)cico 12215  [,]cicc 12216  volcvol 23278  Σ^csumge0 40897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280  df-sumge0 40898
This theorem is referenced by:  hoidmv1lelem3  41128
  Copyright terms: Public domain W3C validator