Metamath Proof Explorer

Theorem hoidmv1lelem2

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)

Ref Expression
Hypotheses 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 hoidmv1lelem2 ( 𝜑 → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )

Proof

Step Hyp Ref Expression
1 hoidmv1lelem2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 hoidmv1lelem2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 hoidmv1lelem2.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ℝ )
4 hoidmv1lelem2.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℝ )
5 hoidmv1lelem2.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
6 hoidmv1lelem2.u ⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) }
7 hoidmv1lelem2.e ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
8 hoidmv1lelem2.g ⊢ ( 𝜑 → 𝐴 ≤ 𝑆 )
9 hoidmv1lelem2.l ⊢ ( 𝜑 → 𝑆 < 𝐵 )
10 hoidmv1lelem2.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
11 hoidmv1lelem2.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐶 ‘ 𝐾 ) [,) ( 𝐷 ‘ 𝐾 ) ) )
12 hoidmv1lelem2.m ⊢ 𝑀 = if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 )
13 12 a1i ⊢ ( 𝜑 → 𝑀 = if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) )
14 4 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐾 ) ∈ ℝ )
15 14 2 ifcld ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ∈ ℝ )
16 13 15 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
17 3 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐾 ) ∈ ℝ )
18 14 rexrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐾 ) ∈ ℝ* )
19 icossre ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝐾 ) [,) ( 𝐷 ‘ 𝐾 ) ) ⊆ ℝ )
20 17 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝐾 ) [,) ( 𝐷 ‘ 𝐾 ) ) ⊆ ℝ )
21 20 11 sseldd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
22 17 rexrd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐾 ) ∈ ℝ* )
23 icoltub ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ* ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝐾 ) [,) ( 𝐷 ‘ 𝐾 ) ) ) → 𝑆 < ( 𝐷 ‘ 𝐾 ) )
24 22 18 11 23 syl3anc ⊢ ( 𝜑 → 𝑆 < ( 𝐷 ‘ 𝐾 ) )
25 21 14 24 ltled ⊢ ( 𝜑 → 𝑆 ≤ ( 𝐷 ‘ 𝐾 ) )
26 21 2 9 ltled ⊢ ( 𝜑 → 𝑆 ≤ 𝐵 )
27 25 26 jca ⊢ ( 𝜑 → ( 𝑆 ≤ ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 ≤ 𝐵 ) )
28 lemin ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑆 ≤ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ↔ ( 𝑆 ≤ ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 ≤ 𝐵 ) ) )
29 21 14 2 28 syl3anc ⊢ ( 𝜑 → ( 𝑆 ≤ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ↔ ( 𝑆 ≤ ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 ≤ 𝐵 ) ) )
30 27 29 mpbird ⊢ ( 𝜑 → 𝑆 ≤ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) )
31 1 21 15 8 30 letrd ⊢ ( 𝜑 → 𝐴 ≤ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) )
32 13 eqcomd ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) = 𝑀 )
33 31 32 breqtrd ⊢ ( 𝜑 → 𝐴 ≤ 𝑀 )
34 min2 ⊢ ( ( ( 𝐷 ‘ 𝐾 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ≤ 𝐵 )
35 14 2 34 syl2anc ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ≤ 𝐵 )
36 13 35 eqbrtrd ⊢ ( 𝜑 → 𝑀 ≤ 𝐵 )
37 1 2 16 33 36 eliccd ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 [,] 𝐵 ) )
38 16 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
39 21 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
40 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
41 38 39 40 npncand ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( 𝑆 − 𝐴 ) ) = ( 𝑀 − 𝐴 ) )
42 41 eqcomd ⊢ ( 𝜑 → ( 𝑀 − 𝐴 ) = ( ( 𝑀 − 𝑆 ) + ( 𝑆 − 𝐴 ) ) )
43 16 21 resubcld ⊢ ( 𝜑 → ( 𝑀 − 𝑆 ) ∈ ℝ )
44 21 1 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝐴 ) ∈ ℝ )
45 43 44 readdcld ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( 𝑆 − 𝐴 ) ) ∈ ℝ )
46 nnex ⊢ ℕ ∈ V
47 46 a1i ⊢ ( 𝜑 → ℕ ∈ V )
48 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
49 48 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
50 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
51 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
52 21 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
53 51 52 ifcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ )
54 53 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* )
55 icombl ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol )
56 50 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol )
57 49 56 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) )
58 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) )
59 57 58 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
60 47 59 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ* )
61 pnfxr ⊢ +∞ ∈ ℝ*
62 61 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
63 5 rexrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
64 nfv ⊢ Ⅎ 𝑗 𝜑
65 51 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ* )
66 icombl ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol )
67 50 65 66 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol )
68 49 67 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
69 50 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ* )
70 50 leidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) )
71 min1 ⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) )
72 51 52 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) )
73 icossico ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ ( 𝐷 ‘ 𝑗 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
74 69 65 70 72 73 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
75 volss ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
76 56 67 74 75 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
77 64 47 57 68 76 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
78 5 ltpnfd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
79 60 63 62 77 78 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) < +∞ )
80 60 62 79 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ≠ +∞ )
81 80 neneqd ⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = +∞ )
82 47 59 sge0repnf ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = +∞ ) )
83 81 82 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ )
84 43 83 readdcld ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ∈ ℝ )
85 16 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑀 ∈ ℝ )
86 51 85 ifcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ )
87 86 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ* )
88 icombl ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ∈ dom vol )
89 50 87 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ∈ dom vol )
90 49 89 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ∈ ( 0 [,] +∞ ) )
91 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) )
92 90 91 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
93 47 92 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ* )
94 min1 ⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ≤ ( 𝐷 ‘ 𝑗 ) )
95 51 85 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ≤ ( 𝐷 ‘ 𝑗 ) )
96 icossico ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ≤ ( 𝐷 ‘ 𝑗 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
97 69 65 70 95 96 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
98 volss ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
99 89 67 97 98 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
100 64 47 90 68 99 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
101 93 63 62 100 78 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) < +∞ )
102 93 62 101 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ≠ +∞ )
103 102 neneqd ⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = +∞ )
104 47 92 sge0repnf ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = +∞ ) )
105 103 104 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ )
106 7 6 eleqtrdi ⊢ ( 𝜑 → 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
107 oveq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 − 𝐴 ) = ( 𝑆 − 𝐴 ) )
108 simpl ⊢ ( ( 𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ ) → 𝑧 = 𝑆 )
109 108 breq2d ⊢ ( ( 𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) )
110 109 108 ifbieq2d ⊢ ( ( 𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
111 110 oveq2d ⊢ ( ( 𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) )
112 111 fveq2d ⊢ ( ( 𝑧 = 𝑆 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) )
113 112 mpteq2dva ⊢ ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) )
114 113 fveq2d ⊢ ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
115 107 114 breq12d ⊢ ( 𝑧 = 𝑆 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
116 115 elrab ⊢ ( 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
117 106 116 sylib ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
118 117 simprd ⊢ ( 𝜑 → ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
119 44 83 43 118 leadd2dd ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( 𝑆 − 𝐴 ) ) ≤ ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
120 difssd ⊢ ( 𝜑 → ( ℕ ∖ { 𝐾 } ) ⊆ ℕ )
121 64 47 57 83 120 sge0ssrempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ )
122 difexg ⊢ ( ℕ ∈ V → ( ℕ ∖ { 𝐾 } ) ∈ V )
123 46 122 ax-mp ⊢ ( ℕ ∖ { 𝐾 } ) ∈ V
124 123 a1i ⊢ ( 𝜑 → ( ℕ ∖ { 𝐾 } ) ∈ V )
125 48 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
126 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → 𝜑 )
127 eldifi ⊢ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) → 𝑗 ∈ ℕ )
128 127 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → 𝑗 ∈ ℕ )
129 126 128 50 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
130 128 87 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ* )
131 129 130 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ∈ dom vol )
132 125 131 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ∈ ( 0 [,] +∞ ) )
133 64 124 132 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ* )
134 47 90 120 sge0lessmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
135 133 93 62 134 101 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) < +∞ )
136 133 62 135 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ≠ +∞ )
137 136 neneqd ⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = +∞ )
138 64 124 132 sge0repnfmpt ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = +∞ ) )
139 137 138 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ )
140 16 17 resubcld ⊢ ( 𝜑 → ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) ∈ ℝ )
141 128 57 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) )
142 128 56 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol )
143 128 69 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ* )
144 128 70 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) )
145 iftrue ⊢ ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) )
146 145 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) )
147 51 leidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ≤ ( 𝐷 ‘ 𝑗 ) )
148 147 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ≤ ( 𝐷 ‘ 𝑗 ) )
149 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
150 85 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑀 ∈ ℝ )
151 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 ∈ ℝ )
152 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 )
153 24 9 jca ⊢ ( 𝜑 → ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝐵 ) )
154 ltmin ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝐵 ) ) )
155 21 14 2 154 syl3anc ⊢ ( 𝜑 → ( 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝐵 ) ) )
156 153 155 mpbird ⊢ ( 𝜑 → 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) )
157 156 32 breqtrd ⊢ ( 𝜑 → 𝑆 < 𝑀 )
158 157 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 < 𝑀 )
159 149 151 150 152 158 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) < 𝑀 )
160 149 150 159 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 )
161 148 160 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( ( 𝐷 ‘ 𝑗 ) ≤ ( 𝐷 ‘ 𝑗 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 ) )
162 lemin ⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑗 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ↔ ( ( 𝐷 ‘ 𝑗 ) ≤ ( 𝐷 ‘ 𝑗 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 ) ) )
163 149 149 150 162 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( ( 𝐷 ‘ 𝑗 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ↔ ( ( 𝐷 ‘ 𝑗 ) ≤ ( 𝐷 ‘ 𝑗 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 ) ) )
164 161 163 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
165 146 164 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
166 iffalse ⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 )
167 166 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 )
168 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 ∈ ℝ )
169 86 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ )
170 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 )
171 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
172 168 171 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝑆 < ( 𝐷 ‘ 𝑗 ) ↔ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) )
173 170 172 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 < ( 𝐷 ‘ 𝑗 ) )
174 157 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 < 𝑀 )
175 173 174 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝑆 < ( 𝐷 ‘ 𝑗 ) ∧ 𝑆 < 𝑀 ) )
176 85 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑀 ∈ ℝ )
177 ltmin ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑆 < if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝑗 ) ∧ 𝑆 < 𝑀 ) ) )
178 168 171 176 177 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( 𝑆 < if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝑗 ) ∧ 𝑆 < 𝑀 ) ) )
179 175 178 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 < if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
180 168 169 179 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑆 ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
181 167 180 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
182 165 181 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
183 128 182 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
184 icossico ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) )
185 143 130 144 183 184 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) )
186 volss ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) )
187 142 131 185 186 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) )
188 64 124 141 132 187 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
189 121 139 140 188 leadd2dd ⊢ ( 𝜑 → ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ≤ ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
190 difsnid ⊢ ( 𝐾 ∈ ℕ → ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ℕ )
191 10 190 syl ⊢ ( 𝜑 → ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) = ℕ )
192 191 eqcomd ⊢ ( 𝜑 → ℕ = ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
193 192 mpteq1d ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) = ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) )
194 193 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
195 neldifsnd ⊢ ( 𝜑 → ¬ 𝐾 ∈ ( ℕ ∖ { 𝐾 } ) )
196 fveq2 ⊢ ( 𝑗 = 𝐾 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝐾 ) )
197 fveq2 ⊢ ( 𝑗 = 𝐾 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝐾 ) )
198 197 breq1d ⊢ ( 𝑗 = 𝐾 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ↔ ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 ) )
199 198 197 ifbieq1d ⊢ ( 𝑗 = 𝐾 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) )
200 196 199 oveq12d ⊢ ( 𝑗 = 𝐾 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) = ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) )
201 200 fveq2d ⊢ ( 𝑗 = 𝐾 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) )
202 48 a1i ⊢ ( 𝜑 → vol : dom vol ⟶ ( 0 [,] +∞ ) )
203 14 21 ifcld ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ∈ ℝ )
204 203 rexrd ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ∈ ℝ* )
205 icombl ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ∈ dom vol )
206 17 204 205 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ∈ dom vol )
207 202 206 ffvelcdmd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) )
208 64 124 10 195 141 201 207 sge0splitsn ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) )
209 volicore ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ∈ ℝ )
210 17 203 209 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ∈ ℝ )
211 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ ∧ ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) )
212 121 210 211 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) )
213 volico ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) = if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) )
214 17 203 213 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) = if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) )
215 21 14 ltnled ⊢ ( 𝜑 → ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ↔ ¬ ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 ) )
216 24 215 mpbid ⊢ ( 𝜑 → ¬ ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 )
217 216 iffalsed ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) = 𝑆 )
218 217 breq2d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ↔ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) )
219 218 ifbid ⊢ ( 𝜑 → if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) = if ( ( 𝐶 ‘ 𝐾 ) < 𝑆 , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) )
220 217 oveq1d ⊢ ( 𝜑 → ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) = ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) )
221 220 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) = ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) )
222 217 204 eqeltrrd ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
223 222 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → 𝑆 ∈ ℝ* )
224 22 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝐶 ‘ 𝐾 ) ∈ ℝ* )
225 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 )
226 21 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → 𝑆 ∈ ℝ )
227 17 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝐶 ‘ 𝐾 ) ∈ ℝ )
228 226 227 lenltd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝑆 ≤ ( 𝐶 ‘ 𝐾 ) ↔ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) )
229 225 228 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → 𝑆 ≤ ( 𝐶 ‘ 𝐾 ) )
230 icogelb ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ* ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝐾 ) [,) ( 𝐷 ‘ 𝐾 ) ) ) → ( 𝐶 ‘ 𝐾 ) ≤ 𝑆 )
231 22 18 11 230 syl3anc ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐾 ) ≤ 𝑆 )
232 231 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝐶 ‘ 𝐾 ) ≤ 𝑆 )
233 223 224 229 232 xrletrid ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → 𝑆 = ( 𝐶 ‘ 𝐾 ) )
234 233 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) = ( ( 𝐶 ‘ 𝐾 ) − ( 𝐶 ‘ 𝐾 ) ) )
235 227 recnd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( 𝐶 ‘ 𝐾 ) ∈ ℂ )
236 235 subidd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → ( ( 𝐶 ‘ 𝐾 ) − ( 𝐶 ‘ 𝐾 ) ) = 0 )
237 234 236 eqtr2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ‘ 𝐾 ) < 𝑆 ) → 0 = ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) )
238 221 237 ifeqda ⊢ ( 𝜑 → if ( ( 𝐶 ‘ 𝐾 ) < 𝑆 , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) = ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) )
239 214 219 238 3eqtrd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) = ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) )
240 239 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) )
241 121 recnd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℂ )
242 17 recnd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐾 ) ∈ ℂ )
243 39 242 subcld ⊢ ( 𝜑 → ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ∈ ℂ )
244 241 243 addcomd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) = ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
245 212 240 244 3eqtrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑆 , ( 𝐷 ‘ 𝐾 ) , 𝑆 ) ) ) ) = ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
246 194 208 245 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) = ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
247 246 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) = ( ( 𝑀 − 𝑆 ) + ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) )
248 43 recnd ⊢ ( 𝜑 → ( 𝑀 − 𝑆 ) ∈ ℂ )
249 248 243 241 addassd ⊢ ( 𝜑 → ( ( ( 𝑀 − 𝑆 ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) = ( ( 𝑀 − 𝑆 ) + ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) )
250 249 eqcomd ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ) = ( ( ( 𝑀 − 𝑆 ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
251 38 39 242 npncand ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) = ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) )
252 251 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 − 𝑆 ) + ( 𝑆 − ( 𝐶 ‘ 𝐾 ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) = ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
253 247 250 252 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) = ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
254 192 mpteq1d ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) = ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) )
255 254 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
256 197 breq1d ⊢ ( 𝑗 = 𝐾 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 ↔ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) )
257 256 197 ifbieq1d ⊢ ( 𝑗 = 𝐾 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) = if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) )
258 196 257 oveq12d ⊢ ( 𝑗 = 𝐾 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) = ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) )
259 258 fveq2d ⊢ ( 𝑗 = 𝐾 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) )
260 14 16 ifcld ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ∈ ℝ )
261 260 rexrd ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ∈ ℝ* )
262 icombl ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ∈ dom vol )
263 17 261 262 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ∈ dom vol )
264 202 263 ffvelcdmd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ∈ ( 0 [,] +∞ ) )
265 64 124 10 195 132 259 264 sge0splitsn ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ( ℕ ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) )
266 volicore ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ∈ ℝ )
267 17 260 266 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ∈ ℝ )
268 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℝ ∧ ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) )
269 139 267 268 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) )
270 volico ⊢ ( ( ( 𝐶 ‘ 𝐾 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) = if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) )
271 17 260 270 syl2anc ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) = if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) )
272 24 157 jca ⊢ ( 𝜑 → ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝑀 ) )
273 ltmin ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐷 ‘ 𝐾 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝑀 ) ) )
274 21 14 16 273 syl3anc ⊢ ( 𝜑 → ( 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ↔ ( 𝑆 < ( 𝐷 ‘ 𝐾 ) ∧ 𝑆 < 𝑀 ) ) )
275 272 274 mpbird ⊢ ( 𝜑 → 𝑆 < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) )
276 17 21 260 231 275 lelttrd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) )
277 276 iftrued ⊢ ( 𝜑 → if ( ( 𝐶 ‘ 𝐾 ) < if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) , ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) − ( 𝐶 ‘ 𝐾 ) ) , 0 ) = ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) − ( 𝐶 ‘ 𝐾 ) ) )
278 iftrue ⊢ ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) = ( 𝐷 ‘ 𝐾 ) )
279 278 adantl ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) = ( 𝐷 ‘ 𝐾 ) )
280 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → ( 𝐷 ‘ 𝐾 ) ∈ ℝ* )
281 16 rexrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
282 281 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → 𝑀 ∈ ℝ* )
283 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 )
284 min1 ⊢ ( ( ( 𝐷 ‘ 𝐾 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ≤ ( 𝐷 ‘ 𝐾 ) )
285 14 2 284 syl2anc ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝐵 , ( 𝐷 ‘ 𝐾 ) , 𝐵 ) ≤ ( 𝐷 ‘ 𝐾 ) )
286 13 285 eqbrtrd ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 ‘ 𝐾 ) )
287 286 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → 𝑀 ≤ ( 𝐷 ‘ 𝐾 ) )
288 280 282 283 287 xrletrid ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → ( 𝐷 ‘ 𝐾 ) = 𝑀 )
289 279 288 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) = 𝑀 )
290 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → ¬ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 )
291 290 iffalsed ⊢ ( ( 𝜑 ∧ ¬ ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 ) → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) = 𝑀 )
292 289 291 pm2.61dan ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) = 𝑀 )
293 292 oveq1d ⊢ ( 𝜑 → ( if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) − ( 𝐶 ‘ 𝐾 ) ) = ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) )
294 271 277 293 3eqtrd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) = ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) )
295 294 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) + ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) + ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) ) )
296 139 recnd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ∈ ℂ )
297 38 242 subcld ⊢ ( 𝜑 → ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) ∈ ℂ )
298 296 297 addcomd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) + ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) ) = ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
299 269 295 298 3eqtrd ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) +𝑒 ( vol ‘ ( ( 𝐶 ‘ 𝐾 ) [,) if ( ( 𝐷 ‘ 𝐾 ) ≤ 𝑀 , ( 𝐷 ‘ 𝐾 ) , 𝑀 ) ) ) ) = ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
300 255 265 299 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) = ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
301 253 300 breq12d ⊢ ( 𝜑 → ( ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ↔ ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ≤ ( ( 𝑀 − ( 𝐶 ‘ 𝐾 ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( ℕ ∖ { 𝐾 } ) ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) ) )
302 189 301 mpbird ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
303 45 84 105 119 302 letrd ⊢ ( 𝜑 → ( ( 𝑀 − 𝑆 ) + ( 𝑆 − 𝐴 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
304 42 303 eqbrtrd ⊢ ( 𝜑 → ( 𝑀 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
305 37 304 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑀 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
306 oveq1 ⊢ ( 𝑧 = 𝑀 → ( 𝑧 − 𝐴 ) = ( 𝑀 − 𝐴 ) )
307 breq2 ⊢ ( 𝑧 = 𝑀 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 ) )
308 id ⊢ ( 𝑧 = 𝑀 → 𝑧 = 𝑀 )
309 307 308 ifbieq2d ⊢ ( 𝑧 = 𝑀 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) )
310 309 oveq2d ⊢ ( 𝑧 = 𝑀 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) )
311 310 fveq2d ⊢ ( 𝑧 = 𝑀 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) )
312 311 mpteq2dv ⊢ ( 𝑧 = 𝑀 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) )
313 312 fveq2d ⊢ ( 𝑧 = 𝑀 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) )
314 306 313 breq12d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝑀 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
315 314 elrab ⊢ ( 𝑀 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑀 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑀 , ( 𝐷 ‘ 𝑗 ) , 𝑀 ) ) ) ) ) ) )
316 305 315 sylibr ⊢ ( 𝜑 → 𝑀 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
317 316 6 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
318 272 simprd ⊢ ( 𝜑 → 𝑆 < 𝑀 )
319 breq2 ⊢ ( 𝑢 = 𝑀 → ( 𝑆 < 𝑢 ↔ 𝑆 < 𝑀 ) )
320 319 rspcev ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑆 < 𝑀 ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
321 317 318 320 syl2anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )