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 biimpi ⊢ ( 𝑧 ∈ 𝑈 → 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
127 126 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
128 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ) )
129 127 128 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ) )
130 129 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) )
131 54 98 97 lesubaddd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ) )
132 130 131 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) )
133 122 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ∈ ℝ )
134 106 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ∈ ( 0 [,] +∞ ) )
135 105 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol )
136 103 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* )
137 61 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ∈ ℝ )
138 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑗 ) )
139 iftrue ⊢ ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = ( 𝐷 ‘ 𝑗 ) )
140 139 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = ( 𝐷 ‘ 𝑗 ) )
141 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
142 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ∈ ℝ )
143 100 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑆 ∈ ℝ )
144 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 )
145 53 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ⊆ ℝ )
146 47 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑈 ≠ ∅ )
147 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
148 iccsupr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )
149 147 11 46 148 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )
150 149 simp3d ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 )
151 150 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 )
152 127 125 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
153 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ sup ( 𝑈 , ℝ , < ) )
154 145 146 151 152 153 syl31anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ sup ( 𝑈 , ℝ , < ) )
155 154 8 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ 𝑆 )
156 155 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ≤ 𝑆 )
157 141 142 143 144 156 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 )
158 157 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) )
159 138 140 158 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
160 137 159 eqled ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
161 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ∈ ℝ )
162 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
163 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 )
164 161 162 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → ( 𝑧 < ( 𝐷 ‘ 𝑗 ) ↔ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) )
165 163 164 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 < ( 𝐷 ‘ 𝑗 ) )
166 161 162 165 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) )
167 166 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) )
168 iffalse ⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 )
169 168 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 )
170 iftrue ⊢ ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) )
171 170 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = ( 𝐷 ‘ 𝑗 ) )
172 169 171 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ↔ 𝑧 ≤ ( 𝐷 ‘ 𝑗 ) ) )
173 167 172 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
174 155 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → 𝑧 ≤ 𝑆 )
175 168 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = 𝑧 )
176 iffalse ⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 )
177 176 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) = 𝑆 )
178 175 177 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → ( if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ↔ 𝑧 ≤ 𝑆 ) )
179 174 178 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
180 173 179 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) ∧ ¬ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
181 160 180 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
182 icossico ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ≤ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) )
183 78 136 81 181 182 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) )
184 volss ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) )
185 64 135 183 184 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) )
186 55 56 65 134 185 sge0lempt ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
187 97 133 98 186 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) + 𝐴 ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) )
188 54 99 124 132 187 letrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) )
189 188 ex ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑈 → 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) )
190 51 189 ralrimi ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) )
191 suprleub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ∈ ℝ ) → ( sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) )
192 53 47 150 123 191 syl31anc ⊢ ( 𝜑 → ( sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ↔ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) )
193 190 192 mpbird ⊢ ( 𝜑 → sup ( 𝑈 , ℝ , < ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) )
194 50 193 eqbrtrd ⊢ ( 𝜑 → 𝑆 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) )
195 100 1 122 lesubaddd ⊢ ( 𝜑 → ( ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ↔ 𝑆 ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) + 𝐴 ) ) )
196 194 195 mpbird ⊢ ( 𝜑 → ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
197 49 196 jca ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
198 oveq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 − 𝐴 ) = ( 𝑆 − 𝐴 ) )
199 breq2 ⊢ ( 𝑧 = 𝑆 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 ) )
200 id ⊢ ( 𝑧 = 𝑆 → 𝑧 = 𝑆 )
201 199 200 ifbieq2d ⊢ ( 𝑧 = 𝑆 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) )
202 201 oveq2d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) )
203 202 fveq2d ⊢ ( 𝑧 = 𝑆 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) )
204 203 mpteq2dv ⊢ ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) )
205 204 fveq2d ⊢ ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) )
206 198 205 breq12d ⊢ ( 𝑧 = 𝑆 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
207 206 elrab ⊢ ( 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑆 , ( 𝐷 ‘ 𝑗 ) , 𝑆 ) ) ) ) ) ) )
208 197 207 sylibr ⊢ ( 𝜑 → 𝑆 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
209 208 7 eleqtrrdi ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
210 209 46 150 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )