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⁡jD⁡j∈ℝ
hoidmv1lelem2.u ⊢U=z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
hoidmv1lelem2.e ⊢φ→S∈U
hoidmv1lelem2.g ⊢φ→A≤S
hoidmv1lelem2.l ⊢φ→S<B
hoidmv1lelem2.k ⊢φ→K∈ℕ
hoidmv1lelem2.s ⊢φ→S∈C⁡KD⁡K
hoidmv1lelem2.m ⊢M=ifD⁡K≤BD⁡KB
Assertion hoidmv1lelem2 ⊢φ→∃u∈US<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⁡jD⁡j∈ℝ
6 hoidmv1lelem2.u ⊢U=z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
7 hoidmv1lelem2.e ⊢φ→S∈U
8 hoidmv1lelem2.g ⊢φ→A≤S
9 hoidmv1lelem2.l ⊢φ→S<B
10 hoidmv1lelem2.k ⊢φ→K∈ℕ
11 hoidmv1lelem2.s ⊢φ→S∈C⁡KD⁡K
12 hoidmv1lelem2.m ⊢M=ifD⁡K≤BD⁡KB
13 12 a1i ⊢φ→M=ifD⁡K≤BD⁡KB
14 4 10 ffvelcdmd ⊢φ→D⁡K∈ℝ
15 14 2 ifcld ⊢φ→ifD⁡K≤BD⁡KB∈ℝ
16 13 15 eqeltrd ⊢φ→M∈ℝ
17 3 10 ffvelcdmd ⊢φ→C⁡K∈ℝ
18 14 rexrd ⊢φ→D⁡K∈ℝ*
19 icossre ⊢C⁡K∈ℝ∧D⁡K∈ℝ*→C⁡KD⁡K⊆ℝ
20 17 18 19 syl2anc ⊢φ→C⁡KD⁡K⊆ℝ
21 20 11 sseldd ⊢φ→S∈ℝ
22 17 rexrd ⊢φ→C⁡K∈ℝ*
23 icoltub ⊢C⁡K∈ℝ*∧D⁡K∈ℝ*∧S∈C⁡KD⁡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≤ifD⁡K≤BD⁡KB↔S≤D⁡K∧S≤B
29 21 14 2 28 syl3anc ⊢φ→S≤ifD⁡K≤BD⁡KB↔S≤D⁡K∧S≤B
30 27 29 mpbird ⊢φ→S≤ifD⁡K≤BD⁡KB
31 1 21 15 8 30 letrd ⊢φ→A≤ifD⁡K≤BD⁡KB
32 13 eqcomd ⊢φ→ifD⁡K≤BD⁡KB=M
33 31 32 breqtrd ⊢φ→A≤M
34 min2 ⊢D⁡K∈ℝ∧B∈ℝ→ifD⁡K≤BD⁡KB≤B
35 14 2 34 syl2anc ⊢φ→ifD⁡K≤BD⁡KB≤B
36 13 35 eqbrtrd ⊢φ→M≤B
37 1 2 16 33 36 eliccd ⊢φ→M∈AB
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 ffvelcdmda ⊢φ∧j∈ℕ→C⁡j∈ℝ
51 4 ffvelcdmda ⊢φ∧j∈ℕ→D⁡j∈ℝ
52 21 adantr ⊢φ∧j∈ℕ→S∈ℝ
53 51 52 ifcld ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS∈ℝ
54 53 rexrd ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS∈ℝ*
55 icombl ⊢C⁡j∈ℝ∧ifD⁡j≤SD⁡jS∈ℝ*→C⁡jifD⁡j≤SD⁡jS∈dom⁡vol
56 50 54 55 syl2anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤SD⁡jS∈dom⁡vol
57 49 56 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤SD⁡jS∈0+∞
58 eqid ⊢j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
59 57 58 fmptd ⊢φ→j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS:ℕ⟶0+∞
60 47 59 sge0xrcl ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ*
61 pnfxr ⊢+∞∈ℝ*
62 61 a1i ⊢φ→+∞∈ℝ*
63 5 rexrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j∈ℝ*
64 nfv ⊢Ⅎjφ
65 51 rexrd ⊢φ∧j∈ℕ→D⁡j∈ℝ*
66 icombl ⊢C⁡j∈ℝ∧D⁡j∈ℝ*→C⁡jD⁡j∈dom⁡vol
67 50 65 66 syl2anc ⊢φ∧j∈ℕ→C⁡jD⁡j∈dom⁡vol
68 49 67 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jD⁡j∈0+∞
69 50 rexrd ⊢φ∧j∈ℕ→C⁡j∈ℝ*
70 50 leidd ⊢φ∧j∈ℕ→C⁡j≤C⁡j
71 min1 ⊢D⁡j∈ℝ∧S∈ℝ→ifD⁡j≤SD⁡jS≤D⁡j
72 51 52 71 syl2anc ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS≤D⁡j
73 icossico ⊢C⁡j∈ℝ*∧D⁡j∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤SD⁡jS≤D⁡j→C⁡jifD⁡j≤SD⁡jS⊆C⁡jD⁡j
74 69 65 70 72 73 syl22anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤SD⁡jS⊆C⁡jD⁡j
75 volss ⊢C⁡jifD⁡j≤SD⁡jS∈dom⁡vol∧C⁡jD⁡j∈dom⁡vol∧C⁡jifD⁡j≤SD⁡jS⊆C⁡jD⁡j→vol⁡C⁡jifD⁡j≤SD⁡jS≤vol⁡C⁡jD⁡j
76 56 67 74 75 syl3anc ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤SD⁡jS≤vol⁡C⁡jD⁡j
77 64 47 57 68 76 sge0lempt ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j
78 5 ltpnfd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j<+∞
79 60 63 62 77 78 xrlelttrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS<+∞
80 60 62 79 xrltned ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≠+∞
81 80 neneqd ⊢φ→¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=+∞
82 47 59 sge0repnf ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ↔¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=+∞
83 81 82 mpbird ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ
84 43 83 readdcld ⊢φ→M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ
85 16 adantr ⊢φ∧j∈ℕ→M∈ℝ
86 51 85 ifcld ⊢φ∧j∈ℕ→ifD⁡j≤MD⁡jM∈ℝ
87 86 rexrd ⊢φ∧j∈ℕ→ifD⁡j≤MD⁡jM∈ℝ*
88 icombl ⊢C⁡j∈ℝ∧ifD⁡j≤MD⁡jM∈ℝ*→C⁡jifD⁡j≤MD⁡jM∈dom⁡vol
89 50 87 88 syl2anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤MD⁡jM∈dom⁡vol
90 49 89 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤MD⁡jM∈0+∞
91 eqid ⊢j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
92 90 91 fmptd ⊢φ→j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM:ℕ⟶0+∞
93 47 92 sge0xrcl ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ*
94 min1 ⊢D⁡j∈ℝ∧M∈ℝ→ifD⁡j≤MD⁡jM≤D⁡j
95 51 85 94 syl2anc ⊢φ∧j∈ℕ→ifD⁡j≤MD⁡jM≤D⁡j
96 icossico ⊢C⁡j∈ℝ*∧D⁡j∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤MD⁡jM≤D⁡j→C⁡jifD⁡j≤MD⁡jM⊆C⁡jD⁡j
97 69 65 70 95 96 syl22anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤MD⁡jM⊆C⁡jD⁡j
98 volss ⊢C⁡jifD⁡j≤MD⁡jM∈dom⁡vol∧C⁡jD⁡j∈dom⁡vol∧C⁡jifD⁡j≤MD⁡jM⊆C⁡jD⁡j→vol⁡C⁡jifD⁡j≤MD⁡jM≤vol⁡C⁡jD⁡j
99 89 67 97 98 syl3anc ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤MD⁡jM≤vol⁡C⁡jD⁡j
100 64 47 90 68 99 sge0lempt ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM≤sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j
101 93 63 62 100 78 xrlelttrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM<+∞
102 93 62 101 xrltned ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM≠+∞
103 102 neneqd ⊢φ→¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=+∞
104 47 92 sge0repnf ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ↔¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=+∞
105 103 104 mpbird ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ
106 7 6 eleqtrdi ⊢φ→S∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
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∈ℕ→ifD⁡j≤zD⁡jz=ifD⁡j≤SD⁡jS
111 110 oveq2d ⊢z=S∧j∈ℕ→C⁡jifD⁡j≤zD⁡jz=C⁡jifD⁡j≤SD⁡jS
112 111 fveq2d ⊢z=S∧j∈ℕ→vol⁡C⁡jifD⁡j≤zD⁡jz=vol⁡C⁡jifD⁡j≤SD⁡jS
113 112 mpteq2dva ⊢z=S→j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
114 113 fveq2d ⊢z=S→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
115 107 114 breq12d ⊢z=S→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
116 115 elrab ⊢S∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔S∈AB∧S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
117 106 116 sylib ⊢φ→S∈AB∧S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
118 117 simprd ⊢φ→S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
119 44 83 43 118 leadd2dd ⊢φ→M−S+S-A≤M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
120 difssd ⊢φ→ℕ∖K⊆ℕ
121 64 47 57 83 120 sge0ssrempt ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ
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→ifD⁡j≤MD⁡jM∈ℝ*
131 129 130 88 syl2anc ⊢φ∧j∈ℕ∖K→C⁡jifD⁡j≤MD⁡jM∈dom⁡vol
132 125 131 ffvelcdmd ⊢φ∧j∈ℕ∖K→vol⁡C⁡jifD⁡j≤MD⁡jM∈0+∞
133 64 124 132 sge0xrclmpt ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ*
134 47 90 120 sge0lessmpt ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
135 133 93 62 134 101 xrlelttrd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM<+∞
136 133 62 135 xrltned ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM≠+∞
137 136 neneqd ⊢φ→¬sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM=+∞
138 64 124 132 sge0repnfmpt ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ↔¬sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM=+∞
139 137 138 mpbird ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ
140 16 17 resubcld ⊢φ→M−C⁡K∈ℝ
141 128 57 syldan ⊢φ∧j∈ℕ∖K→vol⁡C⁡jifD⁡j≤SD⁡jS∈0+∞
142 128 56 syldan ⊢φ∧j∈ℕ∖K→C⁡jifD⁡j≤SD⁡jS∈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→ifD⁡j≤SD⁡jS=D⁡j
146 145 adantl ⊢φ∧j∈ℕ∧D⁡j≤S→ifD⁡j≤SD⁡jS=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<ifD⁡K≤BD⁡KB↔S<D⁡K∧S<B
155 21 14 2 154 syl3anc ⊢φ→S<ifD⁡K≤BD⁡KB↔S<D⁡K∧S<B
156 153 155 mpbird ⊢φ→S<ifD⁡K≤BD⁡KB
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≤ifD⁡j≤MD⁡jM↔D⁡j≤D⁡j∧D⁡j≤M
163 149 149 150 162 syl3anc ⊢φ∧j∈ℕ∧D⁡j≤S→D⁡j≤ifD⁡j≤MD⁡jM↔D⁡j≤D⁡j∧D⁡j≤M
164 161 163 mpbird ⊢φ∧j∈ℕ∧D⁡j≤S→D⁡j≤ifD⁡j≤MD⁡jM
165 146 164 eqbrtrd ⊢φ∧j∈ℕ∧D⁡j≤S→ifD⁡j≤SD⁡jS≤ifD⁡j≤MD⁡jM
166 iffalse ⊢¬D⁡j≤S→ifD⁡j≤SD⁡jS=S
167 166 adantl ⊢φ∧j∈ℕ∧¬D⁡j≤S→ifD⁡j≤SD⁡jS=S
168 52 adantr ⊢φ∧j∈ℕ∧¬D⁡j≤S→S∈ℝ
169 86 adantr ⊢φ∧j∈ℕ∧¬D⁡j≤S→ifD⁡j≤MD⁡jM∈ℝ
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<ifD⁡j≤MD⁡jM↔S<D⁡j∧S<M
178 168 171 176 177 syl3anc ⊢φ∧j∈ℕ∧¬D⁡j≤S→S<ifD⁡j≤MD⁡jM↔S<D⁡j∧S<M
179 175 178 mpbird ⊢φ∧j∈ℕ∧¬D⁡j≤S→S<ifD⁡j≤MD⁡jM
180 168 169 179 ltled ⊢φ∧j∈ℕ∧¬D⁡j≤S→S≤ifD⁡j≤MD⁡jM
181 167 180 eqbrtrd ⊢φ∧j∈ℕ∧¬D⁡j≤S→ifD⁡j≤SD⁡jS≤ifD⁡j≤MD⁡jM
182 165 181 pm2.61dan ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS≤ifD⁡j≤MD⁡jM
183 128 182 syldan ⊢φ∧j∈ℕ∖K→ifD⁡j≤SD⁡jS≤ifD⁡j≤MD⁡jM
184 icossico ⊢C⁡j∈ℝ*∧ifD⁡j≤MD⁡jM∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤SD⁡jS≤ifD⁡j≤MD⁡jM→C⁡jifD⁡j≤SD⁡jS⊆C⁡jifD⁡j≤MD⁡jM
185 143 130 144 183 184 syl22anc ⊢φ∧j∈ℕ∖K→C⁡jifD⁡j≤SD⁡jS⊆C⁡jifD⁡j≤MD⁡jM
186 volss ⊢C⁡jifD⁡j≤SD⁡jS∈dom⁡vol∧C⁡jifD⁡j≤MD⁡jM∈dom⁡vol∧C⁡jifD⁡j≤SD⁡jS⊆C⁡jifD⁡j≤MD⁡jM→vol⁡C⁡jifD⁡j≤SD⁡jS≤vol⁡C⁡jifD⁡j≤MD⁡jM
187 142 131 185 186 syl3anc ⊢φ∧j∈ℕ∖K→vol⁡C⁡jifD⁡j≤SD⁡jS≤vol⁡C⁡jifD⁡j≤MD⁡jM
188 64 124 141 132 187 sge0lempt ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
189 121 139 140 188 leadd2dd ⊢φ→M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
190 difsnid ⊢K∈ℕ→ℕ∖K∪K=ℕ
191 10 190 syl ⊢φ→ℕ∖K∪K=ℕ
192 191 eqcomd ⊢φ→ℕ=ℕ∖K∪K
193 192 mpteq1d ⊢φ→j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
194 193 fveq2d ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=sum^⁡j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
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→ifD⁡j≤SD⁡jS=ifD⁡K≤SD⁡KS
200 196 199 oveq12d ⊢j=K→C⁡jifD⁡j≤SD⁡jS=C⁡KifD⁡K≤SD⁡KS
201 200 fveq2d ⊢j=K→vol⁡C⁡jifD⁡j≤SD⁡jS=vol⁡C⁡KifD⁡K≤SD⁡KS
202 48 a1i ⊢φ→vol:dom⁡vol⟶0+∞
203 14 21 ifcld ⊢φ→ifD⁡K≤SD⁡KS∈ℝ
204 203 rexrd ⊢φ→ifD⁡K≤SD⁡KS∈ℝ*
205 icombl ⊢C⁡K∈ℝ∧ifD⁡K≤SD⁡KS∈ℝ*→C⁡KifD⁡K≤SD⁡KS∈dom⁡vol
206 17 204 205 syl2anc ⊢φ→C⁡KifD⁡K≤SD⁡KS∈dom⁡vol
207 202 206 ffvelcdmd ⊢φ→vol⁡C⁡KifD⁡K≤SD⁡KS∈0+∞
208 64 124 10 195 141 201 207 sge0splitsn ⊢φ→sum^⁡j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤SD⁡jS=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+𝑒vol⁡C⁡KifD⁡K≤SD⁡KS
209 volicore ⊢C⁡K∈ℝ∧ifD⁡K≤SD⁡KS∈ℝ→vol⁡C⁡KifD⁡K≤SD⁡KS∈ℝ
210 17 203 209 syl2anc ⊢φ→vol⁡C⁡KifD⁡K≤SD⁡KS∈ℝ
211 rexadd ⊢sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ∧vol⁡C⁡KifD⁡K≤SD⁡KS∈ℝ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+𝑒vol⁡C⁡KifD⁡K≤SD⁡KS=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+vol⁡C⁡KifD⁡K≤SD⁡KS
212 121 210 211 syl2anc ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+𝑒vol⁡C⁡KifD⁡K≤SD⁡KS=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+vol⁡C⁡KifD⁡K≤SD⁡KS
213 volico ⊢C⁡K∈ℝ∧ifD⁡K≤SD⁡KS∈ℝ→vol⁡C⁡KifD⁡K≤SD⁡KS=ifC⁡K<ifD⁡K≤SD⁡KSifD⁡K≤SD⁡KS−C⁡K0
214 17 203 213 syl2anc ⊢φ→vol⁡C⁡KifD⁡K≤SD⁡KS=ifC⁡K<ifD⁡K≤SD⁡KSifD⁡K≤SD⁡KS−C⁡K0
215 21 14 ltnled ⊢φ→S<D⁡K↔¬D⁡K≤S
216 24 215 mpbid ⊢φ→¬D⁡K≤S
217 216 iffalsed ⊢φ→ifD⁡K≤SD⁡KS=S
218 217 breq2d ⊢φ→C⁡K<ifD⁡K≤SD⁡KS↔C⁡K<S
219 218 ifbid ⊢φ→ifC⁡K<ifD⁡K≤SD⁡KSifD⁡K≤SD⁡KS−C⁡K0=ifC⁡K<SifD⁡K≤SD⁡KS−C⁡K0
220 217 oveq1d ⊢φ→ifD⁡K≤SD⁡KS−C⁡K=S−C⁡K
221 220 adantr ⊢φ∧C⁡K<S→ifD⁡K≤SD⁡KS−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⁡KD⁡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 ⊢φ→ifC⁡K<SifD⁡K≤SD⁡KS−C⁡K0=S−C⁡K
239 214 219 238 3eqtrd ⊢φ→vol⁡C⁡KifD⁡K≤SD⁡KS=S−C⁡K
240 239 oveq2d ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+vol⁡C⁡KifD⁡K≤SD⁡KS=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+S-C⁡K
241 121 recnd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℂ
242 17 recnd ⊢φ→C⁡K∈ℂ
243 39 242 subcld ⊢φ→S−C⁡K∈ℂ
244 241 243 addcomd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+S-C⁡K=S-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
245 212 240 244 3eqtrd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS+𝑒vol⁡C⁡KifD⁡K≤SD⁡KS=S-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
246 194 208 245 3eqtrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=S-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
247 246 oveq2d ⊢φ→M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=M−S+S−C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
248 43 recnd ⊢φ→M−S∈ℂ
249 248 243 241 addassd ⊢φ→M−S+S−C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS=M−S+S−C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
250 249 eqcomd ⊢φ→M−S+S−C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS=M−S+S−C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
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⁡jifD⁡j≤SD⁡jS=M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
253 247 250 252 3eqtrd ⊢φ→M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS
254 192 mpteq1d ⊢φ→j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
255 254 fveq2d ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=sum^⁡j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
256 197 breq1d ⊢j=K→D⁡j≤M↔D⁡K≤M
257 256 197 ifbieq1d ⊢j=K→ifD⁡j≤MD⁡jM=ifD⁡K≤MD⁡KM
258 196 257 oveq12d ⊢j=K→C⁡jifD⁡j≤MD⁡jM=C⁡KifD⁡K≤MD⁡KM
259 258 fveq2d ⊢j=K→vol⁡C⁡jifD⁡j≤MD⁡jM=vol⁡C⁡KifD⁡K≤MD⁡KM
260 14 16 ifcld ⊢φ→ifD⁡K≤MD⁡KM∈ℝ
261 260 rexrd ⊢φ→ifD⁡K≤MD⁡KM∈ℝ*
262 icombl ⊢C⁡K∈ℝ∧ifD⁡K≤MD⁡KM∈ℝ*→C⁡KifD⁡K≤MD⁡KM∈dom⁡vol
263 17 261 262 syl2anc ⊢φ→C⁡KifD⁡K≤MD⁡KM∈dom⁡vol
264 202 263 ffvelcdmd ⊢φ→vol⁡C⁡KifD⁡K≤MD⁡KM∈0+∞
265 64 124 10 195 132 259 264 sge0splitsn ⊢φ→sum^⁡j∈ℕ∖K∪K⟼vol⁡C⁡jifD⁡j≤MD⁡jM=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+𝑒vol⁡C⁡KifD⁡K≤MD⁡KM
266 volicore ⊢C⁡K∈ℝ∧ifD⁡K≤MD⁡KM∈ℝ→vol⁡C⁡KifD⁡K≤MD⁡KM∈ℝ
267 17 260 266 syl2anc ⊢φ→vol⁡C⁡KifD⁡K≤MD⁡KM∈ℝ
268 rexadd ⊢sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℝ∧vol⁡C⁡KifD⁡K≤MD⁡KM∈ℝ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+𝑒vol⁡C⁡KifD⁡K≤MD⁡KM=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+vol⁡C⁡KifD⁡K≤MD⁡KM
269 139 267 268 syl2anc ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+𝑒vol⁡C⁡KifD⁡K≤MD⁡KM=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+vol⁡C⁡KifD⁡K≤MD⁡KM
270 volico ⊢C⁡K∈ℝ∧ifD⁡K≤MD⁡KM∈ℝ→vol⁡C⁡KifD⁡K≤MD⁡KM=ifC⁡K<ifD⁡K≤MD⁡KMifD⁡K≤MD⁡KM−C⁡K0
271 17 260 270 syl2anc ⊢φ→vol⁡C⁡KifD⁡K≤MD⁡KM=ifC⁡K<ifD⁡K≤MD⁡KMifD⁡K≤MD⁡KM−C⁡K0
272 24 157 jca ⊢φ→S<D⁡K∧S<M
273 ltmin ⊢S∈ℝ∧D⁡K∈ℝ∧M∈ℝ→S<ifD⁡K≤MD⁡KM↔S<D⁡K∧S<M
274 21 14 16 273 syl3anc ⊢φ→S<ifD⁡K≤MD⁡KM↔S<D⁡K∧S<M
275 272 274 mpbird ⊢φ→S<ifD⁡K≤MD⁡KM
276 17 21 260 231 275 lelttrd ⊢φ→C⁡K<ifD⁡K≤MD⁡KM
277 276 iftrued ⊢φ→ifC⁡K<ifD⁡K≤MD⁡KMifD⁡K≤MD⁡KM−C⁡K0=ifD⁡K≤MD⁡KM−C⁡K
278 iftrue ⊢D⁡K≤M→ifD⁡K≤MD⁡KM=D⁡K
279 278 adantl ⊢φ∧D⁡K≤M→ifD⁡K≤MD⁡KM=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∈ℝ→ifD⁡K≤BD⁡KB≤D⁡K
285 14 2 284 syl2anc ⊢φ→ifD⁡K≤BD⁡KB≤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→ifD⁡K≤MD⁡KM=M
290 simpr ⊢φ∧¬D⁡K≤M→¬D⁡K≤M
291 290 iffalsed ⊢φ∧¬D⁡K≤M→ifD⁡K≤MD⁡KM=M
292 289 291 pm2.61dan ⊢φ→ifD⁡K≤MD⁡KM=M
293 292 oveq1d ⊢φ→ifD⁡K≤MD⁡KM−C⁡K=M−C⁡K
294 271 277 293 3eqtrd ⊢φ→vol⁡C⁡KifD⁡K≤MD⁡KM=M−C⁡K
295 294 oveq2d ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+vol⁡C⁡KifD⁡K≤MD⁡KM=sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+M-C⁡K
296 139 recnd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM∈ℂ
297 38 242 subcld ⊢φ→M−C⁡K∈ℂ
298 296 297 addcomd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+M-C⁡K=M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
299 269 295 298 3eqtrd ⊢φ→sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM+𝑒vol⁡C⁡KifD⁡K≤MD⁡KM=M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
300 255 265 299 3eqtrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM=M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
301 253 300 breq12d ⊢φ→M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM↔M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤M-C⁡K+sum^⁡j∈ℕ∖K⟼vol⁡C⁡jifD⁡j≤MD⁡jM
302 189 301 mpbird ⊢φ→M-S+sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
303 45 84 105 119 302 letrd ⊢φ→M−S+S-A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
304 42 303 eqbrtrd ⊢φ→M−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
305 37 304 jca ⊢φ→M∈AB∧M−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
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→ifD⁡j≤zD⁡jz=ifD⁡j≤MD⁡jM
310 309 oveq2d ⊢z=M→C⁡jifD⁡j≤zD⁡jz=C⁡jifD⁡j≤MD⁡jM
311 310 fveq2d ⊢z=M→vol⁡C⁡jifD⁡j≤zD⁡jz=vol⁡C⁡jifD⁡j≤MD⁡jM
312 311 mpteq2dv ⊢z=M→j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
313 312 fveq2d ⊢z=M→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
314 306 313 breq12d ⊢z=M→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔M−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
315 314 elrab ⊢M∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔M∈AB∧M−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤MD⁡jM
316 305 315 sylibr ⊢φ→M∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
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∈US<u
321 317 318 320 syl2anc ⊢φ→∃u∈US<u