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 sselid ( 𝜑 → ( 𝐴 ( 𝐿𝑊 ) 𝐵 ) ∈ ℝ )
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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻 ‘ ( 𝐵𝑍 ) ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ∈ ( 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 sselid ( 𝜑𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
99 95 98 sselid ( 𝜑𝑆 ∈ ℝ* )
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 sselid ( ( 𝜑𝑘𝑌 ) → 𝑘𝑊 )
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 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) ) ) )