Metamath Proof Explorer

Theorem hoidmv1lelem3

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
hoidmv1lelem3.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
hoidmv1lelem3.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
hoidmv1lelem3.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ℝ )
hoidmv1lelem3.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℝ )
hoidmv1lelem3.x ⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ∪ 𝑗 ∈ ℕ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
hoidmv1lelem3.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
hoidmv1lelem3.u ⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) }
hoidmv1lelem3.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
Assertion hoidmv1lelem3 ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmv1lelem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 hoidmv1lelem3.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 hoidmv1lelem3.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 hoidmv1lelem3.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ℝ )
5 hoidmv1lelem3.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℝ )
6 hoidmv1lelem3.x ⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ∪ 𝑗 ∈ ℕ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
7 hoidmv1lelem3.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
8 hoidmv1lelem3.u ⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) }
9 hoidmv1lelem3.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
10 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
11 nnex ⊢ ℕ ∈ V
12 11 a1i ⊢ ( 𝜑 → ℕ ∈ V )
13 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
14 0xr ⊢ 0 ∈ ℝ*
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℝ* )
16 pnfxr ⊢ +∞ ∈ ℝ*
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → +∞ ∈ ℝ* )
18 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ )
19 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ )
20 2 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐵 ∈ ℝ )
21 19 20 ifcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ∈ ℝ )
22 volicore ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ∈ ℝ )
23 18 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ∈ ℝ )
24 23 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ∈ ℝ* )
25 21 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ∈ ℝ* )
26 icombl ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ∈ dom vol )
27 18 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ∈ dom vol )
28 volge0 ⊢ ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ∈ dom vol → 0 ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) )
30 23 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) < +∞ )
31 15 17 24 29 30 elicod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ∈ ( 0 [,) +∞ ) )
32 13 31 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ∈ ( 0 [,] +∞ ) )
33 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) )
34 32 33 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
35 12 34 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ∈ ℝ* )
36 16 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
37 7 rexrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
38 nfv ⊢ Ⅎ 𝑗 𝜑
39 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
41 19 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ℝ* )
42 icombl ⊢ ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol )
43 18 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol )
44 40 43 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
45 18 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ℝ* )
46 18 leidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) )
47 min1 ⊢ ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ≤ ( 𝐷 ‘ 𝑗 ) )
48 19 20 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ≤ ( 𝐷 ‘ 𝑗 ) )
49 icossico ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑗 ) ∈ ℝ* ) ∧ ( ( 𝐶 ‘ 𝑗 ) ≤ ( 𝐶 ‘ 𝑗 ) ∧ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ≤ ( 𝐷 ‘ 𝑗 ) ) ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
50 45 41 46 48 49 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
51 volss ⊢ ( ( ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ∈ dom vol ∧ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ⊆ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
52 27 43 50 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ≤ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
53 38 12 32 44 52 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
54 7 ltpnfd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
55 35 37 36 53 54 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) < +∞ )
56 35 36 55 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ≠ +∞ )
57 56 neneqd ⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) = +∞ )
58 12 34 sge0repnf ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) = +∞ ) )
59 57 58 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ∈ ℝ )
60 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
61 1 2 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
62 ssrab2 ⊢ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ⊆ ( 𝐴 [,] 𝐵 )
63 8 62 eqsstri ⊢ 𝑈 ⊆ ( 𝐴 [,] 𝐵 )
64 1 2 3 4 5 7 8 9 hoidmv1lelem1 ⊢ ( 𝜑 → ( 𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )
65 64 simp1d ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
66 63 65 sselid ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐴 [,] 𝐵 ) )
67 61 66 sseldd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
68 67 rexrd ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
69 simpl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → 𝜑 )
70 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → ¬ 𝐵 ≤ 𝑆 )
71 69 67 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → 𝑆 ∈ ℝ )
72 69 2 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → 𝐵 ∈ ℝ )
73 71 72 ltnled ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → ( 𝑆 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑆 ) )
74 70 73 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → 𝑆 < 𝐵 )
75 6 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) ⊆ ∪ 𝑗 ∈ ℕ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
76 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐴 ∈ ℝ* )
78 60 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐵 ∈ ℝ* )
79 68 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝑆 ∈ ℝ* )
80 63 61 sstrid ⊢ ( 𝜑 → 𝑈 ⊆ ℝ )
81 65 ne0d ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
82 64 simp3d ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 )
83 64 simp2d ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
84 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≤ sup ( 𝑈 , ℝ , < ) )
85 80 81 82 83 84 syl31anc ⊢ ( 𝜑 → 𝐴 ≤ sup ( 𝑈 , ℝ , < ) )
86 85 9 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝑆 )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐴 ≤ 𝑆 )
88 simpr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝑆 < 𝐵 )
89 77 78 79 87 88 elicod ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝑆 ∈ ( 𝐴 [,) 𝐵 ) )
90 75 89 sseldd ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝑆 ∈ ∪ 𝑗 ∈ ℕ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
91 eliun ⊢ ( 𝑆 ∈ ∪ 𝑗 ∈ ℕ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
92 90 91 sylib ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ∃ 𝑗 ∈ ℕ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
93 1 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐴 ∈ ℝ )
94 93 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝐴 ∈ ℝ )
95 2 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐵 ∈ ℝ )
96 95 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝐵 ∈ ℝ )
97 4 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐶 : ℕ ⟶ ℝ )
98 97 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝐶 : ℕ ⟶ ℝ )
99 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝐷 : ℕ ⟶ ℝ )
100 99 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝐷 : ℕ ⟶ ℝ )
101 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) )
102 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑗 ) )
103 101 102 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
104 103 fveq2d ⊢ ( 𝑖 = 𝑗 → ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
105 104 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) )
106 105 fveq2i ⊢ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) )
107 106 7 eqeltrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∈ ℝ )
108 107 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∈ ℝ )
109 108 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∈ ℝ )
110 102 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ) )
111 110 102 ifbieq1d ⊢ ( 𝑖 = 𝑗 → if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) )
112 101 111 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) )
113 112 fveq2d ⊢ ( 𝑖 = 𝑗 → ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) )
114 113 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) )
115 114 eqcomi ⊢ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) )
116 115 fveq2i ⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) ) )
117 116 breq2i ⊢ ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) ) ) )
118 117 rabbii ⊢ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) ) ) }
119 8 118 eqtri ⊢ 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑖 ) [,) if ( ( 𝐷 ‘ 𝑖 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑖 ) , 𝑧 ) ) ) ) ) }
120 65 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → 𝑆 ∈ 𝑈 )
121 120 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑆 ∈ 𝑈 )
122 87 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝐴 ≤ 𝑆 )
123 88 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑆 < 𝐵 )
124 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑗 ∈ ℕ )
125 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
126 eqid ⊢ if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 )
127 94 96 98 100 109 119 121 122 123 124 125 126 hoidmv1lelem2 ⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝐵 ) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
128 127 3exp ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ( 𝑗 ∈ ℕ → ( 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) ) )
129 128 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ( ∃ 𝑗 ∈ ℕ 𝑆 ∈ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) )
130 92 129 mpd ⊢ ( ( 𝜑 ∧ 𝑆 < 𝐵 ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
131 69 74 130 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
132 61 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
133 63 132 sstrid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ℝ )
134 81 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ≠ ∅ )
135 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
137 63 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) )
138 65 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑆 ∈ 𝑈 )
139 iccsupr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑈 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝑆 ∈ 𝑈 ) → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )
140 136 137 138 139 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) )
141 140 simp3d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 )
142 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
143 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑈 𝑦 ≤ 𝑥 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
144 133 134 141 142 143 syl31anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
145 144 9 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ 𝑆 )
146 145 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 )
147 63 sseli ⊢ ( 𝑢 ∈ 𝑈 → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) )
148 147 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) )
149 132 148 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ℝ )
150 67 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑆 ∈ ℝ )
151 149 150 lenltd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑢 ) )
152 151 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ↔ ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ) )
153 146 152 mpbid ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 )
154 ralnex ⊢ ( ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
155 153 154 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
156 155 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝑆 ) → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
157 131 156 condan ⊢ ( 𝜑 → 𝐵 ≤ 𝑆 )
158 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑆 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑆 ≤ 𝐵 )
159 76 60 66 158 syl3anc ⊢ ( 𝜑 → 𝑆 ≤ 𝐵 )
160 60 68 157 159 xrletrid ⊢ ( 𝜑 → 𝐵 = 𝑆 )
161 160 65 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
162 161 8 eleqtrdi ⊢ ( 𝜑 → 𝐵 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } )
163 oveq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
164 breq2 ⊢ ( 𝑧 = 𝐵 → ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 ↔ ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 ) )
165 id ⊢ ( 𝑧 = 𝐵 → 𝑧 = 𝐵 )
166 164 165 ifbieq2d ⊢ ( 𝑧 = 𝐵 → if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) = if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) )
167 166 oveq2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) )
168 167 fveq2d ⊢ ( 𝑧 = 𝐵 → ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) = ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) )
169 168 mpteq2dv ⊢ ( 𝑧 = 𝐵 → ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) )
170 169 fveq2d ⊢ ( 𝑧 = 𝐵 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) )
171 163 170 breq12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) ↔ ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ) )
172 171 elrab ⊢ ( 𝐵 ∈ { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝑧 , ( 𝐷 ‘ 𝑗 ) , 𝑧 ) ) ) ) ) } ↔ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ) )
173 162 172 sylib ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) ) )
174 173 simprd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) if ( ( 𝐷 ‘ 𝑗 ) ≤ 𝐵 , ( 𝐷 ‘ 𝑗 ) , 𝐵 ) ) ) ) ) )
175 10 59 7 174 53 letrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )