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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
hoidmv1lelem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
hoidmv1lelem1.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
hoidmv1lelem1.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ℝ )
hoidmv1lelem1.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℝ )
hoidmv1lelem1.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
hoidmv1lelem1.u ⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) }
hoidmv1lelem1.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
Assertion hoidmv1lelem1 ( 𝜑 → ( 𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )

Proof

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