Metamath Proof Explorer

Theorem hoidmvlelem4

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29, case nonempty interval and dimension of the space greater than 1 . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem4.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hoidmvlelem4.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoidmvlelem4.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
hoidmvlelem4.n ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
hoidmvlelem4.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
hoidmvlelem4.w ⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
hoidmvlelem4.a ⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ )
hoidmvlelem4.b ⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ )
hoidmvlelem4.k ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
hoidmvlelem4.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem4.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem4.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
hoidmvlelem4.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
hoidmvlelem4.14 ⊢ 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) )
hoidmvlelem4.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
hoidmvlelem4.u ⊢ 𝑈 = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) }
hoidmvlelem4.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
hoidmvlelem4.i ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
hoidmvlelem4.i2 ⊢ ( 𝜑 → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
Assertion hoidmvlelem4 ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmvlelem4.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoidmvlelem4.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoidmvlelem4.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4 hoidmvlelem4.n ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
5 hoidmvlelem4.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
6 hoidmvlelem4.w ⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
7 hoidmvlelem4.a ⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ )
8 hoidmvlelem4.b ⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ )
9 hoidmvlelem4.k ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
10 hoidmvlelem4.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
11 hoidmvlelem4.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
12 hoidmvlelem4.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
13 hoidmvlelem4.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
14 hoidmvlelem4.14 ⊢ 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) )
15 hoidmvlelem4.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
16 hoidmvlelem4.u ⊢ 𝑈 = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) }
17 hoidmvlelem4.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
18 hoidmvlelem4.i ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
19 hoidmvlelem4.i2 ⊢ ( 𝜑 → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
20 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
21 5 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
22 snssi ⊢ ( 𝑍 ∈ 𝑋 → { 𝑍 } ⊆ 𝑋 )
23 21 22 syl ⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑋 )
24 3 23 unssd ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ⊆ 𝑋 )
25 6 24 eqsstrid ⊢ ( 𝜑 → 𝑊 ⊆ 𝑋 )
26 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑊 ⊆ 𝑋 ) → 𝑊 ∈ Fin )
27 2 25 26 syl2anc ⊢ ( 𝜑 → 𝑊 ∈ Fin )
28 1 27 7 8 hoidmvcl ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
29 20 28 sseldi ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ )
30 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
31 15 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
32 30 31 readdcld ⊢ ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ )
33 nfv ⊢ Ⅎ 𝑗 𝜑
34 nnex ⊢ ℕ ∈ V
35 34 a1i ⊢ ( 𝜑 → ℕ ∈ V )
36 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
37 27 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
38 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
39 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
40 38 39 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
41 eleq1 ⊢ ( 𝑗 = ℎ → ( 𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
42 fveq2 ⊢ ( 𝑗 = ℎ → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ ℎ ) )
43 42 breq1d ⊢ ( 𝑗 = ℎ → ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝑐 ‘ ℎ ) ≤ 𝑥 ) )
44 43 42 ifbieq1d ⊢ ( 𝑗 = ℎ → if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) = if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) )
45 41 42 44 ifbieq12d ⊢ ( 𝑗 = ℎ → if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) = if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
46 45 cbvmptv ⊢ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) = ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
47 46 mpteq2i ⊢ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) )
48 47 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
49 13 48 eqtri ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
50 snidg ⊢ ( 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑍 ∈ { 𝑍 } )
51 5 50 syl ⊢ ( 𝜑 → 𝑍 ∈ { 𝑍 } )
52 elun2 ⊢ ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
53 51 52 syl ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
54 6 a1i ⊢ ( 𝜑 → 𝑊 = ( 𝑌 ∪ { 𝑍 } ) )
55 54 eqcomd ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) = 𝑊 )
56 53 55 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
57 8 56 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
59 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
60 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
62 49 58 37 61 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
63 1 37 40 62 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
64 36 63 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
65 33 35 64 sge0clmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
66 33 35 64 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
67 pnfxr ⊢ +∞ ∈ ℝ*
68 67 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
69 12 rexrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
70 1 37 40 61 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
71 36 70 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
72 5 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
73 56 72 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
75 1 37 74 6 58 49 40 61 hsphoidmvle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) )
76 33 35 64 71 75 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
77 12 ltpnfd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
78 66 69 68 76 77 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
79 66 68 78 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ )
80 ge0xrre ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
81 65 79 80 syl2anc ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
82 32 81 remulcld ⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
83 32 12 remulcld ⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
84 56 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) )
85 eleq1 ⊢ ( 𝑘 = 𝑍 → ( 𝑘 ∈ 𝑊 ↔ 𝑍 ∈ 𝑊 ) )
86 85 anbi2d ⊢ ( 𝑘 = 𝑍 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ↔ ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) ) )
87 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑍 ) )
88 fveq2 ⊢ ( 𝑘 = 𝑍 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑍 ) )
89 87 88 breq12d ⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) )
90 86 89 imbi12d ⊢ ( 𝑘 = 𝑍 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ) )
91 90 9 vtoclg ⊢ ( 𝑍 ∈ 𝑊 → ( ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) )
92 56 84 91 sylc ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) )
93 1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92 hoidmvlelem1 ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
94 57 rexrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
95 iccssxr ⊢ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ⊆ ℝ*
96 ssrab2 ⊢ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) )
97 16 96 eqsstri ⊢ 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) )
98 97 93 sseldi ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
99 95 98 sseldi ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
100 simpl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝜑 )
101 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 )
102 7 56 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
103 102 57 iccssred ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ⊆ ℝ )
104 103 98 sseldd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
105 104 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝑆 ∈ ℝ )
106 100 57 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
107 105 106 ltnled ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ( 𝑆 < ( 𝐵 ‘ 𝑍 ) ↔ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) )
108 101 107 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝑆 < ( 𝐵 ‘ 𝑍 ) )
109 2 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑋 ∈ Fin )
110 3 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑌 ⊆ 𝑋 )
111 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
112 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐴 : 𝑊 ⟶ ℝ )
113 8 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐵 : 𝑊 ⟶ ℝ )
114 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
115 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ 0 ) = ( 𝑦 ∈ 𝑌 ↦ 0 )
116 10 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
117 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) )
118 117 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) )
119 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑗 ) )
120 119 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) )
121 118 120 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) )
122 121 eleq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) )
123 117 reseq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) = ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) )
124 122 123 ifbieq1d ⊢ ( 𝑖 = 𝑗 → if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
125 124 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
126 11 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
127 119 reseq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) = ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) )
128 122 127 ifbieq1d ⊢ ( 𝑖 = 𝑗 → if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
129 128 cbvmptv ⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
130 12 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
131 15 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐸 ∈ ℝ+ )
132 93 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑆 ∈ 𝑈 )
133 simpr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑆 < ( 𝐵 ‘ 𝑍 ) )
134 biid ⊢ ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) )
135 eqidd ⊢ ( 𝑤 = 𝑦 → 0 = 0 )
136 135 cbvmptv ⊢ ( 𝑤 ∈ 𝑌 ↦ 0 ) = ( 𝑦 ∈ 𝑌 ↦ 0 )
137 134 136 ifbieq2i ⊢ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) )
138 137 mpteq2i ⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
139 138 a1i ⊢ ( 𝑙 = 𝑗 → ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) )
140 id ⊢ ( 𝑙 = 𝑗 → 𝑙 = 𝑗 )
141 139 140 fveq12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) = ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) )
142 134 136 ifbieq2i ⊢ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) )
143 142 mpteq2i ⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) )
144 143 a1i ⊢ ( 𝑙 = 𝑗 → ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) )
145 144 140 fveq12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) = ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) )
146 141 145 oveq12d ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) )
147 146 cbvmptv ⊢ ( 𝑙 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) )
148 18 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) )
149 19 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) )
150 eqid ⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) )
151 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑘 ) )
152 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑘 ) )
153 151 152 oveq12d ⊢ ( 𝑦 = 𝑘 → ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
154 153 cbvixpv ⊢ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) = X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
155 eleq1 ⊢ ( 𝑦 = 𝑘 → ( 𝑦 ∈ 𝑌 ↔ 𝑘 ∈ 𝑌 ) )
156 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑥 ‘ 𝑦 ) = ( 𝑥 ‘ 𝑘 ) )
157 155 156 ifbieq1d ⊢ ( 𝑦 = 𝑘 → if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) = if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) )
158 157 cbvmptv ⊢ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) = ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) )
159 154 158 mpteq12i ⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ↦ ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) )
160 150 159 eqtri ⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ↦ ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) )
161 1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160 hoidmvlelem3 ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
162 100 108 161 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
163 97 a1i ⊢ ( 𝜑 → 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
164 163 103 sstrd ⊢ ( 𝜑 → 𝑈 ⊆ ℝ )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ℝ )
166 ne0i ⊢ ( 𝑢 ∈ 𝑈 → 𝑈 ≠ ∅ )
167 166 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ≠ ∅ )
168 102 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
170 94 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
171 163 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
172 iccleub ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
173 169 170 171 172 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
174 173 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
175 brralrspcev ⊢ ( ( ( 𝐵 ‘ 𝑍 ) ∈ ℝ ∧ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 )
176 57 174 175 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 )
177 176 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 )
178 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
179 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
180 165 167 177 178 179 syl31anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
181 180 17 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ 𝑆 )
182 181 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 )
183 165 178 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ℝ )
184 104 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑆 ∈ ℝ )
185 183 184 lenltd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑢 ) )
186 185 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ↔ ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ) )
187 182 186 mpbid ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 )
188 ralnex ⊢ ( ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
189 187 188 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
190 189 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
191 100 108 190 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 )
192 162 191 condan ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 )
193 iccleub ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑆 ≤ ( 𝐵 ‘ 𝑍 ) )
194 168 94 98 193 syl3anc ⊢ ( 𝜑 → 𝑆 ≤ ( 𝐵 ‘ 𝑍 ) )
195 94 99 192 194 xrletrid ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) = 𝑆 )
196 16 eqcomi ⊢ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } = 𝑈
197 196 a1i ⊢ ( 𝜑 → { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } = 𝑈 )
198 195 197 eleq12d ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ 𝑆 ∈ 𝑈 ) )
199 93 198 mpbird ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
200 oveq1 ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
201 200 oveq2d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
202 fveq2 ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) )
203 202 fveq1d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
204 203 oveq2d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
205 204 mpteq2dv ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
206 205 fveq2d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
207 206 oveq2d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
208 201 207 breq12d ⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
209 208 elrab ⊢ ( ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( ( 𝐵 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
210 199 209 sylib ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
211 210 simprd ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
212 2 3 ssfid ⊢ ( 𝜑 → 𝑌 ∈ Fin )
213 eqid ⊢ ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
214 1 212 5 72 6 7 8 213 hoiprodp1 ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) = ( ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) )
215 eqidd ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
216 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐴 : 𝑊 ⟶ ℝ )
217 ssun1 ⊢ 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } )
218 6 eqcomi ⊢ ( 𝑌 ∪ { 𝑍 } ) = 𝑊
219 217 218 sseqtri ⊢ 𝑌 ⊆ 𝑊
220 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝑘 ∈ 𝑌 )
221 219 220 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝑘 ∈ 𝑊 )
222 216 221 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
223 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 : 𝑊 ⟶ ℝ )
224 223 221 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
225 221 9 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
226 222 224 225 volicon0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
227 226 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
228 14 a1i ⊢ ( 𝜑 → 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) )
229 219 a1i ⊢ ( 𝜑 → 𝑌 ⊆ 𝑊 )
230 7 229 fssresd ⊢ ( 𝜑 → ( 𝐴 ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
231 8 229 fssresd ⊢ ( 𝜑 → ( 𝐵 ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
232 1 212 4 230 231 hoidmvn0val ⊢ ( 𝜑 → ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) )
233 fvres ⊢ ( 𝑘 ∈ 𝑌 → ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
234 fvres ⊢ ( 𝑘 ∈ 𝑌 → ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
235 233 234 oveq12d ⊢ ( 𝑘 ∈ 𝑌 → ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
236 235 fveq2d ⊢ ( 𝑘 ∈ 𝑌 → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
237 236 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
238 volico ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
239 222 224 238 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) )
240 239 226 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
241 237 239 240 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
242 241 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
243 228 232 242 3eqtrd ⊢ ( 𝜑 → 𝐺 = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) )
244 215 227 243 3eqtr4d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 𝐺 )
245 102 57 92 volicon0 ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
246 244 245 oveq12d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
247 214 246 eqtrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
248 247 breq1d ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
249 211 248 mpbird ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
250 0le1 ⊢ 0 ≤ 1
251 250 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
252 15 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐸 )
253 30 31 251 252 addge0d ⊢ ( 𝜑 → 0 ≤ ( 1 + 𝐸 ) )
254 81 12 32 253 76 lemul2ad ⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
255 29 82 83 249 254 letrd ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) )