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