Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmvlelem2 Structured version   Visualization version   GIF version

Theorem hoidmvlelem2 47605
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.)
Hypotheses
Ref Expression
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
Ref Expression
hoidmvlelem2 (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑘   𝑧,𝐴   𝐵,𝑎,𝑏,𝑘   𝑦,𝐵   𝑧,𝐵   𝐶,𝑎,𝑏,𝑗,𝑘   𝐶,𝑖,𝑗   𝑧,𝐶,𝑗   𝐷,𝑎,𝑏,𝑗,𝑘   𝐷,𝑐,𝑗,𝑘   𝐷,𝑖   𝑦,𝐷,𝑗   𝑧,𝐷   𝑧,𝐸   𝐹,𝑎,𝑏,𝑘   𝑧,𝐺   𝐻,𝑎,𝑏,𝑘   𝑧,𝐻   𝐽,𝑎,𝑏,𝑘   𝐾,𝑎,𝑏,𝑘   𝑧,𝐿   𝑖,𝑀,𝑗   𝑖,𝑂   𝑃,𝑎,𝑏,𝑘,𝑥   𝑄,𝑎,𝑏,𝑗,𝑘,𝑥   𝑄,𝑐,𝑥   𝑢,𝑄   𝑧,𝑄   𝑆,𝑎,𝑏,𝑗,𝑘,𝑥   𝑆,𝑐   𝑆,𝑖,𝑥   𝑢,𝑆   𝑧,𝑆   𝑢,𝑈   𝑥,𝑉,𝑦   𝑊,𝑎,𝑏,𝑗,𝑘,𝑥   𝑊,𝑐   𝑧,𝑊   𝑌,𝑎,𝑏,𝑗,𝑘,𝑥   𝑌,𝑐   𝑦,𝑌   𝑍,𝑐,𝑗,𝑘,𝑥   𝑖,𝑍   𝑦,𝑍   𝑧,𝑍   𝜑,𝑎,𝑏,𝑗,𝑘,𝑥   𝜑,𝑐   𝜑,𝑖   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑧, 𝑢)   𝐴(𝑥, 𝑦, 𝑢, 𝑖, 𝑗, 𝑐)   𝐵(𝑥, 𝑢, 𝑖, 𝑗, 𝑐)   𝐶(𝑥, 𝑦, 𝑢, 𝑐)   𝐷(𝑥, 𝑢)   𝑃(𝑦, 𝑧, 𝑢, 𝑖, 𝑗, 𝑐)   𝑄(𝑦, 𝑖)   𝑆(𝑦)   𝑈(𝑥, 𝑦, 𝑧, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝐸(𝑥, 𝑦, 𝑢, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝐹(𝑥, 𝑦, 𝑧, 𝑢, 𝑖, 𝑗, 𝑐)   𝐺(𝑥, 𝑦, 𝑢, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝐻(𝑥, 𝑦, 𝑢, 𝑖, 𝑗, 𝑐)   𝐽(𝑥, 𝑦, 𝑧, 𝑢, 𝑖, 𝑗, 𝑐)   𝐾(𝑥, 𝑦, 𝑧, 𝑢, 𝑖, 𝑗, 𝑐)   𝐿(𝑥, 𝑦, 𝑢, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝑀(𝑥, 𝑦, 𝑧, 𝑢, 𝑘, 𝑎, 𝑏, 𝑐)   𝑂(𝑥, 𝑦, 𝑧, 𝑢, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝑉(𝑧, 𝑢, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝑊(𝑦, 𝑢, 𝑖)   𝑋(𝑥, 𝑦, 𝑧, 𝑢, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐)   𝑌(𝑧, 𝑢, 𝑖)   𝑍(𝑢, 𝑎, 𝑏)

Proof of Theorem hoidmvlelem2
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 hoidmvlelem2.a . . . . . . 7 (𝜑 → 𝐴:𝑊⟶ℝ)
2 hoidmvlelem2.z . . . . . . . . . 10 (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
3 snidg 4621 . . . . . . . . . 10 (𝑍 ∈ (𝑋 ∖ 𝑌) → 𝑍 ∈ {𝑍})
42, 3syl 18 . . . . . . . . 9 (𝜑 → 𝑍 ∈ {𝑍})
5 elun2 4129 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
64, 5syl 18 . . . . . . . 8 (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍}))
7 hoidmvlelem2.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
86, 7eleqtrrdi 2872 . . . . . . 7 (𝜑 → 𝑍 ∈ 𝑊)
91, 8ffvelcdmd 7085 . . . . . 6 (𝜑 → (𝐴‘𝑍) ∈ ℝ)
10 hoidmvlelem2.b . . . . . . 7 (𝜑 → 𝐵:𝑊⟶ℝ)
1110, 8ffvelcdmd 7085 . . . . . 6 (𝜑 → (𝐵‘𝑍) ∈ ℝ)
12 hoidmvlelem2.v . . . . . . . 8 𝑉 = ({(𝐵‘𝑍)} ∪ 𝑂)
1311snssd 4747 . . . . . . . . 9 (𝜑 → {(𝐵‘𝑍)} ⊆ ℝ)
14 hoidmvlelem2.O . . . . . . . . . 10 𝑂 = ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))
15 nfv 1947 . . . . . . . . . . 11 Ⅎ𝑖𝜑
16 eqid 2761 . . . . . . . . . . 11 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) = (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))
17 simpl 488 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝜑)
18 fz1ssnn 13689 . . . . . . . . . . . . . 14 (1...𝑀) ⊆ ℕ
19 elrabi 3641 . . . . . . . . . . . . . 14 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ (1...𝑀))
2018, 19sselid 3929 . . . . . . . . . . . . 13 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ ℕ)
2120adantl 487 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑖 ∈ ℕ)
22 eleq1w 2844 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ))
2322anbi2d 642 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑖 ∈ ℕ)))
24 fveq2 6885 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
2524fveq1d 6887 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
2625eleq1d 2846 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝐷‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐷‘𝑖)‘𝑍) ∈ ℝ))
2723, 26imbi12d 347 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ)))
28 hoidmvlelem2.d . . . . . . . . . . . . . . . 16 (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊))
2928ffvelcdmda 7084 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑊))
30 elmapi 8869 . . . . . . . . . . . . . . 15 ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ)
3129, 30syl 18 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ)
328adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑊)
3331, 32ffvelcdmd 7085 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
3427, 33chvarvv 2022 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ)
3517, 21, 34syl2anc 596 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ)
3615, 16, 35rnmptssd 7124 . . . . . . . . . 10 (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ⊆ ℝ)
3714, 36eqsstrid 3969 . . . . . . . . 9 (𝜑 → 𝑂 ⊆ ℝ)
3813, 37unssd 4138 . . . . . . . 8 (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ⊆ ℝ)
3912, 38eqsstrid 3969 . . . . . . 7 (𝜑 → 𝑉 ⊆ ℝ)
40 hoidmvlelem2.q . . . . . . . 8 𝑄 = inf(𝑉, ℝ, < )
41 ltso 11390 . . . . . . . . . 10 < Or ℝ
4241a1i 11 . . . . . . . . 9 (𝜑 → < Or ℝ)
43 snfi 9071 . . . . . . . . . . . 12 {(𝐵‘𝑍)} ∈ Fin
4443a1i 11 . . . . . . . . . . 11 (𝜑 → {(𝐵‘𝑍)} ∈ Fin)
45 fzfi 14115 . . . . . . . . . . . . . . 15 (1...𝑀) ∈ Fin
46 rabfi 9262 . . . . . . . . . . . . . . 15 ((1...𝑀) ∈ Fin → {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin)
4745, 46ax-mp 5 . . . . . . . . . . . . . 14 {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin
4847a1i 11 . . . . . . . . . . . . 13 (𝜑 → {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin)
4916rnmptfi 46185 . . . . . . . . . . . . 13 ({𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin)
5048, 49syl 18 . . . . . . . . . . . 12 (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin)
5114, 50eqeltrid 2865 . . . . . . . . . . 11 (𝜑 → 𝑂 ∈ Fin)
52 unfi 9186 . . . . . . . . . . 11 (({(𝐵‘𝑍)} ∈ Fin ∧ 𝑂 ∈ Fin) → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin)
5344, 51, 52syl2anc 596 . . . . . . . . . 10 (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin)
5412, 53eqeltrid 2865 . . . . . . . . 9 (𝜑 → 𝑉 ∈ Fin)
55 fvex 6898 . . . . . . . . . . . . . 14 (𝐵‘𝑍) ∈ V
5655snid 4623 . . . . . . . . . . . . 13 (𝐵‘𝑍) ∈ {(𝐵‘𝑍)}
57 elun1 4128 . . . . . . . . . . . . 13 ((𝐵‘𝑍) ∈ {(𝐵‘𝑍)} → (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂))
5856, 57ax-mp 5 . . . . . . . . . . . 12 (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)
5912eqcomi 2770 . . . . . . . . . . . 12 ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉
6058, 59eleqtri 2859 . . . . . . . . . . 11 (𝐵‘𝑍) ∈ 𝑉
6160a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵‘𝑍) ∈ 𝑉)
62 ne0i 4287 . . . . . . . . . 10 ((𝐵‘𝑍) ∈ 𝑉 → 𝑉 ≠ ∅)
6361, 62syl 18 . . . . . . . . 9 (𝜑 → 𝑉 ≠ ∅)
64 fiinfcl 9495 . . . . . . . . 9 (( < Or ℝ ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ∧ 𝑉 ⊆ ℝ)) → inf(𝑉, ℝ, < ) ∈ 𝑉)
6542, 54, 63, 39, 64syl13anc 1399 . . . . . . . 8 (𝜑 → inf(𝑉, ℝ, < ) ∈ 𝑉)
6640, 65eqeltrid 2865 . . . . . . 7 (𝜑 → 𝑄 ∈ 𝑉)
6739, 66sseldd 3932 . . . . . 6 (𝜑 → 𝑄 ∈ ℝ)
68 hoidmvlelem2.u . . . . . . . . . . . 12 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}
69 ssrab2 4028 . . . . . . . . . . . 12 {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍))
7068, 69eqsstri 3977 . . . . . . . . . . 11 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍))
7170a1i 11 . . . . . . . . . 10 (𝜑 → 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)))
729, 11iccssred 13565 . . . . . . . . . 10 (𝜑 → ((𝐴‘𝑍)[,](𝐵‘𝑍)) ⊆ ℝ)
7371, 72sstrd 3941 . . . . . . . . 9 (𝜑 → 𝑈 ⊆ ℝ)
74 hoidmvlelem2.su . . . . . . . . 9 (𝜑 → 𝑆 ∈ 𝑈)
7573, 74sseldd 3932 . . . . . . . 8 (𝜑 → 𝑆 ∈ ℝ)
769rexrd 11359 . . . . . . . . 9 (𝜑 → (𝐴‘𝑍) ∈ ℝ*)
7711rexrd 11359 . . . . . . . . 9 (𝜑 → (𝐵‘𝑍) ∈ ℝ*)
7870, 74sselid 3929 . . . . . . . . 9 (𝜑 → 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)))
79 iccgelb 13533 . . . . . . . . 9 (((𝐴‘𝑍) ∈ ℝ* ∧ (𝐵‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) → (𝐴‘𝑍) ≤ 𝑆)
8076, 77, 78, 79syl3anc 1398 . . . . . . . 8 (𝜑 → (𝐴‘𝑍) ≤ 𝑆)
81 hoidmvlelem2.sb . . . . . . . . . . . . . . 15 (𝜑 → 𝑆 < (𝐵‘𝑍))
8281adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < (𝐵‘𝑍))
83 id 23 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐵‘𝑍) → 𝑥 = (𝐵‘𝑍))
8483eqcomd 2767 . . . . . . . . . . . . . . 15 (𝑥 = (𝐵‘𝑍) → (𝐵‘𝑍) = 𝑥)
8584adantl 487 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → (𝐵‘𝑍) = 𝑥)
8682, 85breqtrd 5131 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥)
8786adantlr 728 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥)
88 simpll 779 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝜑)
89 id 23 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉)
9089, 12eleqtrdi 2871 . . . . . . . . . . . . . . . 16 (𝑥 ∈ 𝑉 → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂))
9190adantr 486 . . . . . . . . . . . . . . 15 ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂))
92 elsni 4601 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {(𝐵‘𝑍)} → 𝑥 = (𝐵‘𝑍))
9392con3i 155 . . . . . . . . . . . . . . . 16 (¬ 𝑥 = (𝐵‘𝑍) → ¬ 𝑥 ∈ {(𝐵‘𝑍)})
9493adantl 487 . . . . . . . . . . . . . . 15 ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → ¬ 𝑥 ∈ {(𝐵‘𝑍)})
95 elunnel1 4101 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂) ∧ ¬ 𝑥 ∈ {(𝐵‘𝑍)}) → 𝑥 ∈ 𝑂)
9691, 94, 95syl2anc 596 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂)
9796adantll 727 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂)
98 id 23 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ 𝑂 → 𝑥 ∈ 𝑂)
9998, 14eleqtrdi 2871 . . . . . . . . . . . . . . . 16 (𝑥 ∈ 𝑂 → 𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)))
100 vex 3455 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
10116elrnmpt 5940 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)))
102100, 101ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍))
10399, 102sylib 221 . . . . . . . . . . . . . . 15 (𝑥 ∈ 𝑂 → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍))
104103adantl 487 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ 𝑂) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍))
105 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
106105fveq1d 6887 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
107106eleq1d 2846 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐶‘𝑖)‘𝑍) ∈ ℝ))
10823, 107imbi12d 347 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ)))
109 hoidmvlelem2.c . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊))
110109ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑊))
111 elmapi 8869 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ)
112110, 111syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ)
113112, 32ffvelcdmd 7085 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
114108, 113chvarvv 2022 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ)
115114rexrd 11359 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ*)
11617, 21, 115syl2anc 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ*)
11734rexrd 11359 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ*)
11817, 21, 117syl2anc 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ*)
119106, 25oveq12d 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
120119eleq2d 2847 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑖 → (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
121120elrab 3645 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
122121biimpi 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
123122simprd 501 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
124123adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
125 icoltub 46519 . . . . . . . . . . . . . . . . . . . 20 ((((𝐶‘𝑖)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑖)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) → 𝑆 < ((𝐷‘𝑖)‘𝑍))
126116, 118, 124, 125syl3anc 1398 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 < ((𝐷‘𝑖)‘𝑍))
1271263adant3 1150 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < ((𝐷‘𝑖)‘𝑍))
128 id 23 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑥 = ((𝐷‘𝑖)‘𝑍))
129128eqcomd 2767 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝐷‘𝑖)‘𝑍) → ((𝐷‘𝑖)‘𝑍) = 𝑥)
1301293ad2ant3 1153 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → ((𝐷‘𝑖)‘𝑍) = 𝑥)
131127, 130breqtrd 5131 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < 𝑥)
1321313exp 1137 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥)))
133132adantr 486 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥)))
134133rexlimdv 3162 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ 𝑂) → (∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥))
135104, 134mpd 16 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝑆 < 𝑥)
13688, 97, 135syl2anc 596 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥)
13787, 136pm2.61dan 825 . . . . . . . . . . 11 ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑆 < 𝑥)
138137ralrimiva 3155 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ 𝑉 𝑆 < 𝑥)
139 breq2 5107 . . . . . . . . . . 11 (𝑥 = inf(𝑉, ℝ, < ) → (𝑆 < 𝑥 ↔ 𝑆 < inf(𝑉, ℝ, < )))
140139rspcva 3575 . . . . . . . . . 10 ((inf(𝑉, ℝ, < ) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑉 𝑆 < 𝑥) → 𝑆 < inf(𝑉, ℝ, < ))
14165, 138, 140syl2anc 596 . . . . . . . . 9 (𝜑 → 𝑆 < inf(𝑉, ℝ, < ))
14240eqcomi 2770 . . . . . . . . . 10 inf(𝑉, ℝ, < ) = 𝑄
143142a1i 11 . . . . . . . . 9 (𝜑 → inf(𝑉, ℝ, < ) = 𝑄)
144141, 143breqtrd 5131 . . . . . . . 8 (𝜑 → 𝑆 < 𝑄)
1459, 75, 67, 80, 144lelttrd 11468 . . . . . . 7 (𝜑 → (𝐴‘𝑍) < 𝑄)
1469, 67, 145ltled 11458 . . . . . 6 (𝜑 → (𝐴‘𝑍) ≤ 𝑄)
147 fiminre 12264 . . . . . . . . 9 ((𝑉 ⊆ ℝ ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦)
14839, 54, 63, 147syl3anc 1398 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦)
149 lbinfle 12272 . . . . . . . 8 ((𝑉 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ (𝐵‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍))
15039, 148, 61, 149syl3anc 1398 . . . . . . 7 (𝜑 → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍))
15140, 150eqbrtrid 5140 . . . . . 6 (𝜑 → 𝑄 ≤ (𝐵‘𝑍))
1529, 11, 67, 146, 151eliccd 46515 . . . . 5 (𝜑 → 𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)))
15367recnd 11337 . . . . . . . . . 10 (𝜑 → 𝑄 ∈ ℂ)
15475recnd 11337 . . . . . . . . . 10 (𝜑 → 𝑆 ∈ ℂ)
1559recnd 11337 . . . . . . . . . 10 (𝜑 → (𝐴‘𝑍) ∈ ℂ)
156153, 154, 155npncand 11693 . . . . . . . . 9 (𝜑 → ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))) = (𝑄 − (𝐴‘𝑍)))
157156eqcomd 2767 . . . . . . . 8 (𝜑 → (𝑄 − (𝐴‘𝑍)) = ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))))
158157oveq2d 7436 . . . . . . 7 (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))))
159 rge0ssre 13587 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
160 hoidmvlelem2.g . . . . . . . . . . 11 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌))
161 hoidmvlelem2.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
162 hoidmvlelem2.x . . . . . . . . . . . . 13 (𝜑 → 𝑋 ∈ Fin)
163 hoidmvlelem2.y . . . . . . . . . . . . 13 (𝜑 → 𝑌 ⊆ 𝑋)
164162, 163ssfid 9260 . . . . . . . . . . . 12 (𝜑 → 𝑌 ∈ Fin)
165 ssun1 4124 . . . . . . . . . . . . . . 15 𝑌 ⊆ (𝑌 ∪ {𝑍})
166165, 7sseqtrri 3980 . . . . . . . . . . . . . 14 𝑌 ⊆ 𝑊
167166a1i 11 . . . . . . . . . . . . 13 (𝜑 → 𝑌 ⊆ 𝑊)
1681, 167fssresd 6749 . . . . . . . . . . . 12 (𝜑 → (𝐴 ↾ 𝑌):𝑌⟶ℝ)
16910, 167fssresd 6749 . . . . . . . . . . . 12 (𝜑 → (𝐵 ↾ 𝑌):𝑌⟶ℝ)
170161, 164, 168, 169hoidmvcl 47591 . . . . . . . . . . 11 (𝜑 → ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) ∈ (0[,)+∞))
171160, 170eqeltrid 2865 . . . . . . . . . 10 (𝜑 → 𝐺 ∈ (0[,)+∞))
172159, 171sselid 3929 . . . . . . . . 9 (𝜑 → 𝐺 ∈ ℝ)
173172recnd 11337 . . . . . . . 8 (𝜑 → 𝐺 ∈ ℂ)
174153, 154subcld 11669 . . . . . . . 8 (𝜑 → (𝑄 − 𝑆) ∈ ℂ)
175154, 155subcld 11669 . . . . . . . 8 (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℂ)
176173, 174, 175adddid 11333 . . . . . . 7 (𝜑 → (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))))
177173, 174mulcld 11329 . . . . . . . 8 (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℂ)
178173, 175mulcld 11329 . . . . . . . 8 (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℂ)
179177, 178addcomd 11512 . . . . . . 7 (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))))
180158, 176, 1793eqtrd 2800 . . . . . 6 (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))))
18167, 75jca 521 . . . . . . . . . . . . 13 (𝜑 → (𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ))
182 resubcl 11622 . . . . . . . . . . . . 13 ((𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑄 − 𝑆) ∈ ℝ)
183181, 182syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑄 − 𝑆) ∈ ℝ)
184172, 183jca 521 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ))
185 remulcl 11285 . . . . . . . . . . 11 ((𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ) → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ)
186184, 185syl 18 . . . . . . . . . 10 (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ)
18775, 9jca 521 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ))
188 resubcl 11622 . . . . . . . . . . . . 13 ((𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ) → (𝑆 − (𝐴‘𝑍)) ∈ ℝ)
189187, 188syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℝ)
190172, 189jca 521 . . . . . . . . . . 11 (𝜑 → (𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ))
191 remulcl 11285 . . . . . . . . . . 11 ((𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ) → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ)
192190, 191syl 18 . . . . . . . . . 10 (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ)
193186, 192jca 521 . . . . . . . . 9 (𝜑 → ((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ))
194 readdcl 11283 . . . . . . . . 9 (((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ)
195193, 194syl 18 . . . . . . . 8 (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ)
196179, 195eqeltrrd 2862 . . . . . . 7 (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ∈ ℝ)
197 1red 11309 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
198 hoidmvlelem2.e . . . . . . . . . . 11 (𝜑 → 𝐸 ∈ ℝ+)
199198rpred 13164 . . . . . . . . . 10 (𝜑 → 𝐸 ∈ ℝ)
200197, 199readdcld 11338 . . . . . . . . 9 (𝜑 → (1 + 𝐸) ∈ ℝ)
2012eldifbd 3912 . . . . . . . . . . 11 (𝜑 → ¬ 𝑍 ∈ 𝑌)
2028, 201eldifd 3910 . . . . . . . . . 10 (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌))
203 hoidmvlelem2.r . . . . . . . . . 10 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
204 hoidmvlelem2.h . . . . . . . . . 10 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))))
205161, 164, 202, 7, 109, 28, 203, 204, 75sge0hsphoire 47598 . . . . . . . . 9 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ)
206200, 205remulcld 11339 . . . . . . . 8 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ)
207 fzfid 14116 . . . . . . . . . 10 (𝜑 → (1...𝑀) ∈ Fin)
208183adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℝ)
209 simpl 488 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝜑)
210 elfznn 13687 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
211210adantl 487 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
212 id 23 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
213 ovexd 7455 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V)
214 hoidmvlelem2.p . . . . . . . . . . . . . . . . 17 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
215214fvmpt2 7005 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ ∧ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
216212, 213, 215syl2anc 596 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
217216adantl 487 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
218164adantr 486 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ Fin)
219166a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ⊆ 𝑊)
220112, 219fssresd 6749 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ)
221220adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ)
222 iftrue 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌))
223222adantl 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌))
224223feq1d 6691 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ))
225221, 224mpbird 260 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
226 0red 11311 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ 𝑌) → 0 ∈ ℝ)
227 hoidmvlelem2.f . . . . . . . . . . . . . . . . . . . 20 𝐹 = (𝑦 ∈ 𝑌 ↦ 0)
228226, 227fmptd 7114 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐹:𝑌⟶ℝ)
229228ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝐹:𝑌⟶ℝ)
230 iffalse 4491 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹)
231230adantl 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹)
232231feq1d 6691 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ))
233229, 232mpbird 260 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
234225, 233pm2.61dan 825 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
235 simpr 490 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
236 fvex 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘𝑗) ∈ V
237236resex 6018 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶‘𝑗) ↾ 𝑌) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐶‘𝑗) ↾ 𝑌) ∈ V)
239162, 163ssexd 5286 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑌 ∈ V)
240 mptexg 7227 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ 0) ∈ V)
241239, 240syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑦 ∈ 𝑌 ↦ 0) ∈ V)
242227, 241eqeltrid 2865 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝐹 ∈ V)
243238, 242ifcld 4529 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V)
244243adantr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V)
245 hoidmvlelem2.j . . . . . . . . . . . . . . . . . . 19 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹))
246245fvmpt2 7005 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹))
247235, 244, 246syl2anc 596 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹))
248247feq1d 6691 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ))
249234, 248mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗):𝑌⟶ℝ)
25031, 219fssresd 6749 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ)
251250adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ)
252 iftrue 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌))
253252adantl 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌))
254253feq1d 6691 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ))
255251, 254mpbird 260 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
256 iffalse 4491 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹)
257256adantl 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹)
258257feq1d 6691 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ))
259229, 258mpbird 260 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
260255, 259pm2.61dan 825 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)
261 fvex 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷‘𝑗) ∈ V
262261resex 6018 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷‘𝑗) ↾ 𝑌) ∈ V
263262a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷‘𝑗) ↾ 𝑌) ∈ V)
264263, 242ifcld 4529 . . . . . . . . . . . . . . . . . . 19 (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V)
265264adantr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V)
266 hoidmvlelem2.k . . . . . . . . . . . . . . . . . . 19 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹))
267266fvmpt2 7005 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹))
268235, 265, 267syl2anc 596 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹))
269268feq1d 6691 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐾‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ))
270260, 269mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗):𝑌⟶ℝ)
271161, 218, 249, 270hoidmvcl 47591 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ (0[,)+∞))
272217, 271eqeltrd 2861 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ (0[,)+∞))
273159, 272sselid 3929 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℝ)
274209, 211, 273syl2anc 596 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℝ)
275208, 274remulcld 11339 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ)
276207, 275fsumrecl 15900 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ)
277200, 276remulcld 11339 . . . . . . . 8 (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ)
278206, 277readdcld 11338 . . . . . . 7 (𝜑 → (((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ)
279161, 164, 202, 7, 109, 28, 203, 204, 67sge0hsphoire 47598 . . . . . . . 8 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ)
280200, 279remulcld 11339 . . . . . . 7 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) ∈ ℝ)
28174, 68eleqtrdi 2871 . . . . . . . . . 10 (𝜑 → 𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))})
282 oveq1 7427 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑧 − (𝐴‘𝑍)) = (𝑆 − (𝐴‘𝑍)))
283282oveq2d 7436 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑆 − (𝐴‘𝑍))))
284 fveq2 6885 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑆 → (𝐻‘𝑧) = (𝐻‘𝑆))
285284fveq1d 6887 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑆 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑆)‘(𝐷‘𝑗)))
286285oveq2d 7436 . . . . . . . . . . . . . . 15 (𝑧 = 𝑆 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))
287286mpteq2dv 5199 . . . . . . . . . . . . . 14 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))
288287fveq2d 6889 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))
289288oveq2d 7436 . . . . . . . . . . . 12 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
290283, 289breq12d 5116 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))))
291290elrab 3645 . . . . . . . . . 10 (𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))))
292281, 291sylib 221 . . . . . . . . 9 (𝜑 → (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))))
293292simprd 501 . . . . . . . 8 (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
294207, 274fsumrecl 15900 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℝ)
295200, 294remulcld 11339 . . . . . . . . . 10 (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) ∈ ℝ)
296 0red 11311 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
29775, 67posdifd 11903 . . . . . . . . . . . 12 (𝜑 → (𝑆 < 𝑄 ↔ 0 < (𝑄 − 𝑆)))
298144, 297mpbid 235 . . . . . . . . . . 11 (𝜑 → 0 < (𝑄 − 𝑆))
299296, 183, 298ltled 11458 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝑄 − 𝑆))
300 hoidmvlelem2.le . . . . . . . . . 10 (𝜑 → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)))
301172, 295, 183, 299, 300lemul1ad 12256 . . . . . . . . 9 (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)))
302200recnd 11337 . . . . . . . . . . 11 (𝜑 → (1 + 𝐸) ∈ ℂ)
303294recnd 11337 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℂ)
304302, 303, 174mulassd 11332 . . . . . . . . . 10 (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆))))
305274recnd 11337 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℂ)
306207, 174, 305fsummulc1 15951 . . . . . . . . . . . 12 (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆)))
307174adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℂ)
308305, 307mulcomd 11330 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − 𝑆)) = ((𝑄 − 𝑆) · (𝑃‘𝑗)))
309308sumeq2dv 15869 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))
310306, 309eqtrd 2796 . . . . . . . . . . 11 (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))
311310oveq2d 7436 . . . . . . . . . 10 (𝜑 → ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆))) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))
312304, 311eqtrd 2796 . . . . . . . . 9 (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))
313301, 312breqtrd 5131 . . . . . . . 8 (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))
314192, 186, 206, 277, 293, 313le2addd 11935 . . . . . . 7 (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ (((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))))
315 hoidmvlelem2.m . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑀 ∈ ℕ)
316 nnsplit 46369 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → ℕ = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
317315, 316syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
318 uncom 4105 . . . . . . . . . . . . . . . . 17 ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) = ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀))
319318a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) = ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)))
320317, 319eqtr2d 2797 . . . . . . . . . . . . . . 15 (𝜑 → ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) = ℕ)
321320eqcomd 2767 . . . . . . . . . . . . . 14 (𝜑 → ℕ = ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)))
322321mpteq1d 5195 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))
323322fveq2d 6889 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = (Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))
324 nfv 1947 . . . . . . . . . . . . 13 Ⅎ𝑗𝜑
325 fvexd 6900 . . . . . . . . . . . . 13 (𝜑 → (ℤ≥‘(𝑀 + 1)) ∈ V)
326 ovexd 7455 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ∈ V)
327 incom 4155 . . . . . . . . . . . . . . 15 ((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ((1...𝑀) ∩ (ℤ≥‘(𝑀 + 1)))
328 nnuzdisj 46366 . . . . . . . . . . . . . . 15 ((1...𝑀) ∩ (ℤ≥‘(𝑀 + 1))) = ∅
329327, 328eqtri 2784 . . . . . . . . . . . . . 14 ((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅
330329a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅)
331 icossicc 13567 . . . . . . . . . . . . . 14 (0[,)+∞) ⊆ (0[,]+∞)
332 ssid 3953 . . . . . . . . . . . . . . 15 (0[,)+∞) ⊆ (0[,)+∞)
333 simpl 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑)
334315peano2nnd 12352 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + 1) ∈ ℕ)
335 uznnssnn 13022 . . . . . . . . . . . . . . . . . . 19 ((𝑀 + 1) ∈ ℕ → (ℤ≥‘(𝑀 + 1)) ⊆ ℕ)
336334, 335syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℤ≥‘(𝑀 + 1)) ⊆ ℕ)
337336adantr 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → (ℤ≥‘(𝑀 + 1)) ⊆ ℕ)
338 simpr 490 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1)))
339337, 338sseldd 3932 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
340 snfi 9071 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
341340a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
342 unfi 9186 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
343164, 341, 342syl2anc 596 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
3447, 343eqeltrid 2865 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑊 ∈ Fin)
345344adantr 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
346 eleq1w 2844 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝑗 ∈ 𝑌 ↔ 𝑙 ∈ 𝑌))
347 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝑐‘𝑗) = (𝑐‘𝑙))
348347breq1d 5113 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑙 → ((𝑐‘𝑗) ≤ 𝑥 ↔ (𝑐‘𝑙) ≤ 𝑥))
349348, 347ifbieq1d 4507 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥) = if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))
350346, 347, 349ifbieq12d 4511 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) = if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))
351350cbvmptv 5209 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) = (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))
352351mpteq2i 5201 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))))
353352mpteq2i 5201 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))))
354204, 353eqtri 2784 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))))
35575adantr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
356354, 355, 345, 31hsphoif 47585 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑆)‘(𝐷‘𝑗)):𝑊⟶ℝ)
357161, 345, 112, 356hoidmvcl 47591 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
358333, 339, 357syl2anc 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
359332, 358sselid 3929 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
360331, 359sselid 3929 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
361209, 211, 357syl2anc 596 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
362331, 361sselid 3929 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
363324, 325, 326, 330, 360, 362sge0splitmpt 47420 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
364 nnex 12341 . . . . . . . . . . . . . . 15 ℕ ∈ V
365364a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
366331, 357sselid 3929 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
367324, 365, 366, 205, 336sge0ssrempt 47414 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ)
36818a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1...𝑀) ⊆ ℕ)
369324, 365, 366, 205, 368sge0ssrempt 47414 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ)
370 rexadd 13362 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ ∧ (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
371367, 369, 370syl2anc 596 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
372323, 363, 3713eqtrd 2800 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))
373372oveq2d 7436 . . . . . . . . . 10 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))))
374373oveq1d 7435 . . . . . . . . 9 (𝜑 → (((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))))
375372, 205eqeltrrd 2862 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ)
376375recnd 11337 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℂ)
377276recnd 11337 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ)
378302, 376, 377adddid 11333 . . . . . . . . . 10 (𝜑 → ((1 + 𝐸) · (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))))
379378eqcomd 2767 . . . . . . . . 9 (𝜑 → (((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) · (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))))
380367recnd 11337 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ)
381369recnd 11337 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ)
382380, 381, 377addassd 11331 . . . . . . . . . . 11 (𝜑 → (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + ((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))))
383207, 361sge0fsummpt 47399 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))
384383oveq1d 7435 . . . . . . . . . . . . 13 (𝜑 → ((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))
385 ax-resscn 11257 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
386159, 385sstri 3940 . . . . . . . . . . . . . . . . 17 (0[,)+∞) ⊆ ℂ
387386, 357sselid 3929 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ)
388209, 211, 387syl2anc 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ)
389183adantr 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℝ)
390389, 273remulcld 11339 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ)
391390recnd 11337 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ)
392211, 391syldan 603 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ)
393207, 388, 392fsumadd 15906 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))
394393eqcomd 2767 . . . . . . . . . . . . 13 (𝜑 → (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))
395384, 394eqtrd 2796 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))
396395oveq2d 7436 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + ((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))
397382, 396eqtrd 2796 . . . . . . . . . 10 (𝜑 → (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))
398397oveq2d 7436 . . . . . . . . 9 (𝜑 → ((1 + 𝐸) · (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))))
399374, 379, 3983eqtrd 2800 . . . . . . . 8 (𝜑 → (((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))))
400159, 357sselid 3929 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℝ)
401400, 390readdcld 11338 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ)
402209, 211, 401syl2anc 596 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ)
403207, 402fsumrecl 15900 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ)
404367, 403readdcld 11338 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ)
405 0le1 11839 . . . . . . . . . . 11 0 ≤ 1
406405a1i 11 . . . . . . . . . 10 (𝜑 → 0 ≤ 1)
407198rpge0d 13168 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐸)
408197, 199, 406, 407addge0d 11892 . . . . . . . . 9 (𝜑 → 0 ≤ (1 + 𝐸))
40967adantr 486 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℝ)
410354, 409, 345, 31hsphoif 47585 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑄)‘(𝐷‘𝑗)):𝑊⟶ℝ)
411161, 345, 112, 410hoidmvcl 47591 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
412331, 411sselid 3929 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
413324, 365, 412, 279, 336sge0ssrempt 47414 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ)
414159, 411sselid 3929 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ)
415209, 211, 414syl2anc 596 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ)
416207, 415fsumrecl 15900 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ)
417333, 339, 412syl2anc 596 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
418202adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌))
41975, 67, 144ltled 11458 . . . . . . . . . . . . . . 15 (𝜑 → 𝑆 ≤ 𝑄)
420419adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ≤ 𝑄)
421161, 345, 418, 7, 355, 409, 420, 354, 112, 31hsphoidmvle2 47594 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
422333, 339, 421syl2anc 596 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
423324, 325, 360, 417, 422sge0lempt 47419 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≤ (Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))
424209adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝜑)
425211adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝑗 ∈ ℕ)
426 simpr 490 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) = 0)
427 oveq2 7428 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘𝑗) = 0 → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0))
428427adantl 487 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0))
429174mul01d 11509 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑄 − 𝑆) · 0) = 0)
430429ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · 0) = 0)
431428, 430eqtrd 2796 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = 0)
432431oveq2d 7436 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0))
433387addridd 11510 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))
434433adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))
435432, 434eqtrd 2796 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))
436421adantr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
437435, 436eqbrtrd 5127 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
438424, 425, 426, 437syl21anc 851 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
439 simpl 488 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝜑 ∧ 𝑗 ∈ (1...𝑀)))
440 neqne 2964 . . . . . . . . . . . . . . 15 (¬ (𝑃‘𝑗) = 0 → (𝑃‘𝑗) ≠ 0)
441440adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) ≠ 0)
442402adantr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ)
443209adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝜑)
444211adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ ℕ)
445 simpr 490 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) ≠ 0)
4462adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑋 ∖ 𝑌))
447201adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → ¬ 𝑍 ∈ 𝑌)
448 eqid 2761 . . . . . . . . . . . . . . . . . . . . . 22 ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)))
449161, 218, 446, 447, 7, 112, 356, 448hoiprodp1 47597 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)))))
450449adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)))))
451217adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
452218adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ∈ Fin)
453217adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
454 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑌 = ∅ → (𝐿‘𝑌) = (𝐿‘∅))
455454oveqd 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑌 = ∅ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗)))
456455adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗)))
457249adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):𝑌⟶ℝ)
458 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑌 = ∅ → 𝑌 = ∅)
459458eqcomd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑌 = ∅ → ∅ = 𝑌)
460459adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ∅ = 𝑌)
461460feq2d 6693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗):∅⟶ℝ ↔ (𝐽‘𝑗):𝑌⟶ℝ))
462457, 461mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):∅⟶ℝ)
463270adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):𝑌⟶ℝ)
464460feq2d 6693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐾‘𝑗):∅⟶ℝ ↔ (𝐾‘𝑗):𝑌⟶ℝ))
465463, 464mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):∅⟶ℝ)
466161, 462, 465hoidmv0val 47592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗)) = 0)
467453, 456, 4663eqtrd 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0)
468467adantlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0)
469 neneq 2962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃‘𝑗) ≠ 0 → ¬ (𝑃‘𝑗) = 0)
470469ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → ¬ (𝑃‘𝑗) = 0)
471468, 470pm2.65da 829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ 𝑌 = ∅)
472471neqned 2963 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ≠ ∅)
473249adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗):𝑌⟶ℝ)
474270adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗):𝑌⟶ℝ)
475161, 452, 472, 473, 474hoidmvn0val 47593 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))))
476247adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹))
477217adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
478247adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹))
479478, 231eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = 𝐹)
480268adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹))
481480, 257eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = 𝐹)
482479, 481oveq12d 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = (𝐹(𝐿‘𝑌)𝐹))
483161, 164, 228hoidmvval0b 47599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐹(𝐿‘𝑌)𝐹) = 0)
484483ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐹(𝐿‘𝑌)𝐹) = 0)
485477, 482, 4843eqtrd 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0)
486485adantlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0)
487469ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ¬ (𝑃‘𝑗) = 0)
488486, 487condan 830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
489488iftrued 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌))
490476, 489eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = ((𝐶‘𝑗) ↾ 𝑌))
491490fveq1d 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘))
492491adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘))
493 fvres 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ 𝑌 → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘))
494493adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘))
495492, 494eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑘))
496268adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹))
497488, 252syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌))
498496, 497eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = ((𝐷‘𝑗) ↾ 𝑌))
499498fveq1d 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘))
500499adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘))
501 fvres 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ 𝑌 → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘))
502501adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘))
503500, 502eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑘))
504495, 503oveq12d 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
505504fveq2d 6889 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
506505prodeq2dv 16090 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
507475, 506eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
508355adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑆 ∈ ℝ)
509345adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑊 ∈ Fin)
51031adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (𝐷‘𝑗):𝑊⟶ℝ)
511 elun1 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ 𝑌 → 𝑘 ∈ (𝑌 ∪ {𝑍}))
512511, 7eleqtrrdi 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑊)
513512adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑊)
514354, 508, 509, 510, 513hsphoival 47588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)))
515 iftrue 4488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘))
516515adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘))
517514, 516eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘))
518517oveq2d 7436 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
519518fveq2d 6889 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
520519prodeq2dv 16090 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
521520eqcomd 2767 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))))
522521adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))))
523451, 507, 5223eqtrrd 2801 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗))
524354, 355, 345, 31, 32hsphoival 47588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)))
525201iffalsed 4493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))
526525adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))
527524, 526eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))
528527oveq2d 7436 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)))
529528adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)))
530113rexrd 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ*)
531530adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ*)
53233rexrd 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ*)
533532adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ*)
534 icoltub 46519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑆 < ((𝐷‘𝑗)‘𝑍))
535531, 533, 488, 534syl3anc 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < ((𝐷‘𝑗)‘𝑍))
536355adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ)
53733adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
538536, 537ltnled 11457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑆 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆))
539535, 538mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆)
540539iffalsed 4493 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆) = 𝑆)
541540oveq2d 7436 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆))
542529, 541eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆))
543542fveq2d 6889 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)))
544 volico 46992 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0))
545113, 536, 544syl2an 608 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0)) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0))
546545anabss5 681 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0))
547 iftrue 4488 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
548547adantl 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
549 iffalse 4491 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ ((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0)
550549adantl 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0)
551 simpll 779 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (𝜑 ∧ 𝑗 ∈ ℕ))
552 icogelb 13527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆)
553531, 533, 488, 552syl3anc 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆)
554553adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆)
555 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆)
556554, 555jca 521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆))
557551, 113syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
558551, 355syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 𝑆 ∈ ℝ)
559557, 558eqleltd 11454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) = 𝑆 ↔ (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆)))
560556, 559mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) = 𝑆)
561 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐶‘𝑗)‘𝑍) = 𝑆 → ((𝐶‘𝑗)‘𝑍) = 𝑆)
562561eqcomd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶‘𝑗)‘𝑍) = 𝑆 → 𝑆 = ((𝐶‘𝑗)‘𝑍))
563562oveq1d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐶‘𝑗)‘𝑍) = 𝑆 → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)))
564563adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)))
565385, 113sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ)
566565subidd 11657 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0)
567566adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0)
568564, 567eqtr2d 2797 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
569551, 560, 568syl2anc 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
570550, 569eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
571548, 570pm2.61dan 825 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
572543, 546, 5713eqtrd 2800 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (𝑆 − ((𝐶‘𝑗)‘𝑍)))
573523, 572oveq12d 7438 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))))
574386, 272sselid 3929 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℂ)
575355, 113resubcld 11744 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℝ)
576575recnd 11337 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ)
577574, 576mulcomd 11330 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
578577adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
579450, 573, 5783eqtrd 2800 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
580579oveq1d 7435 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))
581174adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℂ)
582576, 581, 574adddird 11334 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))
583582eqcomd 2767 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)))
584583adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)))
585576, 581addcomd 11512 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍))))
586153adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℂ)
587154adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℂ)
588586, 587, 565npncand 11693 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍)))
589585, 588eqtrd 2796 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = (𝑄 − ((𝐶‘𝑗)‘𝑍)))
590589oveq1d 7435 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
591590adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
592580, 584, 5913eqtrd 2800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
593443, 444, 445, 592syl21anc 851 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
594 eqid 2761 . . . . . . . . . . . . . . . . . . . 20 ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘)))
595161, 218, 32, 447, 7, 112, 410, 594hoiprodp1 47597 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))))
596209, 211, 595syl2anc 596 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))))
597596adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))))
598507eqcomd 2767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)))
599409adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑄 ∈ ℝ)
600354, 599, 509, 510, 513hsphoival 47588 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)))
601 iftrue 4488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘))
602601adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘))
603600, 602eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘))
604603oveq2d 7436 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
605604fveq2d 6889 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
606605prodeq2dv 16090 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
607606adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
608598, 607, 4513eqtr4d 2806 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗))
609443, 444, 445, 608syl21anc 851 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗))
610354, 409, 345, 31, 32hsphoival 47588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)))
611211, 610syldan 603 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)))
612611adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)))
613201iffalsed 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))
614613ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))
615211, 33syldan 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
616615adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
617 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) = 𝑄)
618616, 617eqled 11413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≤ 𝑄)
619618iftrued 4490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = ((𝐷‘𝑗)‘𝑍))
620619, 617eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄)
621620adantlr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄)
62267adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℝ)
623622adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ)
624623adantlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ)
625615adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
626625adantlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
62740a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 = inf(𝑉, ℝ, < ))
628443, 39syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑉 ⊆ ℝ)
629148ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦)
630 simplr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ (1...𝑀))
631210, 488sylanl2 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
632630, 631jca 521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
633 rabid 3433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
634632, 633sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))})
635 eqidd 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍))
636 fveq2 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗))
637636fveq1d 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 = 𝑗 → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘𝑗)‘𝑍))
638637eqeq2d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 = 𝑗 → (((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍) ↔ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)))
639638rspcev 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
640634, 635, 639syl2anc 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
641 fvexd 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ V)
64216, 640, 641elrnmptd 5945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)))
643642, 14eleqtrrdi 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑂)
644 elun2 4129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐷‘𝑗)‘𝑍) ∈ 𝑂 → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂))
645643, 644syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂))
64659a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉)
647645, 646eleqtrd 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑉)
648 lbinfle 12272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑉 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ ((𝐷‘𝑗)‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍))
649628, 629, 647, 648syl3anc 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍))
650627, 649eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍))
651650adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍))
652 neqne 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ ((𝐷‘𝑗)‘𝑍) = 𝑄 → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄)
653652adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄)
654624, 626, 651, 653leneltd 11464 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 < ((𝐷‘𝑗)‘𝑍))
655624, 626ltnled 11457 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → (𝑄 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄))
656654, 655mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄)
657656iffalsed 4493 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄)
658621, 657pm2.61dan 825 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄)
659612, 614, 6583eqtrd 2800 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = 𝑄)
660659oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑄))
661660fveq2d 6889 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)))
662209, 211, 113syl2anc 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
663662adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
664443, 67syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ∈ ℝ)
665 volico 46992 . . . . . . . . . . . . . . . . . . . 20 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0))
666663, 664, 665syl2anc 596 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0))
667443, 75syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ)
668443, 444, 445, 553syl21anc 851 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆)
669443, 144syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < 𝑄)
670663, 667, 664, 668, 669lelttrd 11468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) < 𝑄)
671670iftrued 4490 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑄 − ((𝐶‘𝑗)‘𝑍)))
672661, 666, 6713eqtrd 2800 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍)))
673609, 672oveq12d 7438 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))))
674209, 153syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℂ)
675385, 662sselid 3929 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ)
676674, 675subcld 11669 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ)
677305, 676mulcomd 11330 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
678677adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
679597, 673, 6783eqtrd 2800 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)))
680593, 679eqtr4d 2799 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
681442, 680eqled 11413 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
682439, 441, 681syl2anc 596 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
683438, 682pm2.61dan 825 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
684207, 402, 415, 683fsumle 15966 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
685367, 403, 413, 416, 423, 684le2addd 11935 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤ ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))
686321mpteq1d 5195 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))
687686fveq2d 6889 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = (Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))
688211, 412syldan 603 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
689324, 325, 326, 330, 417, 688sge0splitmpt 47420 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
690687, 689eqtrd 2796 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
691209, 211, 411syl2anc 596 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
692207, 691sge0fsummpt 47399 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
693692, 416eqeltrd 2861 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ)
694 rexadd 13362 . . . . . . . . . . . 12 (((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ ∧ (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
695413, 693, 694syl2anc 596 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +e (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
696692oveq2d 7436 . . . . . . . . . . 11 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + (Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) = ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))
697690, 695, 6963eqtrrd 2801 . . . . . . . . . 10 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))
698685, 697breqtrd 5131 . . . . . . . . 9 (𝜑 → ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))
699404, 279, 200, 408, 698lemul2ad 12257 . . . . . . . 8 (𝜑 → ((1 + 𝐸) · ((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
700399, 699eqbrtrd 5127 . . . . . . 7 (𝜑 → (((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
701196, 278, 280, 314, 700letrd 11467 . . . . . 6 (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
702180, 701eqbrtrd 5127 . . . . 5 (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
703152, 702jca 521 . . . 4 (𝜑 → (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))))
704 oveq1 7427 . . . . . . 7 (𝑧 = 𝑄 → (𝑧 − (𝐴‘𝑍)) = (𝑄 − (𝐴‘𝑍)))
705704oveq2d 7436 . . . . . 6 (𝑧 = 𝑄 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑄 − (𝐴‘𝑍))))
706 fveq2 6885 . . . . . . . . . . 11 (𝑧 = 𝑄 → (𝐻‘𝑧) = (𝐻‘𝑄))
707706fveq1d 6887 . . . . . . . . . 10 (𝑧 = 𝑄 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑄)‘(𝐷‘𝑗)))
708707oveq2d 7436 . . . . . . . . 9 (𝑧 = 𝑄 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))
709708mpteq2dv 5199 . . . . . . . 8 (𝑧 = 𝑄 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))
710709fveq2d 6889 . . . . . . 7 (𝑧 = 𝑄 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))
711710oveq2d 7436 . . . . . 6 (𝑧 = 𝑄 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))
712705, 711breq12d 5116 . . . . 5 (𝑧 = 𝑄 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))))
713712elrab 3645 . . . 4 (𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))))
714703, 713sylibr 237 . . 3 (𝜑 → 𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))})
715714, 68eleqtrrdi 2872 . 2 (𝜑 → 𝑄 ∈ 𝑈)
716 breq2 5107 . . 3 (𝑢 = 𝑄 → (𝑆 < 𝑢 ↔ 𝑆 < 𝑄))
717716rspcev 3577 . 2 ((𝑄 ∈ 𝑈 ∧ 𝑆 < 𝑄) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢)
718715, 144, 717syl2anc 596 1 (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  ifcif 4482  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   Or wor 5558  ran crn 5652   ↾ cres 5653  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422   ↑m cmap 8847  Fincfn 8973  infcinf 9433  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203   · cmul 11205  +∞cpnf 11340  ℝ*cxr 11342   < clt 11343   ≤ cle 11344   − cmin 11541  ℕcn 12335  ℤ≥cuz 12965  ℝ+crp 13120   +e cxad 13239  [,)cico 13478  [,]cicc 13479  ...cfz 13639  Σcsu 15853  ∏cprod 16072  volcvol 25784  Σ^csumge0 47371
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-inf2 9642  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-er 8717  df-map 8849  df-pm 8850  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9504  df-dju 9982  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-q 13076  df-rp 13121  df-xneg 13241  df-xadd 13242  df-xmul 13243  df-ioo 13480  df-ico 13482  df-icc 13483  df-fz 13640  df-fzo 13789  df-fl 13932  df-seq 14145  df-exp 14205  df-hash 14475  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-clim 15655  df-rlim 15656  df-sum 15854  df-prod 16073  df-rest 17593  df-topgen 17614  df-psmet 21670  df-xmet 21671  df-met 21672  df-bl 21673  df-mopn 21674  df-top 23212  df-topon 23229  df-bases 23264  df-cmp 23705  df-ovol 25785  df-vol 25786  df-sumge0 47372
This theorem is used by:  hoidmvlelem3  47606
  Copyright terms: Public domain W3C validator