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 biimpi ⊢ z ∈ U → z ∈ z ∈ A B | z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
127 126 adantl ⊢ φ ∧ z ∈ U → z ∈ z ∈ A B | z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
128 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
129 127 128 sylib ⊢ φ ∧ z ∈ U → z ∈ A B ∧ z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
130 129 simprd ⊢ φ ∧ z ∈ U → z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
131 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
132 130 131 mpbid ⊢ φ ∧ z ∈ U → z ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z + A
133 122 adantr ⊢ φ ∧ z ∈ U → sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S ∈ ℝ
134 106 adantlr ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S ∈ 0 +∞
135 105 adantlr ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → C ⁡ j if D ⁡ j ≤ S D ⁡ j S ∈ dom ⁡ vol
136 103 adantlr ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → if D ⁡ j ≤ S D ⁡ j S ∈ ℝ *
137 61 adantr ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z ∈ ℝ
138 eqidd ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ D ⁡ j ≤ z → D ⁡ j = D ⁡ j
139 iftrue ⊢ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z = D ⁡ j
140 139 adantl ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z = 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 ⊆ A B ∧ A ∈ U → U ⊆ ℝ ∧ U ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ U y ≤ x
149 147 11 46 148 syl3anc ⊢ φ → U ⊆ ℝ ∧ U ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ U y ≤ x
150 149 simp3d ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ U y ≤ x
151 150 adantr ⊢ φ ∧ z ∈ U → ∃ x ∈ ℝ ∀ y ∈ U y ≤ x
152 127 125 sylibr ⊢ φ ∧ z ∈ U → z ∈ U
153 suprub ⊢ U ⊆ ℝ ∧ U ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ U y ≤ x ∧ z ∈ U → z ≤ sup U ℝ <
154 145 146 151 152 153 syl31anc ⊢ φ ∧ z ∈ U → z ≤ sup U ℝ <
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 → if D ⁡ j ≤ S D ⁡ j S = D ⁡ j
159 138 140 158 3eqtr4d ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z = if D ⁡ j ≤ S D ⁡ j S
160 137 159 eqled ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z ≤ if D ⁡ j ≤ S D ⁡ j S
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 → if D ⁡ j ≤ z D ⁡ j z = z
169 168 ad2antlr ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z ∧ D ⁡ j ≤ S → if D ⁡ j ≤ z D ⁡ j z = z
170 iftrue ⊢ D ⁡ j ≤ S → if D ⁡ j ≤ S D ⁡ j S = D ⁡ j
171 170 adantl ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z ∧ D ⁡ j ≤ S → if D ⁡ j ≤ S D ⁡ j S = D ⁡ j
172 169 171 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
173 167 172 mpbird ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z ∧ D ⁡ j ≤ S → if D ⁡ j ≤ z D ⁡ j z ≤ if D ⁡ j ≤ S D ⁡ j S
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 → if D ⁡ j ≤ z D ⁡ j z = z
176 iffalse ⊢ ¬ D ⁡ j ≤ S → if D ⁡ j ≤ S D ⁡ j S = S
177 176 adantl ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z ∧ ¬ D ⁡ j ≤ S → if D ⁡ j ≤ S D ⁡ j S = S
178 175 177 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
179 174 178 mpbird ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z ∧ ¬ D ⁡ j ≤ S → if D ⁡ j ≤ z D ⁡ j z ≤ if D ⁡ j ≤ S D ⁡ j S
180 173 179 pm2.61dan ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ ∧ ¬ D ⁡ j ≤ z → if D ⁡ j ≤ z D ⁡ j z ≤ if D ⁡ j ≤ S D ⁡ j S
181 160 180 pm2.61dan ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → if D ⁡ j ≤ z D ⁡ j z ≤ if D ⁡ j ≤ S D ⁡ j S
182 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
183 78 136 81 181 182 syl22anc ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → C ⁡ j if D ⁡ j ≤ z D ⁡ j z ⊆ C ⁡ j if D ⁡ j ≤ S D ⁡ j S
184 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
185 64 135 183 184 syl3anc ⊢ φ ∧ z ∈ U ∧ j ∈ ℕ → vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z ≤ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S
186 55 56 65 134 185 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
187 97 133 98 186 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
188 54 99 124 132 187 letrd ⊢ φ ∧ z ∈ U → z ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S + A
189 188 ex ⊢ φ → z ∈ U → z ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S + A
190 51 189 ralrimi ⊢ φ → ∀ z ∈ U z ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S + A
191 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
192 53 47 150 123 191 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
193 190 192 mpbird ⊢ φ → sup U ℝ < ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S + A
194 50 193 eqbrtrd ⊢ φ → S ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S + A
195 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
196 194 195 mpbird ⊢ φ → S − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S
197 49 196 jca ⊢ φ → S ∈ A B ∧ S − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S
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 → if D ⁡ j ≤ z D ⁡ j z = if D ⁡ j ≤ S D ⁡ j S
202 201 oveq2d ⊢ z = S → C ⁡ j if D ⁡ j ≤ z D ⁡ j z = C ⁡ j if D ⁡ j ≤ S D ⁡ j S
203 202 fveq2d ⊢ z = S → vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z = vol ⁡ C ⁡ j if D ⁡ j ≤ S D ⁡ j S
204 203 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
205 204 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
206 198 205 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
207 206 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
208 197 207 sylibr ⊢ φ → S ∈ z ∈ A B | z − A ≤ sum^ ⁡ j ∈ ℕ ⟼ vol ⁡ C ⁡ j if D ⁡ j ≤ z D ⁡ j z
209 208 7 eleqtrrdi ⊢ φ → S ∈ U
210 209 46 150 3jca ⊢ φ → S ∈ U ∧ A ∈ U ∧ ∃ x ∈ ℝ ∀ y ∈ U y ≤ x