Metamath Proof Explorer

Theorem hoidmv1lelem1

Description: The supremum of U belongs to U . This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem1.a ⊢φ→A∈ℝ
hoidmv1lelem1.b ⊢φ→B∈ℝ
hoidmv1lelem1.l ⊢φ→A<B
hoidmv1lelem1.c ⊢φ→C:ℕ⟶ℝ
hoidmv1lelem1.d ⊢φ→D:ℕ⟶ℝ
hoidmv1lelem1.r ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j∈ℝ
hoidmv1lelem1.u ⊢U=z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
hoidmv1lelem1.s ⊢S=supUℝ<
Assertion hoidmv1lelem1 ⊢φ→S∈U∧A∈U∧∃x∈ℝ∀y∈Uy≤x

Proof

Step Hyp Ref Expression
1 hoidmv1lelem1.a ⊢φ→A∈ℝ
2 hoidmv1lelem1.b ⊢φ→B∈ℝ
3 hoidmv1lelem1.l ⊢φ→A<B
4 hoidmv1lelem1.c ⊢φ→C:ℕ⟶ℝ
5 hoidmv1lelem1.d ⊢φ→D:ℕ⟶ℝ
6 hoidmv1lelem1.r ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j∈ℝ
7 hoidmv1lelem1.u ⊢U=z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
8 hoidmv1lelem1.s ⊢S=supUℝ<
9 ssrab2 ⊢z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz⊆AB
10 7 9 eqsstri ⊢U⊆AB
11 10 a1i ⊢φ→U⊆AB
12 1 rexrd ⊢φ→A∈ℝ*
13 2 rexrd ⊢φ→B∈ℝ*
14 1 2 3 ltled ⊢φ→A≤B
15 lbicc2 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→A∈AB
16 12 13 14 15 syl3anc ⊢φ→A∈AB
17 1 recnd ⊢φ→A∈ℂ
18 17 subidd ⊢φ→A−A=0
19 nfv ⊢Ⅎjφ
20 nnex ⊢ℕ∈V
21 20 a1i ⊢φ→ℕ∈V
22 volf ⊢vol:dom⁡vol⟶0+∞
23 22 a1i ⊢φ∧j∈ℕ→vol:dom⁡vol⟶0+∞
24 4 ffvelcdmda ⊢φ∧j∈ℕ→C⁡j∈ℝ
25 5 ffvelcdmda ⊢φ∧j∈ℕ→D⁡j∈ℝ
26 1 adantr ⊢φ∧j∈ℕ→A∈ℝ
27 25 26 ifcld ⊢φ∧j∈ℕ→ifD⁡j≤AD⁡jA∈ℝ
28 27 rexrd ⊢φ∧j∈ℕ→ifD⁡j≤AD⁡jA∈ℝ*
29 icombl ⊢C⁡j∈ℝ∧ifD⁡j≤AD⁡jA∈ℝ*→C⁡jifD⁡j≤AD⁡jA∈dom⁡vol
30 24 28 29 syl2anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤AD⁡jA∈dom⁡vol
31 23 30 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤AD⁡jA∈0+∞
32 19 21 31 sge0ge0mpt ⊢φ→0≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
33 18 32 eqbrtrd ⊢φ→A−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
34 16 33 jca ⊢φ→A∈AB∧A−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
35 oveq1 ⊢z=A→z−A=A−A
36 breq2 ⊢z=A→D⁡j≤z↔D⁡j≤A
37 id ⊢z=A→z=A
38 36 37 ifbieq2d ⊢z=A→ifD⁡j≤zD⁡jz=ifD⁡j≤AD⁡jA
39 38 oveq2d ⊢z=A→C⁡jifD⁡j≤zD⁡jz=C⁡jifD⁡j≤AD⁡jA
40 39 fveq2d ⊢z=A→vol⁡C⁡jifD⁡j≤zD⁡jz=vol⁡C⁡jifD⁡j≤AD⁡jA
41 40 mpteq2dv ⊢z=A→j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
42 41 fveq2d ⊢z=A→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
43 35 42 breq12d ⊢z=A→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔A−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
44 43 elrab ⊢A∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔A∈AB∧A−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤AD⁡jA
45 34 44 sylibr ⊢φ→A∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
46 45 7 eleqtrrdi ⊢φ→A∈U
47 46 ne0d ⊢φ→U≠∅
48 1 2 11 47 supicc ⊢φ→supUℝ<∈AB
49 8 48 eqeltrid ⊢φ→S∈AB
50 8 a1i ⊢φ→S=supUℝ<
51 nfv ⊢Ⅎzφ
52 1 2 iccssred ⊢φ→AB⊆ℝ
53 11 52 sstrd ⊢φ→U⊆ℝ
54 53 sselda ⊢φ∧z∈U→z∈ℝ
55 nfv ⊢Ⅎjφ∧z∈U
56 20 a1i ⊢φ∧z∈U→ℕ∈V
57 22 a1i ⊢φ∧z∈U∧j∈ℕ→vol:dom⁡vol⟶0+∞
58 24 adantlr ⊢φ∧z∈U∧j∈ℕ→C⁡j∈ℝ
59 25 adantlr ⊢φ∧z∈U∧j∈ℕ→D⁡j∈ℝ
60 54 adantr ⊢φ∧z∈U∧j∈ℕ→z∈ℝ
61 59 60 ifcld ⊢φ∧z∈U∧j∈ℕ→ifD⁡j≤zD⁡jz∈ℝ
62 61 rexrd ⊢φ∧z∈U∧j∈ℕ→ifD⁡j≤zD⁡jz∈ℝ*
63 icombl ⊢C⁡j∈ℝ∧ifD⁡j≤zD⁡jz∈ℝ*→C⁡jifD⁡j≤zD⁡jz∈dom⁡vol
64 58 62 63 syl2anc ⊢φ∧z∈U∧j∈ℕ→C⁡jifD⁡j≤zD⁡jz∈dom⁡vol
65 57 64 ffvelcdmd ⊢φ∧z∈U∧j∈ℕ→vol⁡C⁡jifD⁡j≤zD⁡jz∈0+∞
66 55 56 65 sge0xrclmpt ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz∈ℝ*
67 pnfxr ⊢+∞∈ℝ*
68 67 a1i ⊢φ∧z∈U→+∞∈ℝ*
69 6 rexrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j∈ℝ*
70 69 adantr ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j∈ℝ*
71 25 rexrd ⊢φ∧j∈ℕ→D⁡j∈ℝ*
72 icombl ⊢C⁡j∈ℝ∧D⁡j∈ℝ*→C⁡jD⁡j∈dom⁡vol
73 24 71 72 syl2anc ⊢φ∧j∈ℕ→C⁡jD⁡j∈dom⁡vol
74 23 73 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jD⁡j∈0+∞
75 74 adantlr ⊢φ∧z∈U∧j∈ℕ→vol⁡C⁡jD⁡j∈0+∞
76 73 adantlr ⊢φ∧z∈U∧j∈ℕ→C⁡jD⁡j∈dom⁡vol
77 24 rexrd ⊢φ∧j∈ℕ→C⁡j∈ℝ*
78 77 adantlr ⊢φ∧z∈U∧j∈ℕ→C⁡j∈ℝ*
79 71 adantlr ⊢φ∧z∈U∧j∈ℕ→D⁡j∈ℝ*
80 24 leidd ⊢φ∧j∈ℕ→C⁡j≤C⁡j
81 80 adantlr ⊢φ∧z∈U∧j∈ℕ→C⁡j≤C⁡j
82 min1 ⊢D⁡j∈ℝ∧z∈ℝ→ifD⁡j≤zD⁡jz≤D⁡j
83 59 60 82 syl2anc ⊢φ∧z∈U∧j∈ℕ→ifD⁡j≤zD⁡jz≤D⁡j
84 icossico ⊢C⁡j∈ℝ*∧D⁡j∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤zD⁡jz≤D⁡j→C⁡jifD⁡j≤zD⁡jz⊆C⁡jD⁡j
85 78 79 81 83 84 syl22anc ⊢φ∧z∈U∧j∈ℕ→C⁡jifD⁡j≤zD⁡jz⊆C⁡jD⁡j
86 volss ⊢C⁡jifD⁡j≤zD⁡jz∈dom⁡vol∧C⁡jD⁡j∈dom⁡vol∧C⁡jifD⁡j≤zD⁡jz⊆C⁡jD⁡j→vol⁡C⁡jifD⁡j≤zD⁡jz≤vol⁡C⁡jD⁡j
87 64 76 85 86 syl3anc ⊢φ∧z∈U∧j∈ℕ→vol⁡C⁡jifD⁡j≤zD⁡jz≤vol⁡C⁡jD⁡j
88 55 56 65 75 87 sge0lempt ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz≤sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j
89 6 ltpnfd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j<+∞
90 89 adantr ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j<+∞
91 66 70 68 88 90 xrlelttrd ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz<+∞
92 66 68 91 xrltned ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz≠+∞
93 92 neneqd ⊢φ∧z∈U→¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=+∞
94 eqid ⊢j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
95 65 94 fmptd ⊢φ∧z∈U→j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz:ℕ⟶0+∞
96 56 95 sge0repnf ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz∈ℝ↔¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=+∞
97 93 96 mpbird ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz∈ℝ
98 1 adantr ⊢φ∧z∈U→A∈ℝ
99 97 98 readdcld ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz+A∈ℝ
100 52 49 sseldd ⊢φ→S∈ℝ
101 100 adantr ⊢φ∧j∈ℕ→S∈ℝ
102 25 101 ifcld ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS∈ℝ
103 102 rexrd ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS∈ℝ*
104 icombl ⊢C⁡j∈ℝ∧ifD⁡j≤SD⁡jS∈ℝ*→C⁡jifD⁡j≤SD⁡jS∈dom⁡vol
105 24 103 104 syl2anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤SD⁡jS∈dom⁡vol
106 23 105 ffvelcdmd ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤SD⁡jS∈0+∞
107 19 21 106 sge0xrclmpt ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ*
108 67 a1i ⊢φ→+∞∈ℝ*
109 min1 ⊢D⁡j∈ℝ∧S∈ℝ→ifD⁡j≤SD⁡jS≤D⁡j
110 25 101 109 syl2anc ⊢φ∧j∈ℕ→ifD⁡j≤SD⁡jS≤D⁡j
111 icossico ⊢C⁡j∈ℝ*∧D⁡j∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤SD⁡jS≤D⁡j→C⁡jifD⁡j≤SD⁡jS⊆C⁡jD⁡j
112 77 71 80 110 111 syl22anc ⊢φ∧j∈ℕ→C⁡jifD⁡j≤SD⁡jS⊆C⁡jD⁡j
113 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
114 105 73 112 113 syl3anc ⊢φ∧j∈ℕ→vol⁡C⁡jifD⁡j≤SD⁡jS≤vol⁡C⁡jD⁡j
115 19 21 106 74 114 sge0lempt ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≤sum^⁡j∈ℕ⟼vol⁡C⁡jD⁡j
116 107 69 108 115 89 xrlelttrd ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS<+∞
117 107 108 116 xrltned ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS≠+∞
118 117 neneqd ⊢φ→¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=+∞
119 eqid ⊢j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
120 106 119 fmptd ⊢φ→j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS:ℕ⟶0+∞
121 21 120 sge0repnf ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ↔¬sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS=+∞
122 118 121 mpbird ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ
123 122 1 readdcld ⊢φ→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A∈ℝ
124 123 adantr ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A∈ℝ
125 7 eleq2i ⊢z∈U↔z∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
126 125 biimpi ⊢z∈U→z∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
127 126 adantl ⊢φ∧z∈U→z∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
128 rabid ⊢z∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔z∈AB∧z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
129 127 128 sylib ⊢φ∧z∈U→z∈AB∧z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
130 129 simprd ⊢φ∧z∈U→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
131 54 98 97 lesubaddd ⊢φ∧z∈U→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔z≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz+A
132 130 131 mpbid ⊢φ∧z∈U→z≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz+A
133 122 adantr ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS∈ℝ
134 106 adantlr ⊢φ∧z∈U∧j∈ℕ→vol⁡C⁡jifD⁡j≤SD⁡jS∈0+∞
135 105 adantlr ⊢φ∧z∈U∧j∈ℕ→C⁡jifD⁡j≤SD⁡jS∈dom⁡vol
136 103 adantlr ⊢φ∧z∈U∧j∈ℕ→ifD⁡j≤SD⁡jS∈ℝ*
137 61 adantr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→ifD⁡j≤zD⁡jz∈ℝ
138 eqidd ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→D⁡j=D⁡j
139 iftrue ⊢D⁡j≤z→ifD⁡j≤zD⁡jz=D⁡j
140 139 adantl ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→ifD⁡j≤zD⁡jz=D⁡j
141 59 adantr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→D⁡j∈ℝ
142 60 adantr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→z∈ℝ
143 100 ad3antrrr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→S∈ℝ
144 simpr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→D⁡j≤z
145 53 adantr ⊢φ∧z∈U→U⊆ℝ
146 47 adantr ⊢φ∧z∈U→U≠∅
147 1 2 jca ⊢φ→A∈ℝ∧B∈ℝ
148 iccsupr ⊢A∈ℝ∧B∈ℝ∧U⊆AB∧A∈U→U⊆ℝ∧U≠∅∧∃x∈ℝ∀y∈Uy≤x
149 147 11 46 148 syl3anc ⊢φ→U⊆ℝ∧U≠∅∧∃x∈ℝ∀y∈Uy≤x
150 149 simp3d ⊢φ→∃x∈ℝ∀y∈Uy≤x
151 150 adantr ⊢φ∧z∈U→∃x∈ℝ∀y∈Uy≤x
152 127 125 sylibr ⊢φ∧z∈U→z∈U
153 suprub ⊢U⊆ℝ∧U≠∅∧∃x∈ℝ∀y∈Uy≤x∧z∈U→z≤supUℝ<
154 145 146 151 152 153 syl31anc ⊢φ∧z∈U→z≤supUℝ<
155 154 8 breqtrrdi ⊢φ∧z∈U→z≤S
156 155 ad2antrr ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→z≤S
157 141 142 143 144 156 letrd ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→D⁡j≤S
158 157 iftrued ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→ifD⁡j≤SD⁡jS=D⁡j
159 138 140 158 3eqtr4d ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→ifD⁡j≤zD⁡jz=ifD⁡j≤SD⁡jS
160 137 159 eqled ⊢φ∧z∈U∧j∈ℕ∧D⁡j≤z→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS
161 60 adantr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→z∈ℝ
162 59 adantr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→D⁡j∈ℝ
163 simpr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→¬D⁡j≤z
164 161 162 ltnled ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→z<D⁡j↔¬D⁡j≤z
165 163 164 mpbird ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→z<D⁡j
166 161 162 165 ltled ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→z≤D⁡j
167 166 adantr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧D⁡j≤S→z≤D⁡j
168 iffalse ⊢¬D⁡j≤z→ifD⁡j≤zD⁡jz=z
169 168 ad2antlr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧D⁡j≤S→ifD⁡j≤zD⁡jz=z
170 iftrue ⊢D⁡j≤S→ifD⁡j≤SD⁡jS=D⁡j
171 170 adantl ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧D⁡j≤S→ifD⁡j≤SD⁡jS=D⁡j
172 169 171 breq12d ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧D⁡j≤S→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS↔z≤D⁡j
173 167 172 mpbird ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧D⁡j≤S→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS
174 155 ad3antrrr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧¬D⁡j≤S→z≤S
175 168 ad2antlr ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧¬D⁡j≤S→ifD⁡j≤zD⁡jz=z
176 iffalse ⊢¬D⁡j≤S→ifD⁡j≤SD⁡jS=S
177 176 adantl ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧¬D⁡j≤S→ifD⁡j≤SD⁡jS=S
178 175 177 breq12d ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧¬D⁡j≤S→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS↔z≤S
179 174 178 mpbird ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z∧¬D⁡j≤S→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS
180 173 179 pm2.61dan ⊢φ∧z∈U∧j∈ℕ∧¬D⁡j≤z→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS
181 160 180 pm2.61dan ⊢φ∧z∈U∧j∈ℕ→ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS
182 icossico ⊢C⁡j∈ℝ*∧ifD⁡j≤SD⁡jS∈ℝ*∧C⁡j≤C⁡j∧ifD⁡j≤zD⁡jz≤ifD⁡j≤SD⁡jS→C⁡jifD⁡j≤zD⁡jz⊆C⁡jifD⁡j≤SD⁡jS
183 78 136 81 181 182 syl22anc ⊢φ∧z∈U∧j∈ℕ→C⁡jifD⁡j≤zD⁡jz⊆C⁡jifD⁡j≤SD⁡jS
184 volss ⊢C⁡jifD⁡j≤zD⁡jz∈dom⁡vol∧C⁡jifD⁡j≤SD⁡jS∈dom⁡vol∧C⁡jifD⁡j≤zD⁡jz⊆C⁡jifD⁡j≤SD⁡jS→vol⁡C⁡jifD⁡j≤zD⁡jz≤vol⁡C⁡jifD⁡j≤SD⁡jS
185 64 135 183 184 syl3anc ⊢φ∧z∈U∧j∈ℕ→vol⁡C⁡jifD⁡j≤zD⁡jz≤vol⁡C⁡jifD⁡j≤SD⁡jS
186 55 56 65 134 185 sge0lempt ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
187 97 133 98 186 leadd1dd ⊢φ∧z∈U→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz+A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
188 54 99 124 132 187 letrd ⊢φ∧z∈U→z≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
189 188 ex ⊢φ→z∈U→z≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
190 51 189 ralrimi ⊢φ→∀z∈Uz≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
191 suprleub ⊢U⊆ℝ∧U≠∅∧∃x∈ℝ∀y∈Uy≤x∧sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A∈ℝ→supUℝ<≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A↔∀z∈Uz≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
192 53 47 150 123 191 syl31anc ⊢φ→supUℝ<≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A↔∀z∈Uz≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
193 190 192 mpbird ⊢φ→supUℝ<≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
194 50 193 eqbrtrd ⊢φ→S≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
195 100 1 122 lesubaddd ⊢φ→S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS↔S≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS+A
196 194 195 mpbird ⊢φ→S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
197 49 196 jca ⊢φ→S∈AB∧S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
198 oveq1 ⊢z=S→z−A=S−A
199 breq2 ⊢z=S→D⁡j≤z↔D⁡j≤S
200 id ⊢z=S→z=S
201 199 200 ifbieq2d ⊢z=S→ifD⁡j≤zD⁡jz=ifD⁡j≤SD⁡jS
202 201 oveq2d ⊢z=S→C⁡jifD⁡j≤zD⁡jz=C⁡jifD⁡j≤SD⁡jS
203 202 fveq2d ⊢z=S→vol⁡C⁡jifD⁡j≤zD⁡jz=vol⁡C⁡jifD⁡j≤SD⁡jS
204 203 mpteq2dv ⊢z=S→j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
205 204 fveq2d ⊢z=S→sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz=sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
206 198 205 breq12d ⊢z=S→z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz↔S−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤SD⁡jS
207 206 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
208 197 207 sylibr ⊢φ→S∈z∈AB|z−A≤sum^⁡j∈ℕ⟼vol⁡C⁡jifD⁡j≤zD⁡jz
209 208 7 eleqtrrdi ⊢φ→S∈U
210 209 46 150 3jca ⊢φ→S∈U∧A∈U∧∃x∈ℝ∀y∈Uy≤x