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 44130
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 6962 . . . . . . . 8 (𝜑 → (𝐷𝐾) ∈ ℝ)
87, 2ifcld 4505 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ∈ ℝ)
94, 8eqeltrd 2839 . . . . . 6 (𝜑𝑀 ∈ ℝ)
10 hoidmv1lelem2.c . . . . . . . . . . 11 (𝜑𝐶:ℕ⟶ℝ)
1110, 6ffvelrnd 6962 . . . . . . . . . 10 (𝜑 → (𝐶𝐾) ∈ ℝ)
127rexrd 11025 . . . . . . . . . 10 (𝜑 → (𝐷𝐾) ∈ ℝ*)
13 icossre 13160 . . . . . . . . . 10 (((𝐶𝐾) ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ*) → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
1411, 12, 13syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐶𝐾)[,)(𝐷𝐾)) ⊆ ℝ)
15 hoidmv1lelem2.s . . . . . . . . 9 (𝜑𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾)))
1614, 15sseldd 3922 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
17 hoidmv1lelem2.g . . . . . . . 8 (𝜑𝐴𝑆)
1811rexrd 11025 . . . . . . . . . . . 12 (𝜑 → (𝐶𝐾) ∈ ℝ*)
19 icoltub 43046 . . . . . . . . . . . 12 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → 𝑆 < (𝐷𝐾))
2018, 12, 15, 19syl3anc 1370 . . . . . . . . . . 11 (𝜑𝑆 < (𝐷𝐾))
2116, 7, 20ltled 11123 . . . . . . . . . 10 (𝜑𝑆 ≤ (𝐷𝐾))
22 hoidmv1lelem2.l . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
2316, 2, 22ltled 11123 . . . . . . . . . 10 (𝜑𝑆𝐵)
2421, 23jca 512 . . . . . . . . 9 (𝜑 → (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵))
25 lemin 12926 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2616, 7, 2, 25syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 ≤ (𝐷𝐾) ∧ 𝑆𝐵)))
2724, 26mpbird 256 . . . . . . . 8 (𝜑𝑆 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
281, 16, 8, 17, 27letrd 11132 . . . . . . 7 (𝜑𝐴 ≤ if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
294eqcomd 2744 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) = 𝑀)
3028, 29breqtrd 5100 . . . . . 6 (𝜑𝐴𝑀)
31 min2 12924 . . . . . . . 8 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
327, 2, 31syl2anc 584 . . . . . . 7 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ 𝐵)
334, 32eqbrtrd 5096 . . . . . 6 (𝜑𝑀𝐵)
341, 2, 9, 30, 33eliccd 43042 . . . . 5 (𝜑𝑀 ∈ (𝐴[,]𝐵))
359recnd 11003 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3616recnd 11003 . . . . . . . 8 (𝜑𝑆 ∈ ℂ)
371recnd 11003 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3835, 36, 37npncand 11356 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) = (𝑀𝐴))
3938eqcomd 2744 . . . . . 6 (𝜑 → (𝑀𝐴) = ((𝑀𝑆) + (𝑆𝐴)))
409, 16resubcld 11403 . . . . . . . 8 (𝜑 → (𝑀𝑆) ∈ ℝ)
4116, 1resubcld 11403 . . . . . . . 8 (𝜑 → (𝑆𝐴) ∈ ℝ)
4240, 41readdcld 11004 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ∈ ℝ)
43 nnex 11979 . . . . . . . . . . . . 13 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ ∈ V)
45 volf 24693 . . . . . . . . . . . . . . 15 vol:dom vol⟶(0[,]+∞)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
4710ffvelrnda 6961 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
485ffvelrnda 6961 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
4916adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
5048, 49ifcld 4505 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ)
5150rexrd 11025 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*)
52 icombl 24728 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5347, 51, 52syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol)
5446, 53ffvelrnd 6962 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ∈ (0[,]+∞))
55 eqid 2738 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
5654, 55fmptd 6988 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
5744, 56sge0xrcl 43923 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ*)
58 pnfxr 11029 . . . . . . . . . . . 12 +∞ ∈ ℝ*
5958a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
60 hoidmv1lelem2.r . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
6160rexrd 11025 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
62 nfv 1917 . . . . . . . . . . . . 13 𝑗𝜑
6348rexrd 11025 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
64 icombl 24728 . . . . . . . . . . . . . . 15 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6547, 63, 64syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
6646, 65ffvelrnd 6962 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
6747rexrd 11025 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
6847leidd 11541 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
69 min1 12923 . . . . . . . . . . . . . . . 16 (((𝐷𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
7048, 49, 69syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))
71 icossico 13149 . . . . . . . . . . . . . . 15 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
7267, 63, 68, 70, 71syl22anc 836 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
73 volss 24697 . . . . . . . . . . . . . 14 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7453, 65, 72, 73syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
7562, 44, 54, 66, 74sge0lempt 43948 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
7660ltpnfd 12857 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
7757, 61, 59, 75, 76xrlelttrd 12894 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) < +∞)
7857, 59, 77xrltned 42896 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≠ +∞)
7978neneqd 2948 . . . . . . . . 9 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞)
8044, 56sge0repnf 43924 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = +∞))
8179, 80mpbird 256 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
8240, 81readdcld 11004 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ∈ ℝ)
839adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → 𝑀 ∈ ℝ)
8448, 83ifcld 4505 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
8584rexrd 11025 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
86 icombl 24728 . . . . . . . . . . . . . 14 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8747, 85, 86syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
8846, 87ffvelrnd 6962 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
89 eqid 2738 . . . . . . . . . . . 12 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
9088, 89fmptd 6988 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))):ℕ⟶(0[,]+∞))
9144, 90sge0xrcl 43923 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
92 min1 12923 . . . . . . . . . . . . . . 15 (((𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
9348, 83, 92syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))
94 icossico 13149 . . . . . . . . . . . . . 14 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
9567, 63, 68, 93, 94syl22anc 836 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
96 volss 24697 . . . . . . . . . . . . 13 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9787, 65, 95, 96syl3anc 1370 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
9862, 44, 88, 66, 97sge0lempt 43948 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
9991, 61, 59, 98, 76xrlelttrd 12894 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
10091, 59, 99xrltned 42896 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
101100neneqd 2948 . . . . . . . 8 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
10244, 90sge0repnf 43924 . . . . . . . 8 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
103101, 102mpbird 256 . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
104 hoidmv1lelem2.e . . . . . . . . . . 11 (𝜑𝑆𝑈)
105 hoidmv1lelem2.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
106104, 105eleqtrdi 2849 . . . . . . . . . 10 (𝜑𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
107 oveq1 7282 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝑧𝐴) = (𝑆𝐴))
108 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑆𝑗 ∈ ℕ) → 𝑧 = 𝑆)
109108breq2d 5086 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑆))
110109, 108ifbieq2d 4485 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑆𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))
111110oveq2d 7291 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑆𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))
112111fveq2d 6778 . . . . . . . . . . . . . 14 ((𝑧 = 𝑆𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))
113112mpteq2dva 5174 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
114113fveq2d 6778 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
115107, 114breq12d 5087 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
116115elrab 3624 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
117106, 116sylib 217 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
118117simprd 496 . . . . . . . 8 (𝜑 → (𝑆𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
11941, 81, 40, 118leadd2dd 11590 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
120 difssd 4067 . . . . . . . . . 10 (𝜑 → (ℕ ∖ {𝐾}) ⊆ ℕ)
12162, 44, 54, 81, 120sge0ssrempt 43943 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℝ)
122 difexg 5251 . . . . . . . . . . . . . . 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 4061 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℕ ∖ {𝐾}) → 𝑗 ∈ ℕ)
128127adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → 𝑗 ∈ ℕ)
129126, 128, 47syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (𝐶𝑗) ∈ ℝ)
130128, 85syldan 591 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*)
131129, 130, 86syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol)
132125, 131ffvelrnd 6962 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) ∈ (0[,]+∞))
13362, 124, 132sge0xrclmpt 43966 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ*)
13444, 88, 120sge0lessmpt 43937 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
135133, 91, 59, 134, 99xrlelttrd 12894 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) < +∞)
136133, 59, 135xrltned 42896 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ≠ +∞)
137136neneqd 2948 . . . . . . . . . 10 (𝜑 → ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞)
13862, 124, 132sge0repnfmpt 43977 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = +∞))
139137, 138mpbird 256 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℝ)
1409, 11resubcld 11403 . . . . . . . . 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 4465 . . . . . . . . . . . . . . . 16 ((𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
146145adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = (𝐷𝑗))
14748leidd 11541 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ≤ (𝐷𝑗))
148147adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ (𝐷𝑗))
14948adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
15083adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
15149adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
152 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑆)
15320, 22jca 512 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵))
154 ltmin 12928 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
15516, 7, 2, 154syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝐵)))
156153, 155mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵))
157156, 29breqtrd 5100 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 < 𝑀)
158157ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
159149, 151, 150, 152, 158lelttrd 11133 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) < 𝑀)
160149, 150, 159ltled 11123 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ 𝑀)
161148, 160jca 512 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀))
162 lemin 12926 . . . . . . . . . . . . . . . . 17 (((𝐷𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
163149, 149, 150, 162syl3anc 1370 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → ((𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ ((𝐷𝑗) ≤ (𝐷𝑗) ∧ (𝐷𝑗) ≤ 𝑀)))
164161, 163mpbird 256 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
165146, 164eqbrtrd 5096 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
166 iffalse 4468 . . . . . . . . . . . . . . . 16 (¬ (𝐷𝑗) ≤ 𝑆 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
167166adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = 𝑆)
16849adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ∈ ℝ)
16984adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ)
170 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → ¬ (𝐷𝑗) ≤ 𝑆)
17148adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝐷𝑗) ∈ ℝ)
172168, 171ltnled 11122 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ↔ ¬ (𝐷𝑗) ≤ 𝑆))
173170, 172mpbird 256 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < (𝐷𝑗))
174157ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < 𝑀)
175173, 174jca 512 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀))
17683adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑀 ∈ ℝ)
177 ltmin 12928 . . . . . . . . . . . . . . . . . 18 ((𝑆 ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
178168, 171, 176, 177syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → (𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ↔ (𝑆 < (𝐷𝑗) ∧ 𝑆 < 𝑀)))
179175, 178mpbird 256 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 < if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
180168, 169, 179ltled 11123 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → 𝑆 ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
181167, 180eqbrtrd 5096 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ¬ (𝐷𝑗) ≤ 𝑆) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
182165, 181pm2.61dan 810 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
183128, 182syldan 591 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
184 icossico 13149 . . . . . . . . . . . 12 ((((𝐶𝑗) ∈ ℝ* ∧ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) ≤ if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
185143, 130, 144, 183, 184syl22anc 836 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
186 volss 24697 . . . . . . . . . . 11 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) ⊆ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
187142, 131, 185, 186syl3anc 1370 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℕ ∖ {𝐾})) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
18862, 124, 141, 132, 187sge0lempt 43948 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ≤ (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
189121, 139, 140, 188leadd2dd 11590 . . . . . . . 8 (𝜑 → ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
190 difsnid 4743 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
1916, 190syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((ℕ ∖ {𝐾}) ∪ {𝐾}) = ℕ)
192191eqcomd 2744 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℕ ∖ {𝐾}) ∪ {𝐾}))
193192mpteq1d 5169 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))
194193fveq2d 6778 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))
195 neldifsnd 4726 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐾 ∈ (ℕ ∖ {𝐾}))
196 fveq2 6774 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → (𝐶𝑗) = (𝐶𝐾))
197 fveq2 6774 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐾 → (𝐷𝑗) = (𝐷𝐾))
198197breq1d 5084 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑆 ↔ (𝐷𝐾) ≤ 𝑆))
199198, 197ifbieq1d 4483 . . . . . . . . . . . . . . 15 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆) = if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))
200196, 199oveq12d 7293 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))
201200fveq2d 6778 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))))
20245a1i 11 . . . . . . . . . . . . . 14 (𝜑 → vol:dom vol⟶(0[,]+∞))
2037, 16ifcld 4505 . . . . . . . . . . . . . . . 16 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ)
204203rexrd 11025 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*)
205 icombl 24728 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
20611, 204, 205syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)) ∈ dom vol)
207202, 206ffvelrnd 6962 . . . . . . . . . . . . 13 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ (0[,]+∞))
20862, 124, 6, 195, 141, 201, 207sge0splitsn 43979 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))))
209 volicore 44119 . . . . . . . . . . . . . . 15 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
21011, 203, 209syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) ∈ ℝ)
211 rexadd 12966 . . . . . . . . . . . . . 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 43524 . . . . . . . . . . . . . . . 16 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21411, 203, 213syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
21516, 7ltnled 11122 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐷𝐾) ↔ ¬ (𝐷𝐾) ≤ 𝑆))
21620, 215mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐷𝐾) ≤ 𝑆)
217216iffalsed 4470 . . . . . . . . . . . . . . . . 17 (𝜑 → if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) = 𝑆)
218217breq2d 5086 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) ↔ (𝐶𝐾) < 𝑆))
219218ifbid 4482 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆), (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0))
220217oveq1d 7290 . . . . . . . . . . . . . . . . 17 (𝜑 → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
221220adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐶𝐾) < 𝑆) → (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)) = (𝑆 − (𝐶𝐾)))
222217, 204eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ∈ ℝ*)
223222adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ*)
22418adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ*)
225 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ¬ (𝐶𝐾) < 𝑆)
22616adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ∈ ℝ)
22711adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℝ)
228226, 227lenltd 11121 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 ≤ (𝐶𝐾) ↔ ¬ (𝐶𝐾) < 𝑆))
229225, 228mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 ≤ (𝐶𝐾))
230 icogelb 13130 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐾) ∈ ℝ* ∧ (𝐷𝐾) ∈ ℝ*𝑆 ∈ ((𝐶𝐾)[,)(𝐷𝐾))) → (𝐶𝐾) ≤ 𝑆)
23118, 12, 15, 230syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐶𝐾) ≤ 𝑆)
232231adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ≤ 𝑆)
233223, 224, 229, 232xrletrid 12889 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 𝑆 = (𝐶𝐾))
234233oveq1d 7290 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝑆 − (𝐶𝐾)) = ((𝐶𝐾) − (𝐶𝐾)))
235227recnd 11003 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → (𝐶𝐾) ∈ ℂ)
236235subidd 11320 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → ((𝐶𝐾) − (𝐶𝐾)) = 0)
237234, 236eqtr2d 2779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶𝐾) < 𝑆) → 0 = (𝑆 − (𝐶𝐾)))
238221, 237ifeqda 4495 . . . . . . . . . . . . . . 15 (𝜑 → if((𝐶𝐾) < 𝑆, (if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆) − (𝐶𝐾)), 0) = (𝑆 − (𝐶𝐾)))
239214, 219, 2383eqtrd 2782 . . . . . . . . . . . . . 14 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆))) = (𝑆 − (𝐶𝐾)))
240239oveq2d 7291 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))))
241121recnd 11003 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) ∈ ℂ)
24211recnd 11003 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐾) ∈ ℂ)
24336, 242subcld 11332 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 − (𝐶𝐾)) ∈ ℂ)
244241, 243addcomd 11177 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) + (𝑆 − (𝐶𝐾))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
245212, 240, 2443eqtrd 2782 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑆, (𝐷𝐾), 𝑆)))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
246194, 208, 2453eqtrd 2782 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))) = ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
247246oveq2d 7291 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
24840recnd 11003 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑆) ∈ ℂ)
249248, 243, 241addassd 10997 . . . . . . . . . . 11 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))))
250249eqcomd 2744 . . . . . . . . . 10 (𝜑 → ((𝑀𝑆) + ((𝑆 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆))))))) = (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
25135, 36, 242npncand 11356 . . . . . . . . . . 11 (𝜑 → ((𝑀𝑆) + (𝑆 − (𝐶𝐾))) = (𝑀 − (𝐶𝐾)))
252251oveq1d 7290 . . . . . . . . . 10 (𝜑 → (((𝑀𝑆) + (𝑆 − (𝐶𝐾))) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
253247, 250, 2523eqtrd 2782 . . . . . . . . 9 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))))
254192mpteq1d 5169 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))) = (𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
255254fveq2d 6778 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
256197breq1d 5084 . . . . . . . . . . . . . 14 (𝑗 = 𝐾 → ((𝐷𝑗) ≤ 𝑀 ↔ (𝐷𝐾) ≤ 𝑀))
257256, 197ifbieq1d 4483 . . . . . . . . . . . . 13 (𝑗 = 𝐾 → if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀) = if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
258196, 257oveq12d 7293 . . . . . . . . . . . 12 (𝑗 = 𝐾 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)) = ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))
259258fveq2d 6778 . . . . . . . . . . 11 (𝑗 = 𝐾 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))) = (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))))
2607, 9ifcld 4505 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ)
261260rexrd 11025 . . . . . . . . . . . . 13 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*)
262 icombl 24728 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ*) → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
26311, 261, 262syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)) ∈ dom vol)
264202, 263ffvelrnd 6962 . . . . . . . . . . 11 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ (0[,]+∞))
26562, 124, 6, 195, 132, 259, 264sge0splitsn 43979 . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ((ℕ ∖ {𝐾}) ∪ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))))
266 volicore 44119 . . . . . . . . . . . . 13 (((𝐶𝐾) ∈ ℝ ∧ if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ∈ ℝ) → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
26711, 260, 266syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) ∈ ℝ)
268 rexadd 12966 . . . . . . . . . . . 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 43524 . . . . . . . . . . . . . 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 12928 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ ℝ ∧ (𝐷𝐾) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
27416, 7, 9, 273syl3anc 1370 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) ↔ (𝑆 < (𝐷𝐾) ∧ 𝑆 < 𝑀)))
275272, 274mpbird 256 . . . . . . . . . . . . . . 15 (𝜑𝑆 < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
27611, 16, 260, 231, 275lelttrd 11133 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))
277276iftrued 4467 . . . . . . . . . . . . 13 (𝜑 → if((𝐶𝐾) < if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀), (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)), 0) = (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)))
278 iftrue 4465 . . . . . . . . . . . . . . . . 17 ((𝐷𝐾) ≤ 𝑀 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
279278adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = (𝐷𝐾))
28012adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ∈ ℝ*)
2819rexrd 11025 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ*)
282281adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ∈ ℝ*)
283 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) ≤ 𝑀)
284 min1 12923 . . . . . . . . . . . . . . . . . . . 20 (((𝐷𝐾) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2857, 2, 284syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if((𝐷𝐾) ≤ 𝐵, (𝐷𝐾), 𝐵) ≤ (𝐷𝐾))
2864, 285eqbrtrd 5096 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ≤ (𝐷𝐾))
287286adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → 𝑀 ≤ (𝐷𝐾))
288280, 282, 283, 287xrletrid 12889 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → (𝐷𝐾) = 𝑀)
289279, 288eqtrd 2778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
290 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → ¬ (𝐷𝐾) ≤ 𝑀)
291290iffalsed 4470 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐷𝐾) ≤ 𝑀) → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
292289, 291pm2.61dan 810 . . . . . . . . . . . . . 14 (𝜑 → if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) = 𝑀)
293292oveq1d 7290 . . . . . . . . . . . . 13 (𝜑 → (if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀) − (𝐶𝐾)) = (𝑀 − (𝐶𝐾)))
294271, 277, 2933eqtrd 2782 . . . . . . . . . . . 12 (𝜑 → (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀))) = (𝑀 − (𝐶𝐾)))
295294oveq2d 7291 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))))
296139recnd 11003 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ∈ ℂ)
29735, 242subcld 11332 . . . . . . . . . . . 12 (𝜑 → (𝑀 − (𝐶𝐾)) ∈ ℂ)
298296, 297addcomd 11177 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) + (𝑀 − (𝐶𝐾))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
299269, 295, 2983eqtrd 2782 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) +𝑒 (vol‘((𝐶𝐾)[,)if((𝐷𝐾) ≤ 𝑀, (𝐷𝐾), 𝑀)))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
300255, 265, 2993eqtrd 2782 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) = ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
301253, 300breq12d 5087 . . . . . . . 8 (𝜑 → (((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))) ↔ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ ((𝑀 − (𝐶𝐾)) + (Σ^‘(𝑗 ∈ (ℕ ∖ {𝐾}) ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))))
302189, 301mpbird 256 . . . . . . 7 (𝜑 → ((𝑀𝑆) + (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑆, (𝐷𝑗), 𝑆)))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30342, 82, 103, 119, 302letrd 11132 . . . . . 6 (𝜑 → ((𝑀𝑆) + (𝑆𝐴)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30439, 303eqbrtrd 5096 . . . . 5 (𝜑 → (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
30534, 304jca 512 . . . 4 (𝜑 → (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
306 oveq1 7282 . . . . . 6 (𝑧 = 𝑀 → (𝑧𝐴) = (𝑀𝐴))
307 breq2 5078 . . . . . . . . . . 11 (𝑧 = 𝑀 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑀))
308 id 22 . . . . . . . . . . 11 (𝑧 = 𝑀𝑧 = 𝑀)
309307, 308ifbieq2d 4485 . . . . . . . . . 10 (𝑧 = 𝑀 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))
310309oveq2d 7291 . . . . . . . . 9 (𝑧 = 𝑀 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))
311310fveq2d 6778 . . . . . . . 8 (𝑧 = 𝑀 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))
312311mpteq2dv 5176 . . . . . . 7 (𝑧 = 𝑀 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))
313312fveq2d 6778 . . . . . 6 (𝑧 = 𝑀 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀))))))
314306, 313breq12d 5087 . . . . 5 (𝑧 = 𝑀 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
315314elrab 3624 . . . 4 (𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝑀 ∈ (𝐴[,]𝐵) ∧ (𝑀𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑀, (𝐷𝑗), 𝑀)))))))
316305, 315sylibr 233 . . 3 (𝜑𝑀 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
317316, 105eleqtrrdi 2850 . 2 (𝜑𝑀𝑈)
318272simprd 496 . 2 (𝜑𝑆 < 𝑀)
319 breq2 5078 . . 3 (𝑢 = 𝑀 → (𝑆 < 𝑢𝑆 < 𝑀))
320319rspcev 3561 . 2 ((𝑀𝑈𝑆 < 𝑀) → ∃𝑢𝑈 𝑆 < 𝑢)
321317, 318, 320syl2anc 584 1 (𝜑 → ∃𝑢𝑈 𝑆 < 𝑢)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wrex 3065  {crab 3068  Vcvv 3432  cdif 3884  cun 3885  wss 3887  ifcif 4459  {csn 4561   class class class wbr 5074  cmpt 5157  dom cdm 5589  wf 6429  cfv 6433  (class class class)co 7275  cr 10870  0cc0 10871   + caddc 10874  +∞cpnf 11006  *cxr 11008   < clt 11009  cle 11010  cmin 11205  cn 11973   +𝑒 cxad 12846  [,)cico 13081  [,]cicc 13082  volcvol 24627  Σ^csumge0 43900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-pm 8618  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-rlim 15198  df-sum 15398  df-rest 17133  df-topgen 17154  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-top 22043  df-topon 22060  df-bases 22096  df-cmp 22538  df-ovol 24628  df-vol 24629  df-sumge0 43901
This theorem is referenced by:  hoidmv1lelem3  44131
  Copyright terms: Public domain W3C validator