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 ⊢ φ → A ∈ ℝ
hoidmv1lelem2.b ⊢ φ → B ∈ ℝ
hoidmv1lelem2.c ⊢ φ → C : ℕ ⟶ ℝ
hoidmv1lelem2.d ⊢ φ → D : ℕ ⟶ ℝ
hoidmv1lelem2.r ⊢ φ → sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j D ⁡ j ∈ ℝ
hoidmv1lelem2.u ⊢ U = z ∈ A B | z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
hoidmv1lelem2.e ⊢ φ → S ∈ U
hoidmv1lelem2.g ⊢ φ → A ≤ S
hoidmv1lelem2.l ⊢ φ → S < B
hoidmv1lelem2.k ⊢ φ → K ∈ ℕ
hoidmv1lelem2.s ⊢ φ → S ∈ C ⁡ K D ⁡ K
hoidmv1lelem2.m ⊢ M = if D ⁡ K ≤ B D ⁡ K B
Assertion hoidmv1lelem2 ⊢ φ → ∃ u ∈ U S < u

Proof

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