Metamath Proof Explorer


Theorem hoidmvlelem2

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem2.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
hoidmvlelem2.x ( 𝜑𝑋 ∈ Fin )
hoidmvlelem2.y ( 𝜑𝑌𝑋 )
hoidmvlelem2.z ( 𝜑𝑍 ∈ ( 𝑋𝑌 ) )
hoidmvlelem2.w 𝑊 = ( 𝑌 ∪ { 𝑍 } )
hoidmvlelem2.a ( 𝜑𝐴 : 𝑊 ⟶ ℝ )
hoidmvlelem2.b ( 𝜑𝐵 : 𝑊 ⟶ ℝ )
hoidmvlelem2.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem2.f 𝐹 = ( 𝑦𝑌 ↦ 0 )
hoidmvlelem2.j 𝐽 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
hoidmvlelem2.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem2.k 𝐾 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
hoidmvlelem2.r ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) ) ∈ ℝ )
hoidmvlelem2.h 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) )
hoidmvlelem2.g 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) )
hoidmvlelem2.e ( 𝜑𝐸 ∈ ℝ+ )
hoidmvlelem2.u 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) }
hoidmvlelem2.su ( 𝜑𝑆𝑈 )
hoidmvlelem2.sb ( 𝜑𝑆 < ( 𝐵𝑍 ) )
hoidmvlelem2.p 𝑃 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
hoidmvlelem2.m ( 𝜑𝑀 ∈ ℕ )
hoidmvlelem2.le ( 𝜑𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) )
hoidmvlelem2.O 𝑂 = ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
hoidmvlelem2.v 𝑉 = ( { ( 𝐵𝑍 ) } ∪ 𝑂 )
hoidmvlelem2.q 𝑄 = inf ( 𝑉 , ℝ , < )
Assertion hoidmvlelem2 ( 𝜑 → ∃ 𝑢𝑈 𝑆 < 𝑢 )

Proof

Step Hyp Ref Expression
1 hoidmvlelem2.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
2 hoidmvlelem2.x ( 𝜑𝑋 ∈ Fin )
3 hoidmvlelem2.y ( 𝜑𝑌𝑋 )
4 hoidmvlelem2.z ( 𝜑𝑍 ∈ ( 𝑋𝑌 ) )
5 hoidmvlelem2.w 𝑊 = ( 𝑌 ∪ { 𝑍 } )
6 hoidmvlelem2.a ( 𝜑𝐴 : 𝑊 ⟶ ℝ )
7 hoidmvlelem2.b ( 𝜑𝐵 : 𝑊 ⟶ ℝ )
8 hoidmvlelem2.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
9 hoidmvlelem2.f 𝐹 = ( 𝑦𝑌 ↦ 0 )
10 hoidmvlelem2.j 𝐽 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
11 hoidmvlelem2.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
12 hoidmvlelem2.k 𝐾 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
13 hoidmvlelem2.r ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) ) ∈ ℝ )
14 hoidmvlelem2.h 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) )
15 hoidmvlelem2.g 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) )
16 hoidmvlelem2.e ( 𝜑𝐸 ∈ ℝ+ )
17 hoidmvlelem2.u 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) }
18 hoidmvlelem2.su ( 𝜑𝑆𝑈 )
19 hoidmvlelem2.sb ( 𝜑𝑆 < ( 𝐵𝑍 ) )
20 hoidmvlelem2.p 𝑃 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
21 hoidmvlelem2.m ( 𝜑𝑀 ∈ ℕ )
22 hoidmvlelem2.le ( 𝜑𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) )
23 hoidmvlelem2.O 𝑂 = ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
24 hoidmvlelem2.v 𝑉 = ( { ( 𝐵𝑍 ) } ∪ 𝑂 )
25 hoidmvlelem2.q 𝑄 = inf ( 𝑉 , ℝ , < )
26 snidg ( 𝑍 ∈ ( 𝑋𝑌 ) → 𝑍 ∈ { 𝑍 } )
27 4 26 syl ( 𝜑𝑍 ∈ { 𝑍 } )
28 elun2 ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
29 27 28 syl ( 𝜑𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
30 29 5 eleqtrrdi ( 𝜑𝑍𝑊 )
31 6 30 ffvelrnd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ )
32 7 30 ffvelrnd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ )
33 32 snssd ( 𝜑 → { ( 𝐵𝑍 ) } ⊆ ℝ )
34 nfv 𝑖 𝜑
35 eqid ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) = ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
36 simpl ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → 𝜑 )
37 fz1ssnn ( 1 ... 𝑀 ) ⊆ ℕ
38 elrabi ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → 𝑖 ∈ ( 1 ... 𝑀 ) )
39 37 38 sseldi ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → 𝑖 ∈ ℕ )
40 39 adantl ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → 𝑖 ∈ ℕ )
41 eleq1w ( 𝑗 = 𝑖 → ( 𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ ) )
42 41 anbi2d ( 𝑗 = 𝑖 → ( ( 𝜑𝑗 ∈ ℕ ) ↔ ( 𝜑𝑖 ∈ ℕ ) ) )
43 fveq2 ( 𝑗 = 𝑖 → ( 𝐷𝑗 ) = ( 𝐷𝑖 ) )
44 43 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
45 44 eleq1d ( 𝑗 = 𝑖 → ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ ↔ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ ) )
46 42 45 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ ) ) )
47 11 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
48 elmapi ( ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷𝑗 ) : 𝑊 ⟶ ℝ )
49 47 48 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) : 𝑊 ⟶ ℝ )
50 30 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑍𝑊 )
51 49 50 ffvelrnd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
52 46 51 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ )
53 36 40 52 syl2anc ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ )
54 34 35 53 rnmptssd ( 𝜑 → ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ⊆ ℝ )
55 23 54 eqsstrid ( 𝜑𝑂 ⊆ ℝ )
56 33 55 unssd ( 𝜑 → ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) ⊆ ℝ )
57 24 56 eqsstrid ( 𝜑𝑉 ⊆ ℝ )
58 ltso < Or ℝ
59 58 a1i ( 𝜑 → < Or ℝ )
60 snfi { ( 𝐵𝑍 ) } ∈ Fin
61 60 a1i ( 𝜑 → { ( 𝐵𝑍 ) } ∈ Fin )
62 fzfi ( 1 ... 𝑀 ) ∈ Fin
63 rabfi ( ( 1 ... 𝑀 ) ∈ Fin → { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∈ Fin )
64 62 63 ax-mp { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∈ Fin
65 64 a1i ( 𝜑 → { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∈ Fin )
66 35 rnmptfi ( { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∈ Fin → ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ∈ Fin )
67 65 66 syl ( 𝜑 → ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ∈ Fin )
68 23 67 eqeltrid ( 𝜑𝑂 ∈ Fin )
69 unfi ( ( { ( 𝐵𝑍 ) } ∈ Fin ∧ 𝑂 ∈ Fin ) → ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) ∈ Fin )
70 61 68 69 syl2anc ( 𝜑 → ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) ∈ Fin )
71 24 70 eqeltrid ( 𝜑𝑉 ∈ Fin )
72 fvex ( 𝐵𝑍 ) ∈ V
73 72 snid ( 𝐵𝑍 ) ∈ { ( 𝐵𝑍 ) }
74 elun1 ( ( 𝐵𝑍 ) ∈ { ( 𝐵𝑍 ) } → ( 𝐵𝑍 ) ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) )
75 73 74 ax-mp ( 𝐵𝑍 ) ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 )
76 24 eqcomi ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) = 𝑉
77 75 76 eleqtri ( 𝐵𝑍 ) ∈ 𝑉
78 77 a1i ( 𝜑 → ( 𝐵𝑍 ) ∈ 𝑉 )
79 ne0i ( ( 𝐵𝑍 ) ∈ 𝑉𝑉 ≠ ∅ )
80 78 79 syl ( 𝜑𝑉 ≠ ∅ )
81 fiinfcl ( ( < Or ℝ ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ∧ 𝑉 ⊆ ℝ ) ) → inf ( 𝑉 , ℝ , < ) ∈ 𝑉 )
82 59 71 80 57 81 syl13anc ( 𝜑 → inf ( 𝑉 , ℝ , < ) ∈ 𝑉 )
83 25 82 eqeltrid ( 𝜑𝑄𝑉 )
84 57 83 sseldd ( 𝜑𝑄 ∈ ℝ )
85 ssrab2 { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
86 17 85 eqsstri 𝑈 ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
87 86 a1i ( 𝜑𝑈 ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
88 31 32 iccssred ( 𝜑 → ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ⊆ ℝ )
89 87 88 sstrd ( 𝜑𝑈 ⊆ ℝ )
90 89 18 sseldd ( 𝜑𝑆 ∈ ℝ )
91 31 rexrd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ* )
92 32 rexrd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ* )
93 86 18 sseldi ( 𝜑𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
94 iccgelb ( ( ( 𝐴𝑍 ) ∈ ℝ* ∧ ( 𝐵𝑍 ) ∈ ℝ*𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ) → ( 𝐴𝑍 ) ≤ 𝑆 )
95 91 92 93 94 syl3anc ( 𝜑 → ( 𝐴𝑍 ) ≤ 𝑆 )
96 19 adantr ( ( 𝜑𝑥 = ( 𝐵𝑍 ) ) → 𝑆 < ( 𝐵𝑍 ) )
97 id ( 𝑥 = ( 𝐵𝑍 ) → 𝑥 = ( 𝐵𝑍 ) )
98 97 eqcomd ( 𝑥 = ( 𝐵𝑍 ) → ( 𝐵𝑍 ) = 𝑥 )
99 98 adantl ( ( 𝜑𝑥 = ( 𝐵𝑍 ) ) → ( 𝐵𝑍 ) = 𝑥 )
100 96 99 breqtrd ( ( 𝜑𝑥 = ( 𝐵𝑍 ) ) → 𝑆 < 𝑥 )
101 100 adantlr ( ( ( 𝜑𝑥𝑉 ) ∧ 𝑥 = ( 𝐵𝑍 ) ) → 𝑆 < 𝑥 )
102 simpll ( ( ( 𝜑𝑥𝑉 ) ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → 𝜑 )
103 id ( 𝑥𝑉𝑥𝑉 )
104 103 24 eleqtrdi ( 𝑥𝑉𝑥 ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) )
105 104 adantr ( ( 𝑥𝑉 ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → 𝑥 ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) )
106 elsni ( 𝑥 ∈ { ( 𝐵𝑍 ) } → 𝑥 = ( 𝐵𝑍 ) )
107 106 con3i ( ¬ 𝑥 = ( 𝐵𝑍 ) → ¬ 𝑥 ∈ { ( 𝐵𝑍 ) } )
108 107 adantl ( ( 𝑥𝑉 ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → ¬ 𝑥 ∈ { ( 𝐵𝑍 ) } )
109 elunnel1 ( ( 𝑥 ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) ∧ ¬ 𝑥 ∈ { ( 𝐵𝑍 ) } ) → 𝑥𝑂 )
110 105 108 109 syl2anc ( ( 𝑥𝑉 ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → 𝑥𝑂 )
111 110 adantll ( ( ( 𝜑𝑥𝑉 ) ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → 𝑥𝑂 )
112 id ( 𝑥𝑂𝑥𝑂 )
113 112 23 eleqtrdi ( 𝑥𝑂𝑥 ∈ ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
114 vex 𝑥 ∈ V
115 35 elrnmpt ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ↔ ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
116 114 115 ax-mp ( 𝑥 ∈ ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ↔ ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
117 113 116 sylib ( 𝑥𝑂 → ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
118 117 adantl ( ( 𝜑𝑥𝑂 ) → ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
119 fveq2 ( 𝑗 = 𝑖 → ( 𝐶𝑗 ) = ( 𝐶𝑖 ) )
120 119 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
121 120 eleq1d ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ ↔ ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ ) )
122 42 121 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ ) ) )
123 8 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
124 elmapi ( ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶𝑗 ) : 𝑊 ⟶ ℝ )
125 123 124 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) : 𝑊 ⟶ ℝ )
126 125 50 ffvelrnd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ )
127 122 126 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ )
128 127 rexrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ* )
129 36 40 128 syl2anc ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ* )
130 52 rexrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ* )
131 36 40 130 syl2anc ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ* )
132 120 44 oveq12d ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
133 132 eleq2d ( 𝑗 = 𝑖 → ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
134 133 elrab ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↔ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
135 134 biimpi ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
136 135 simprd ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
137 136 adantl ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
138 icoltub ( ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) ∈ ℝ* ∧ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ∈ ℝ*𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) → 𝑆 < ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
139 129 131 137 138 syl3anc ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ) → 𝑆 < ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
140 139 3adant3 ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∧ 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) → 𝑆 < ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
141 id ( 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) → 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
142 141 eqcomd ( 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) = 𝑥 )
143 142 3ad2ant3 ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∧ 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) → ( ( 𝐷𝑖 ) ‘ 𝑍 ) = 𝑥 )
144 140 143 breqtrd ( ( 𝜑𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∧ 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) → 𝑆 < 𝑥 )
145 144 3exp ( 𝜑 → ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → ( 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) → 𝑆 < 𝑥 ) ) )
146 145 adantr ( ( 𝜑𝑥𝑂 ) → ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } → ( 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) → 𝑆 < 𝑥 ) ) )
147 146 rexlimdv ( ( 𝜑𝑥𝑂 ) → ( ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } 𝑥 = ( ( 𝐷𝑖 ) ‘ 𝑍 ) → 𝑆 < 𝑥 ) )
148 118 147 mpd ( ( 𝜑𝑥𝑂 ) → 𝑆 < 𝑥 )
149 102 111 148 syl2anc ( ( ( 𝜑𝑥𝑉 ) ∧ ¬ 𝑥 = ( 𝐵𝑍 ) ) → 𝑆 < 𝑥 )
150 101 149 pm2.61dan ( ( 𝜑𝑥𝑉 ) → 𝑆 < 𝑥 )
151 150 ralrimiva ( 𝜑 → ∀ 𝑥𝑉 𝑆 < 𝑥 )
152 breq2 ( 𝑥 = inf ( 𝑉 , ℝ , < ) → ( 𝑆 < 𝑥𝑆 < inf ( 𝑉 , ℝ , < ) ) )
153 152 rspcva ( ( inf ( 𝑉 , ℝ , < ) ∈ 𝑉 ∧ ∀ 𝑥𝑉 𝑆 < 𝑥 ) → 𝑆 < inf ( 𝑉 , ℝ , < ) )
154 82 151 153 syl2anc ( 𝜑𝑆 < inf ( 𝑉 , ℝ , < ) )
155 25 eqcomi inf ( 𝑉 , ℝ , < ) = 𝑄
156 155 a1i ( 𝜑 → inf ( 𝑉 , ℝ , < ) = 𝑄 )
157 154 156 breqtrd ( 𝜑𝑆 < 𝑄 )
158 31 90 84 95 157 lelttrd ( 𝜑 → ( 𝐴𝑍 ) < 𝑄 )
159 31 84 158 ltled ( 𝜑 → ( 𝐴𝑍 ) ≤ 𝑄 )
160 fiminre ( ( 𝑉 ⊆ ℝ ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ∃ 𝑥𝑉𝑦𝑉 𝑥𝑦 )
161 57 71 80 160 syl3anc ( 𝜑 → ∃ 𝑥𝑉𝑦𝑉 𝑥𝑦 )
162 lbinfle ( ( 𝑉 ⊆ ℝ ∧ ∃ 𝑥𝑉𝑦𝑉 𝑥𝑦 ∧ ( 𝐵𝑍 ) ∈ 𝑉 ) → inf ( 𝑉 , ℝ , < ) ≤ ( 𝐵𝑍 ) )
163 57 161 78 162 syl3anc ( 𝜑 → inf ( 𝑉 , ℝ , < ) ≤ ( 𝐵𝑍 ) )
164 25 163 eqbrtrid ( 𝜑𝑄 ≤ ( 𝐵𝑍 ) )
165 31 32 84 159 164 eliccd ( 𝜑𝑄 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
166 84 recnd ( 𝜑𝑄 ∈ ℂ )
167 90 recnd ( 𝜑𝑆 ∈ ℂ )
168 31 recnd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℂ )
169 166 167 168 npncand ( 𝜑 → ( ( 𝑄𝑆 ) + ( 𝑆 − ( 𝐴𝑍 ) ) ) = ( 𝑄 − ( 𝐴𝑍 ) ) )
170 169 eqcomd ( 𝜑 → ( 𝑄 − ( 𝐴𝑍 ) ) = ( ( 𝑄𝑆 ) + ( 𝑆 − ( 𝐴𝑍 ) ) ) )
171 170 oveq2d ( 𝜑 → ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) = ( 𝐺 · ( ( 𝑄𝑆 ) + ( 𝑆 − ( 𝐴𝑍 ) ) ) ) )
172 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
173 2 3 ssfid ( 𝜑𝑌 ∈ Fin )
174 ssun1 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } )
175 174 5 sseqtrri 𝑌𝑊
176 175 a1i ( 𝜑𝑌𝑊 )
177 6 176 fssresd ( 𝜑 → ( 𝐴𝑌 ) : 𝑌 ⟶ ℝ )
178 7 176 fssresd ( 𝜑 → ( 𝐵𝑌 ) : 𝑌 ⟶ ℝ )
179 1 173 177 178 hoidmvcl ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ∈ ( 0 [,) +∞ ) )
180 15 179 eqeltrid ( 𝜑𝐺 ∈ ( 0 [,) +∞ ) )
181 172 180 sseldi ( 𝜑𝐺 ∈ ℝ )
182 181 recnd ( 𝜑𝐺 ∈ ℂ )
183 166 167 subcld ( 𝜑 → ( 𝑄𝑆 ) ∈ ℂ )
184 167 168 subcld ( 𝜑 → ( 𝑆 − ( 𝐴𝑍 ) ) ∈ ℂ )
185 182 183 184 adddid ( 𝜑 → ( 𝐺 · ( ( 𝑄𝑆 ) + ( 𝑆 − ( 𝐴𝑍 ) ) ) ) = ( ( 𝐺 · ( 𝑄𝑆 ) ) + ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ) )
186 182 183 mulcld ( 𝜑 → ( 𝐺 · ( 𝑄𝑆 ) ) ∈ ℂ )
187 182 184 mulcld ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ∈ ℂ )
188 186 187 addcomd ( 𝜑 → ( ( 𝐺 · ( 𝑄𝑆 ) ) + ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ) = ( ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) + ( 𝐺 · ( 𝑄𝑆 ) ) ) )
189 171 185 188 3eqtrd ( 𝜑 → ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) = ( ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) + ( 𝐺 · ( 𝑄𝑆 ) ) ) )
190 84 90 jca ( 𝜑 → ( 𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ ) )
191 resubcl ( ( 𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑄𝑆 ) ∈ ℝ )
192 190 191 syl ( 𝜑 → ( 𝑄𝑆 ) ∈ ℝ )
193 181 192 jca ( 𝜑 → ( 𝐺 ∈ ℝ ∧ ( 𝑄𝑆 ) ∈ ℝ ) )
194 remulcl ( ( 𝐺 ∈ ℝ ∧ ( 𝑄𝑆 ) ∈ ℝ ) → ( 𝐺 · ( 𝑄𝑆 ) ) ∈ ℝ )
195 193 194 syl ( 𝜑 → ( 𝐺 · ( 𝑄𝑆 ) ) ∈ ℝ )
196 90 31 jca ( 𝜑 → ( 𝑆 ∈ ℝ ∧ ( 𝐴𝑍 ) ∈ ℝ ) )
197 resubcl ( ( 𝑆 ∈ ℝ ∧ ( 𝐴𝑍 ) ∈ ℝ ) → ( 𝑆 − ( 𝐴𝑍 ) ) ∈ ℝ )
198 196 197 syl ( 𝜑 → ( 𝑆 − ( 𝐴𝑍 ) ) ∈ ℝ )
199 181 198 jca ( 𝜑 → ( 𝐺 ∈ ℝ ∧ ( 𝑆 − ( 𝐴𝑍 ) ) ∈ ℝ ) )
200 remulcl ( ( 𝐺 ∈ ℝ ∧ ( 𝑆 − ( 𝐴𝑍 ) ) ∈ ℝ ) → ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ∈ ℝ )
201 199 200 syl ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ∈ ℝ )
202 195 201 jca ( 𝜑 → ( ( 𝐺 · ( 𝑄𝑆 ) ) ∈ ℝ ∧ ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ∈ ℝ ) )
203 readdcl ( ( ( 𝐺 · ( 𝑄𝑆 ) ) ∈ ℝ ∧ ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ∈ ℝ ) → ( ( 𝐺 · ( 𝑄𝑆 ) ) + ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ) ∈ ℝ )
204 202 203 syl ( 𝜑 → ( ( 𝐺 · ( 𝑄𝑆 ) ) + ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ) ∈ ℝ )
205 188 204 eqeltrrd ( 𝜑 → ( ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) + ( 𝐺 · ( 𝑄𝑆 ) ) ) ∈ ℝ )
206 1red ( 𝜑 → 1 ∈ ℝ )
207 16 rpred ( 𝜑𝐸 ∈ ℝ )
208 206 207 readdcld ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ )
209 4 eldifbd ( 𝜑 → ¬ 𝑍𝑌 )
210 30 209 eldifd ( 𝜑𝑍 ∈ ( 𝑊𝑌 ) )
211 1 173 210 5 8 11 13 14 90 sge0hsphoire ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
212 208 211 remulcld ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ∈ ℝ )
213 fzfid ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
214 192 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄𝑆 ) ∈ ℝ )
215 simpl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
216 elfznn ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
217 216 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℕ )
218 id ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
219 ovexd ( 𝑗 ∈ ℕ → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ V )
220 20 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ V ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
221 218 219 220 syl2anc ( 𝑗 ∈ ℕ → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
222 221 adantl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
223 173 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑌 ∈ Fin )
224 175 a1i ( ( 𝜑𝑗 ∈ ℕ ) → 𝑌𝑊 )
225 125 224 fssresd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
226 225 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
227 iftrue ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
228 227 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
229 228 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) )
230 226 229 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
231 0red ( ( 𝜑𝑦𝑌 ) → 0 ∈ ℝ )
232 231 9 fmptd ( 𝜑𝐹 : 𝑌 ⟶ ℝ )
233 232 ad2antrr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝐹 : 𝑌 ⟶ ℝ )
234 iffalse ( ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
235 234 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
236 235 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ 𝐹 : 𝑌 ⟶ ℝ ) )
237 233 236 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
238 230 237 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
239 simpr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
240 fvex ( 𝐶𝑗 ) ∈ V
241 240 resex ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ V
242 241 a1i ( 𝜑 → ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ V )
243 2 3 ssexd ( 𝜑𝑌 ∈ V )
244 mptexg ( 𝑌 ∈ V → ( 𝑦𝑌 ↦ 0 ) ∈ V )
245 243 244 syl ( 𝜑 → ( 𝑦𝑌 ↦ 0 ) ∈ V )
246 9 245 eqeltrid ( 𝜑𝐹 ∈ V )
247 242 246 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
248 247 adantr ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
249 10 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
250 239 248 249 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
251 250 feq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ ↔ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ) )
252 238 251 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
253 49 224 fssresd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
254 253 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐷𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
255 iftrue ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
256 255 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
257 256 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ ( ( 𝐷𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) )
258 254 257 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
259 iffalse ( ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
260 259 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
261 260 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ 𝐹 : 𝑌 ⟶ ℝ ) )
262 233 261 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
263 258 262 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
264 fvex ( 𝐷𝑗 ) ∈ V
265 264 resex ( ( 𝐷𝑗 ) ↾ 𝑌 ) ∈ V
266 265 a1i ( 𝜑 → ( ( 𝐷𝑗 ) ↾ 𝑌 ) ∈ V )
267 266 246 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
268 267 adantr ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
269 12 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
270 239 268 269 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
271 270 feq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ ↔ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ) )
272 263 271 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ )
273 1 223 252 272 hoidmvcl ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ ( 0 [,) +∞ ) )
274 222 273 eqeltrd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 0 [,) +∞ ) )
275 172 274 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ℝ )
276 215 217 275 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃𝑗 ) ∈ ℝ )
277 214 276 remulcld ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℝ )
278 213 277 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℝ )
279 208 278 remulcld ( 𝜑 → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ∈ ℝ )
280 212 279 readdcld ( 𝜑 → ( ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ∈ ℝ )
281 1 173 210 5 8 11 13 14 84 sge0hsphoire ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
282 208 281 remulcld ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ∈ ℝ )
283 18 17 eleqtrdi ( 𝜑𝑆 ∈ { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } )
284 oveq1 ( 𝑧 = 𝑆 → ( 𝑧 − ( 𝐴𝑍 ) ) = ( 𝑆 − ( 𝐴𝑍 ) ) )
285 284 oveq2d ( 𝑧 = 𝑆 → ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) = ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) )
286 fveq2 ( 𝑧 = 𝑆 → ( 𝐻𝑧 ) = ( 𝐻𝑆 ) )
287 286 fveq1d ( 𝑧 = 𝑆 → ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) = ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) )
288 287 oveq2d ( 𝑧 = 𝑆 → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) )
289 288 mpteq2dv ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) )
290 289 fveq2d ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
291 290 oveq2d ( 𝑧 = 𝑆 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
292 285 291 breq12d ( 𝑧 = 𝑆 → ( ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
293 292 elrab ( 𝑆 ∈ { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } ↔ ( 𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
294 283 293 sylib ( 𝜑 → ( 𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
295 294 simprd ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
296 213 276 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ∈ ℝ )
297 208 296 remulcld ( 𝜑 → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) ∈ ℝ )
298 0red ( 𝜑 → 0 ∈ ℝ )
299 90 84 posdifd ( 𝜑 → ( 𝑆 < 𝑄 ↔ 0 < ( 𝑄𝑆 ) ) )
300 157 299 mpbid ( 𝜑 → 0 < ( 𝑄𝑆 ) )
301 298 192 300 ltled ( 𝜑 → 0 ≤ ( 𝑄𝑆 ) )
302 181 297 192 301 22 lemul1ad ( 𝜑 → ( 𝐺 · ( 𝑄𝑆 ) ) ≤ ( ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) · ( 𝑄𝑆 ) ) )
303 208 recnd ( 𝜑 → ( 1 + 𝐸 ) ∈ ℂ )
304 296 recnd ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ∈ ℂ )
305 303 304 183 mulassd ( 𝜑 → ( ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) · ( 𝑄𝑆 ) ) = ( ( 1 + 𝐸 ) · ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) ) )
306 276 recnd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃𝑗 ) ∈ ℂ )
307 213 183 306 fsummulc1 ( 𝜑 → ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) )
308 183 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄𝑆 ) ∈ ℂ )
309 306 308 mulcomd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) = ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) )
310 309 sumeq2dv ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) )
311 307 310 eqtrd ( 𝜑 → ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) )
312 311 oveq2d ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) · ( 𝑄𝑆 ) ) ) = ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
313 305 312 eqtrd ( 𝜑 → ( ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑃𝑗 ) ) · ( 𝑄𝑆 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
314 302 313 breqtrd ( 𝜑 → ( 𝐺 · ( 𝑄𝑆 ) ) ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
315 201 195 212 279 295 314 leadd12dd ( 𝜑 → ( ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) + ( 𝐺 · ( 𝑄𝑆 ) ) ) ≤ ( ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
316 nnsplit ( 𝑀 ∈ ℕ → ℕ = ( ( 1 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
317 21 316 syl ( 𝜑 → ℕ = ( ( 1 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
318 uncom ( ( 1 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) )
319 318 a1i ( 𝜑 → ( ( 1 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) )
320 317 319 eqtr2d ( 𝜑 → ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) = ℕ )
321 320 eqcomd ( 𝜑 → ℕ = ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) )
322 321 mpteq1d ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) )
323 322 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
324 nfv 𝑗 𝜑
325 fvexd ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ∈ V )
326 ovexd ( 𝜑 → ( 1 ... 𝑀 ) ∈ V )
327 incom ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) = ( ( 1 ... 𝑀 ) ∩ ( ℤ ‘ ( 𝑀 + 1 ) ) )
328 nnuzdisj ( ( 1 ... 𝑀 ) ∩ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = ∅
329 327 328 eqtri ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅
330 329 a1i ( 𝜑 → ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
331 icossicc ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
332 ssid ( 0 [,) +∞ ) ⊆ ( 0 [,) +∞ )
333 simpl ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → 𝜑 )
334 21 peano2nnd ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
335 uznnssnn ( ( 𝑀 + 1 ) ∈ ℕ → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ )
336 334 335 syl ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ )
337 336 adantr ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ )
338 simpr ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
339 337 338 sseldd ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → 𝑗 ∈ ℕ )
340 snfi { 𝑍 } ∈ Fin
341 340 a1i ( 𝜑 → { 𝑍 } ∈ Fin )
342 unfi ( ( 𝑌 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
343 173 341 342 syl2anc ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
344 5 343 eqeltrid ( 𝜑𝑊 ∈ Fin )
345 344 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
346 eleq1w ( 𝑗 = 𝑙 → ( 𝑗𝑌𝑙𝑌 ) )
347 fveq2 ( 𝑗 = 𝑙 → ( 𝑐𝑗 ) = ( 𝑐𝑙 ) )
348 347 breq1d ( 𝑗 = 𝑙 → ( ( 𝑐𝑗 ) ≤ 𝑥 ↔ ( 𝑐𝑙 ) ≤ 𝑥 ) )
349 348 347 ifbieq1d ( 𝑗 = 𝑙 → if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) = if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) )
350 346 347 349 ifbieq12d ( 𝑗 = 𝑙 → if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) = if ( 𝑙𝑌 , ( 𝑐𝑙 ) , if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) ) )
351 350 cbvmptv ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) = ( 𝑙𝑊 ↦ if ( 𝑙𝑌 , ( 𝑐𝑙 ) , if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) ) )
352 351 mpteq2i ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑙𝑊 ↦ if ( 𝑙𝑌 , ( 𝑐𝑙 ) , if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) ) ) )
353 352 mpteq2i ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑙𝑊 ↦ if ( 𝑙𝑌 , ( 𝑐𝑙 ) , if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) ) ) ) )
354 14 353 eqtri 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑙𝑊 ↦ if ( 𝑙𝑌 , ( 𝑐𝑙 ) , if ( ( 𝑐𝑙 ) ≤ 𝑥 , ( 𝑐𝑙 ) , 𝑥 ) ) ) ) )
355 90 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
356 354 355 345 49 hsphoif ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) : 𝑊 ⟶ ℝ )
357 1 345 125 356 hoidmvcl ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
358 333 339 357 syl2anc ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
359 332 358 sseldi ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
360 331 359 sseldi ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
361 215 217 357 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
362 331 361 sseldi ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
363 324 325 326 330 360 362 sge0splitmpt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
364 nnex ℕ ∈ V
365 364 a1i ( 𝜑 → ℕ ∈ V )
366 331 357 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
367 324 365 366 211 336 sge0ssrempt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
368 37 a1i ( 𝜑 → ( 1 ... 𝑀 ) ⊆ ℕ )
369 324 365 366 211 368 sge0ssrempt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
370 rexadd ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
371 367 369 370 syl2anc ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
372 323 363 371 3eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
373 372 oveq2d ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
374 373 oveq1d ( 𝜑 → ( ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
375 372 211 eqeltrrd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ∈ ℝ )
376 375 recnd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ∈ ℂ )
377 278 recnd ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℂ )
378 303 376 377 adddid ( 𝜑 → ( ( 1 + 𝐸 ) · ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
379 378 eqcomd ( 𝜑 → ( ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( 1 + 𝐸 ) · ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
380 367 recnd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℂ )
381 369 recnd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℂ )
382 380 381 377 addassd ( 𝜑 → ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
383 213 361 sge0fsummpt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) )
384 383 oveq1d ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
385 ax-resscn ℝ ⊆ ℂ
386 172 385 sstri ( 0 [,) +∞ ) ⊆ ℂ
387 386 357 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℂ )
388 215 217 387 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℂ )
389 192 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑄𝑆 ) ∈ ℝ )
390 389 275 remulcld ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℝ )
391 390 recnd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℂ )
392 217 391 syldan ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ∈ ℂ )
393 213 388 392 fsumadd ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
394 393 eqcomd ( 𝜑 → ( Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
395 384 394 eqtrd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
396 395 oveq2d ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
397 382 396 eqtrd ( 𝜑 → ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) )
398 397 oveq2d ( 𝜑 → ( ( 1 + 𝐸 ) · ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ) )
399 374 379 398 3eqtrd ( 𝜑 → ( ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) = ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ) )
400 172 357 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℝ )
401 400 390 readdcld ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ∈ ℝ )
402 215 217 401 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ∈ ℝ )
403 213 402 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ∈ ℝ )
404 367 403 readdcld ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ∈ ℝ )
405 0le1 0 ≤ 1
406 405 a1i ( 𝜑 → 0 ≤ 1 )
407 16 rpge0d ( 𝜑 → 0 ≤ 𝐸 )
408 206 207 406 407 addge0d ( 𝜑 → 0 ≤ ( 1 + 𝐸 ) )
409 84 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑄 ∈ ℝ )
410 354 409 345 49 hsphoif ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) : 𝑊 ⟶ ℝ )
411 1 345 125 410 hoidmvcl ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
412 331 411 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
413 324 365 412 281 336 sge0ssrempt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
414 172 411 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℝ )
415 215 217 414 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℝ )
416 213 415 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ℝ )
417 333 339 412 syl2anc ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
418 210 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊𝑌 ) )
419 90 84 157 ltled ( 𝜑𝑆𝑄 )
420 419 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑆𝑄 )
421 1 345 418 5 355 409 420 354 125 49 hsphoidmvle2 ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
422 333 339 421 syl2anc ( ( 𝜑𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
423 324 325 360 417 422 sge0lempt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
424 215 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) = 0 ) → 𝜑 )
425 217 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) = 0 ) → 𝑗 ∈ ℕ )
426 simpr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) = 0 ) → ( 𝑃𝑗 ) = 0 )
427 oveq2 ( ( 𝑃𝑗 ) = 0 → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) = ( ( 𝑄𝑆 ) · 0 ) )
428 427 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) = ( ( 𝑄𝑆 ) · 0 ) )
429 183 mul01d ( 𝜑 → ( ( 𝑄𝑆 ) · 0 ) = 0 )
430 429 ad2antrr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( 𝑄𝑆 ) · 0 ) = 0 )
431 428 430 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) = 0 )
432 431 oveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + 0 ) )
433 387 addid1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + 0 ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) )
434 433 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + 0 ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) )
435 432 434 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) )
436 421 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
437 435 436 eqbrtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
438 424 425 426 437 syl21anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
439 simpl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( 𝑃𝑗 ) = 0 ) → ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) )
440 neqne ( ¬ ( 𝑃𝑗 ) = 0 → ( 𝑃𝑗 ) ≠ 0 )
441 440 adantl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( 𝑃𝑗 ) = 0 ) → ( 𝑃𝑗 ) ≠ 0 )
442 402 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ∈ ℝ )
443 215 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝜑 )
444 217 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑗 ∈ ℕ )
445 simpr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝑃𝑗 ) ≠ 0 )
446 4 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑋𝑌 ) )
447 209 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ¬ 𝑍𝑌 )
448 eqid 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) )
449 1 223 446 447 5 125 356 448 hoiprodp1 ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) = ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) )
450 449 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) = ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) )
451 222 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
452 223 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑌 ∈ Fin )
453 222 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
454 fveq2 ( 𝑌 = ∅ → ( 𝐿𝑌 ) = ( 𝐿 ‘ ∅ ) )
455 454 oveqd ( 𝑌 = ∅ → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿 ‘ ∅ ) ( 𝐾𝑗 ) ) )
456 455 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿 ‘ ∅ ) ( 𝐾𝑗 ) ) )
457 252 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
458 id ( 𝑌 = ∅ → 𝑌 = ∅ )
459 458 eqcomd ( 𝑌 = ∅ → ∅ = 𝑌 )
460 459 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ∅ = 𝑌 )
461 460 feq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( ( 𝐽𝑗 ) : ∅ ⟶ ℝ ↔ ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ ) )
462 457 461 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝐽𝑗 ) : ∅ ⟶ ℝ )
463 272 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ )
464 460 feq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( ( 𝐾𝑗 ) : ∅ ⟶ ℝ ↔ ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ ) )
465 463 464 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝐾𝑗 ) : ∅ ⟶ ℝ )
466 1 462 465 hoidmv0val ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( ( 𝐽𝑗 ) ( 𝐿 ‘ ∅ ) ( 𝐾𝑗 ) ) = 0 )
467 453 456 466 3eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑌 = ∅ ) → ( 𝑃𝑗 ) = 0 )
468 467 adantlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑌 = ∅ ) → ( 𝑃𝑗 ) = 0 )
469 neneq ( ( 𝑃𝑗 ) ≠ 0 → ¬ ( 𝑃𝑗 ) = 0 )
470 469 ad2antlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑌 = ∅ ) → ¬ ( 𝑃𝑗 ) = 0 )
471 468 470 pm2.65da ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ¬ 𝑌 = ∅ )
472 471 neqned ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑌 ≠ ∅ )
473 252 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
474 272 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ )
475 1 452 472 473 474 hoidmvn0val ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
476 250 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
477 222 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
478 250 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
479 478 235 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = 𝐹 )
480 270 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
481 480 260 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = 𝐹 )
482 479 481 oveq12d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( 𝐹 ( 𝐿𝑌 ) 𝐹 ) )
483 1 173 232 hoidmvval0b ( 𝜑 → ( 𝐹 ( 𝐿𝑌 ) 𝐹 ) = 0 )
484 483 ad2antrr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐹 ( 𝐿𝑌 ) 𝐹 ) = 0 )
485 477 482 484 3eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝑃𝑗 ) = 0 )
486 485 adantlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝑃𝑗 ) = 0 )
487 469 ad2antlr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ¬ ( 𝑃𝑗 ) = 0 )
488 486 487 condan ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
489 488 iftrued ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
490 476 489 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐽𝑗 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
491 490 fveq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
492 491 adantr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
493 fvres ( 𝑘𝑌 → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
494 493 adantl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
495 492 494 eqtrd ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
496 270 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
497 488 255 syl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
498 496 497 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝐾𝑗 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
499 498 fveq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
500 499 adantr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
501 fvres ( 𝑘𝑌 → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
502 501 adantl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
503 500 502 eqtrd ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
504 495 503 oveq12d ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
505 504 fveq2d ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ 𝑘𝑌 ) → ( vol ‘ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
506 505 prodeq2dv ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
507 475 506 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
508 355 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → 𝑆 ∈ ℝ )
509 345 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → 𝑊 ∈ Fin )
510 49 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( 𝐷𝑗 ) : 𝑊 ⟶ ℝ )
511 elun1 ( 𝑘𝑌𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
512 511 5 eleqtrrdi ( 𝑘𝑌𝑘𝑊 )
513 512 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → 𝑘𝑊 )
514 354 508 509 510 513 hsphoival ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑆 ) ) )
515 iftrue ( 𝑘𝑌 → if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑆 ) ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
516 515 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑆 ) ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
517 514 516 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
518 517 oveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
519 518 fveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
520 519 prodeq2dv ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
521 520 eqcomd ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) )
522 521 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) )
523 451 507 522 3eqtrrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑃𝑗 ) )
524 354 355 345 49 50 hsphoival ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) )
525 209 iffalsed ( 𝜑 → if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) = if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) )
526 525 adantr ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) = if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) )
527 524 526 eqtrd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) )
528 527 oveq2d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) )
529 528 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) )
530 126 rexrd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ* )
531 530 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ* )
532 51 rexrd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ* )
533 532 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ* )
534 icoltub ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ* ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ*𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝑆 < ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
535 531 533 488 534 syl3anc ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 < ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
536 355 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 ∈ ℝ )
537 51 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
538 536 537 ltnled ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝑆 < ( ( 𝐷𝑗 ) ‘ 𝑍 ) ↔ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 ) )
539 535 538 mpbid ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 )
540 539 iffalsed ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) = 𝑆 )
541 540 oveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑆 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑆 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) )
542 529 541 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) )
543 542 fveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) ) )
544 volico ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) ) = if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) )
545 126 536 544 syl2an ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) ) = if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) )
546 545 anabss5 ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑆 ) ) = if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) )
547 iftrue ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
548 547 adantl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
549 iffalse ( ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = 0 )
550 549 adantl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = 0 )
551 simpll ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( 𝜑𝑗 ∈ ℕ ) )
552 icogelb ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ* ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ*𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 )
553 531 533 488 552 syl3anc ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 )
554 553 adantr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 )
555 simpr ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 )
556 554 555 jca ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) )
557 551 126 syl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ )
558 551 355 syl ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → 𝑆 ∈ ℝ )
559 557 558 eqleltd ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 ↔ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) ) )
560 556 559 mpbird ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 )
561 id ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 )
562 561 eqcomd ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆𝑆 = ( ( 𝐶𝑗 ) ‘ 𝑍 ) )
563 562 oveq1d ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 → ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
564 563 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 ) → ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
565 385 126 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℂ )
566 565 subidd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = 0 )
567 566 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) = 0 )
568 564 567 eqtr2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( ( 𝐶𝑗 ) ‘ 𝑍 ) = 𝑆 ) → 0 = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
569 551 560 568 syl2anc ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → 0 = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
570 550 569 eqtrd ( ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 ) → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
571 548 570 pm2.61dan ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑆 , ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
572 543 546 571 3eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) = ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
573 523 572 oveq12d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) = ( ( 𝑃𝑗 ) · ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) )
574 386 274 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ℂ )
575 355 126 resubcld ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ∈ ℝ )
576 575 recnd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ∈ ℂ )
577 574 576 mulcomd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑃𝑗 ) · ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) = ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
578 577 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝑃𝑗 ) · ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) = ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
579 450 573 578 3eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
580 579 oveq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
581 183 adantr ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑄𝑆 ) ∈ ℂ )
582 576 581 574 adddird ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) · ( 𝑃𝑗 ) ) = ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) )
583 582 eqcomd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) · ( 𝑃𝑗 ) ) )
584 583 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) · ( 𝑃𝑗 ) ) )
585 576 581 addcomd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) = ( ( 𝑄𝑆 ) + ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) )
586 166 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑄 ∈ ℂ )
587 167 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑆 ∈ ℂ )
588 586 587 565 npncand ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑄𝑆 ) + ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) = ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
589 585 588 eqtrd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) = ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
590 589 oveq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) · ( 𝑃𝑗 ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
591 590 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝑆 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) + ( 𝑄𝑆 ) ) · ( 𝑃𝑗 ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
592 580 584 591 3eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
593 443 444 445 592 syl21anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
594 eqid 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) )
595 1 223 50 447 5 125 410 594 hoiprodp1 ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) = ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) )
596 215 217 595 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) = ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) )
597 596 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) = ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) )
598 507 eqcomd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
599 409 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → 𝑄 ∈ ℝ )
600 354 599 509 510 513 hsphoival ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑄 ) ) )
601 iftrue ( 𝑘𝑌 → if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑄 ) ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
602 601 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑘 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑘 ) , 𝑄 ) ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
603 600 602 eqtrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
604 603 oveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
605 604 fveq2d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑘𝑌 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
606 605 prodeq2dv ( ( 𝜑𝑗 ∈ ℕ ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
607 606 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
608 598 607 451 3eqtr4d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑃𝑗 ) )
609 443 444 445 608 syl21anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑃𝑗 ) )
610 354 409 345 49 50 hsphoival ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) ) )
611 217 610 syldan ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) ) )
612 611 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) ) )
613 209 iffalsed ( 𝜑 → if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) ) = if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) )
614 613 ad2antrr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( 𝑍𝑌 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) ) = if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) )
615 217 51 syldan ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
616 615 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
617 simpr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 )
618 616 617 eqled ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 )
619 618 iftrued ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
620 619 617 eqtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) = 𝑄 )
621 620 adantlr ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) = 𝑄 )
622 84 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑄 ∈ ℝ )
623 622 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → 𝑄 ∈ ℝ )
624 623 adantlr ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → 𝑄 ∈ ℝ )
625 615 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
626 625 adantlr ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ℝ )
627 25 a1i ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑄 = inf ( 𝑉 , ℝ , < ) )
628 443 57 syl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑉 ⊆ ℝ )
629 161 ad2antrr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∃ 𝑥𝑉𝑦𝑉 𝑥𝑦 )
630 simplr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
631 216 488 sylanl2 ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
632 630 631 jca ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
633 rabid ( 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↔ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
634 632 633 sylibr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } )
635 eqidd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
636 fveq2 ( 𝑖 = 𝑗 → ( 𝐷𝑖 ) = ( 𝐷𝑗 ) )
637 636 fveq1d ( 𝑖 = 𝑗 → ( ( 𝐷𝑖 ) ‘ 𝑍 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
638 637 eqeq2d ( 𝑖 = 𝑗 → ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) ↔ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
639 638 rspcev ( ( 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
640 634 635 639 syl2anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ∃ 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
641 fvexd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ V )
642 35 640 641 elrnmptd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ran ( 𝑖 ∈ { 𝑗 ∈ ( 1 ... 𝑀 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
643 642 23 eleqtrrdi ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ 𝑂 )
644 elun2 ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ 𝑂 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) )
645 643 644 syl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) )
646 76 a1i ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( { ( 𝐵𝑍 ) } ∪ 𝑂 ) = 𝑉 )
647 645 646 eleqtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ 𝑉 )
648 lbinfle ( ( 𝑉 ⊆ ℝ ∧ ∃ 𝑥𝑉𝑦𝑉 𝑥𝑦 ∧ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ∈ 𝑉 ) → inf ( 𝑉 , ℝ , < ) ≤ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
649 628 629 647 648 syl3anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → inf ( 𝑉 , ℝ , < ) ≤ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
650 627 649 eqbrtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑄 ≤ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
651 650 adantr ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → 𝑄 ≤ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
652 neqne ( ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≠ 𝑄 )
653 652 adantl ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≠ 𝑄 )
654 624 626 651 653 leneltd ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → 𝑄 < ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
655 624 626 ltnled ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ( 𝑄 < ( ( 𝐷𝑗 ) ‘ 𝑍 ) ↔ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 ) )
656 654 655 mpbid ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 )
657 656 iffalsed ( ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) ∧ ¬ ( ( 𝐷𝑗 ) ‘ 𝑍 ) = 𝑄 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) = 𝑄 )
658 621 657 pm2.61dan ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( ( ( 𝐷𝑗 ) ‘ 𝑍 ) ≤ 𝑄 , ( ( 𝐷𝑗 ) ‘ 𝑍 ) , 𝑄 ) = 𝑄 )
659 612 614 658 3eqtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) = 𝑄 )
660 659 oveq2d ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑄 ) )
661 660 fveq2d ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) = ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑄 ) ) )
662 215 217 126 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ )
663 662 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ )
664 443 84 syl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑄 ∈ ℝ )
665 volico ( ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑄 ) ) = if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑄 , ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) )
666 663 664 665 syl2anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) 𝑄 ) ) = if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑄 , ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) )
667 443 90 syl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 ∈ ℝ )
668 443 444 445 553 syl21anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ≤ 𝑆 )
669 443 157 syl ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → 𝑆 < 𝑄 )
670 663 667 664 668 669 lelttrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑄 )
671 670 iftrued ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → if ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) < 𝑄 , ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) , 0 ) = ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
672 661 666 671 3eqtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) = ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) )
673 609 672 oveq12d ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑘 ) ) ) · ( vol ‘ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ‘ 𝑍 ) ) ) ) = ( ( 𝑃𝑗 ) · ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) )
674 215 166 syl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑄 ∈ ℂ )
675 385 662 sseldi ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ‘ 𝑍 ) ∈ ℂ )
676 674 675 subcld ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ∈ ℂ )
677 306 676 mulcomd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑃𝑗 ) · ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
678 677 adantr ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝑃𝑗 ) · ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
679 597 673 678 3eqtrd ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝑄 − ( ( 𝐶𝑗 ) ‘ 𝑍 ) ) · ( 𝑃𝑗 ) ) )
680 593 679 eqtr4d ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
681 442 680 eqled ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ( 𝑃𝑗 ) ≠ 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
682 439 441 681 syl2anc ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( 𝑃𝑗 ) = 0 ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
683 438 682 pm2.61dan ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
684 213 402 415 683 fsumle ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
685 367 403 413 416 423 684 leadd12dd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ≤ ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) )
686 321 mpteq1d ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) )
687 686 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
688 217 412 syldan ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
689 324 325 326 330 417 688 sge0splitmpt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( ( ℤ ‘ ( 𝑀 + 1 ) ) ∪ ( 1 ... 𝑀 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
690 687 689 eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
691 215 217 411 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
692 213 691 sge0fsummpt ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
693 692 416 eqeltrd ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
694 rexadd ( ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
695 413 693 694 syl2anc ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
696 692 oveq2d ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + ( Σ^ ‘ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) )
697 690 695 696 3eqtrrd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
698 685 697 breqtrd ( 𝜑 → ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
699 404 281 208 408 698 lemul2ad ( 𝜑 → ( ( 1 + 𝐸 ) · ( ( Σ^ ‘ ( 𝑗 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) + Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) + ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
700 399 699 eqbrtrd ( 𝜑 → ( ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑆 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) + ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑄𝑆 ) · ( 𝑃𝑗 ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
701 205 280 282 315 700 letrd ( 𝜑 → ( ( 𝐺 · ( 𝑆 − ( 𝐴𝑍 ) ) ) + ( 𝐺 · ( 𝑄𝑆 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
702 189 701 eqbrtrd ( 𝜑 → ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
703 165 702 jca ( 𝜑 → ( 𝑄 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∧ ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
704 oveq1 ( 𝑧 = 𝑄 → ( 𝑧 − ( 𝐴𝑍 ) ) = ( 𝑄 − ( 𝐴𝑍 ) ) )
705 704 oveq2d ( 𝑧 = 𝑄 → ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) = ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) )
706 fveq2 ( 𝑧 = 𝑄 → ( 𝐻𝑧 ) = ( 𝐻𝑄 ) )
707 706 fveq1d ( 𝑧 = 𝑄 → ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) = ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) )
708 707 oveq2d ( 𝑧 = 𝑄 → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) )
709 708 mpteq2dv ( 𝑧 = 𝑄 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) )
710 709 fveq2d ( 𝑧 = 𝑄 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) )
711 710 oveq2d ( 𝑧 = 𝑄 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) )
712 705 711 breq12d ( 𝑧 = 𝑄 → ( ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
713 712 elrab ( 𝑄 ∈ { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } ↔ ( 𝑄 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∧ ( 𝐺 · ( 𝑄 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑄 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ) )
714 703 713 sylibr ( 𝜑𝑄 ∈ { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } )
715 714 17 eleqtrrdi ( 𝜑𝑄𝑈 )
716 breq2 ( 𝑢 = 𝑄 → ( 𝑆 < 𝑢𝑆 < 𝑄 ) )
717 716 rspcev ( ( 𝑄𝑈𝑆 < 𝑄 ) → ∃ 𝑢𝑈 𝑆 < 𝑢 )
718 715 157 717 syl2anc ( 𝜑 → ∃ 𝑢𝑈 𝑆 < 𝑢 )