Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmv1le Structured version   Visualization version   GIF version
Theorem hoidmv1le 47166
Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmv1le.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hoidmv1le.z (𝜑 → 𝑍 ∈ 𝑉)
hoidmv1le.x 𝑋 = {𝑍}
hoidmv1le.a (𝜑 → 𝐴:𝑋⟶ℝ)
hoidmv1le.b (𝜑 → 𝐵:𝑋⟶ℝ)
hoidmv1le.c (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋))
hoidmv1le.d (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋))
hoidmv1le.s (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
Assertion
Ref Expression
hoidmv1le (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑗,𝑘,𝑥   𝐵,𝑎,𝑏,𝑗,𝑘,𝑥   𝐶,𝑎,𝑏,𝑗,𝑘,𝑥   𝐷,𝑎,𝑏,𝑗,𝑘,𝑥   𝑘,𝑉   𝑋,𝑎,𝑏,𝑘,𝑥   𝑗,𝑍,𝑘,𝑥   𝜑,𝑎,𝑏,𝑗,𝑥
Allowed substitution hints:   𝜑(𝑘)   𝐿(𝑥,𝑗,𝑘,𝑎,𝑏)   𝑉(𝑥,𝑗,𝑎,𝑏)   𝑋(𝑗)   𝑍(𝑎,𝑏)
Proof of Theorem hoidmv1le
Dummy variables 𝑖 𝑤 𝑧 𝑦 𝑙 ℎ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmv1le.b . . . . . . . . . 10 (𝜑 → 𝐵:𝑋⟶ℝ)
2 hoidmv1le.z . . . . . . . . . . . 12 (𝜑 → 𝑍 ∈ 𝑉)
3 snidg 4622 . . . . . . . . . . . 12 (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
42, 3syl 18 . . . . . . . . . . 11 (𝜑 → 𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5eleqtrrdi 2876 . . . . . . . . . 10 (𝜑 → 𝑍 ∈ 𝑋)
71, 6ffvelcdmd 7070 . . . . . . . . 9 (𝜑 → (𝐵‘𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑 → 𝐴:𝑋⟶ℝ)
98, 6ffvelcdmd 7070 . . . . . . . . 9 (𝜑 → (𝐴‘𝑍) ∈ ℝ)
107, 9resubcld 11630 . . . . . . . 8 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ)
1110rexrd 11247 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ*)
12 pnfxr 11251 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 13137 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) < +∞)
1511, 13, 14xrltled 13166 . . . . . 6 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
1615ad2antrr 738 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
17 id 23 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
1817eqcomd 2771 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
1918adantl 486 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
2016, 19breqtrd 5131 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
21 simpl 487 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)))
22 simpr 489 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
23 nnex 12230 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝑋 = {𝑍})
27 snfi 9028 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2865 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ∈ Fin)
3029adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
316ne0d 4297 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ≠ ∅)
3231adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋))
3433ffvelcdmda 7069 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑋))
35 elmapi 8834 . . . . . . . . . . . . 13 ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
3634, 35syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
37 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋))
3837ffvelcdmda 7069 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑋))
39 elmapi 8834 . . . . . . . . . . . . 13 ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
4038, 39syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
4125, 30, 32, 36, 40hoidmvn0val 47156 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
425prodeq1i 15960 . . . . . . . . . . . 12 ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
4342a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
442adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑉)
456adantr 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑋)
4636, 45ffvelcdmd 7070 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
4740, 45ffvelcdmd 7070 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
48 volicore 47153 . . . . . . . . . . . . . 14 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
4946, 47, 48syl2anc 595 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
5049recnd 11225 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ)
51 fveq2 6871 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑍))
52 fveq2 6871 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑍))
5351, 52oveq12d 7418 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
5453fveq2d 6875 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5554prodsn 16006 . . . . . . . . . . . 12 ((𝑍 ∈ 𝑉 ∧ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5644, 50, 55syl2anc 595 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5741, 43, 563eqtrd 2804 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5857mpteq2dva 5198 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
59 fveq2 6871 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎‘𝑘) = (𝑎‘𝑙))
60 fveq2 6871 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏‘𝑘) = (𝑏‘𝑙))
6159, 60oveq12d 7418 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑎‘𝑙)[,)(𝑏‘𝑙)))
6261fveq2d 6875 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
6362cbvprodv 15958 . . . . . . . . . . . . . . . . 17 ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))
64 ifeq2 4488 . . . . . . . . . . . . . . . . 17 (∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
6563, 64ax-mp 5 . . . . . . . . . . . . . . . 16 if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (ℝ ↑m 𝑥) ∧ 𝑏 ∈ (ℝ ↑m 𝑥)) → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
6766mpoeq3ia 7478 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
6867mpteq2i 5201 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
6925, 68eqtri 2788 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
7069, 30, 36, 40hoidmvcl 47154 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
71 eqid 2765 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
7270, 71fmptd 7099 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
73 icossicc 13454 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7473a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7572, 74fssd 6713 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
7658, 75feq1dd 6678 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7776ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7824, 77sge0repnf 46958 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞))
7922, 78mpbird 260 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
809ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) ∈ ℝ)
817ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐵‘𝑍) ∈ ℝ)
82 simplr 780 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) < (𝐵‘𝑍))
83 eqid 2765 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))
8446, 83fmptd 7099 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
8584ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
86 eqid 2765 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))
8747, 86fmptd 7099 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
8887ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
89 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
905eleq2i 2857 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ 𝑋 ↔ 𝑘 ∈ {𝑍})
9190biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ 𝑋 → 𝑘 ∈ {𝑍})
92 elsni 4602 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9391, 92syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → 𝑘 = 𝑍)
9493, 53syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9594rgen 3081 . . . . . . . . . . . . . . . . . . . . 21 ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
96 ixpeq2 8897 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
9897a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9998iuneq2i 4974 . . . . . . . . . . . . . . . . . 18 ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
10099a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
10189, 100sseqtrd 3975 . . . . . . . . . . . . . . . 16 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
102101adantr 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
103 id 23 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
104 eqidd 2766 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105 opeq2 4835 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106105sneqd 4597 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107106rspceeqv 3607 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108103, 104, 107syl2anc 595 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109108adantl 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110 elixpsn 8923 . . . . . . . . . . . . . . . . . . 19 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1112, 110syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112111adantr 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113109, 112mpbird 260 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
1145eqcomi 2774 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
115 ixpeq1 8894 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍))
117 fveq2 6871 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍))
11893, 117syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐴‘𝑘) = (𝐴‘𝑍))
119 fveq2 6871 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍))
12093, 119syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐵‘𝑘) = (𝐵‘𝑍))
121118, 120oveq12d 7418 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
122121eqcomd 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝑋 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
123122rgen 3081 . . . . . . . . . . . . . . . . . . . 20 ∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))
124 ixpeq2 8897 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
126116, 125eqtri 2788 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
127126a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
128127adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
129113, 128eleqtrd 2867 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
130102, 129sseldd 3940 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
131 eliun 4956 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
132130, 131sylib 221 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
133 ixpeq1 8894 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = {𝑍} → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1345, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
135134eleq2i 2857 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
136135bilani 509 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
137 elixpsn 8923 . . . . . . . . . . . . . . . . . . . 20 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1382, 137syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
139138adantr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140136, 139mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
141 opex 5436 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⟨𝑍, 𝑥⟩ ∈ V
142141sneqr 4801 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
143142adantl 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144 vex 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝑥 ∈ V)
146 opthg 5450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
1472, 145, 146syl2anc 595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
148147adantr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
149143, 148mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))
150149simprd 500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1511503adant2 1147 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
152 simp2 1153 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
153151, 152eqeltrd 2865 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1541533exp 1135 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
155154adantr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
156155rexlimdv 3164 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
157140, 156mpd 16 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
158157ex 417 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
159158ad2antrr 738 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
160159reximdva 3178 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
161132, 160mpd 16 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
162 eliun 4956 . . . . . . . . . . . 12 (𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
163161, 162sylibr 237 . . . . . . . . . . 11 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → 𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
164163ralrimiva 3157 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
165 dfss3 3928 . . . . . . . . . 10 (((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
166164, 165sylibr 237 . . . . . . . . 9 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
167 eqidd 2766 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)))
168 fveq2 6871 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
169168fveq1d 6873 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
170169adantl 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
171 simpr 489 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
172 fvexd 6886 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ V)
173167, 170, 171, 172fvmptd 6987 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
174 eqidd 2766 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)))
175 fveq2 6871 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
176175fveq1d 6873 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
177176adantl 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
178 fvexd 6886 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ V)
179174, 177, 171, 178fvmptd 6987 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
180173, 179oveq12d 7418 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
181180iuneq2dv 4977 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
182169, 176oveq12d 7418 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
183182cbviunv 4999 . . . . . . . . . . . 12 ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))
184183eqcomi 2774 . . . . . . . . . . 11 ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
185184a1i 11 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
186181, 185eqtr2d 2801 . . . . . . . . 9 (𝜑 → ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
187166, 186sseqtrd 3975 . . . . . . . 8 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
188187ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
189 fvex 6884 . . . . . . . . . . . . . . 15 ((𝐶‘𝑖)‘𝑍) ∈ V
190169, 83, 189fvmpt 6979 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
191 fvex 6884 . . . . . . . . . . . . . . 15 ((𝐷‘𝑖)‘𝑍) ∈ V
192176, 86, 191fvmpt 6979 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
193190, 192oveq12d 7418 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
194193fveq2d 6875 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
195194mpteq2ia 5200 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
196 eqcom 2772 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 ↔ 𝑖 = 𝑗)
197196imbi1i 352 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
198 eqcom 2772 . . . . . . . . . . . . . . . 16 ((((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) ↔ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
199198imbi2i 339 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
200197, 199bitri 278 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
201182, 200mpbi 233 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
202201fveq2d 6875 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
203202cbvmptv 5209 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
204195, 203eqtri 2788 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
205204fveq2i 6874 . . . . . . . . 9 (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
206205a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
207 simpr 489 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
208206, 207eqeltrd 2865 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
209 oveq1 7407 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
210192breq1d 5115 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷‘𝑖)‘𝑍) ≤ 𝑧))
211210, 192ifbieq1d 4508 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))
212190, 211oveq12d 7418 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))
213212fveq2d 6875 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
214213mpteq2ia 5200 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
215 fveq2 6871 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (𝐶‘𝑖) = (𝐶‘ℎ))
216215fveq1d 6873 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → ((𝐶‘𝑖)‘𝑍) = ((𝐶‘ℎ)‘𝑍))
217 fveq2 6871 . . . . . . . . . . . . . . . . . . 19 (𝑖 = ℎ → (𝐷‘𝑖) = (𝐷‘ℎ))
218217fveq1d 6873 . . . . . . . . . . . . . . . . . 18 (𝑖 = ℎ → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘ℎ)‘𝑍))
219218breq1d 5115 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (((𝐷‘𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
220219, 218ifbieq1d 4508 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
221216, 220oveq12d 7418 . . . . . . . . . . . . . . 15 (𝑖 = ℎ → (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))
222221fveq2d 6875 . . . . . . . . . . . . . 14 (𝑖 = ℎ → (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
223222cbvmptv 5209 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
224214, 223eqtri 2788 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
225224a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))))
226 breq2 5109 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷‘ℎ)‘𝑍) ≤ 𝑤 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
227 id 23 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → 𝑤 = 𝑧)
228226, 227ifbieq2d 4510 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
229228eqcomd 2771 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))
230229oveq2d 7416 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))
231230fveq2d 6875 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))
232231mpteq2dv 5199 . . . . . . . . . . 11 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))
233225, 232eqtr2d 2801 . . . . . . . . . 10 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))
234233fveq2d 6875 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))))
235209, 234breq12d 5118 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))))
236235cbvrabv 3427 . . . . . . 7 {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))}
237 eqid 2765 . . . . . . 7 sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < )
23880, 81, 82, 85, 88, 188, 208, 236, 237hoidmv1lelem3 47165 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))))
239238, 206breqtrd 5131 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24021, 79, 239syl2anc 595 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24120, 240pm2.61dan 824 . . 3 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24225, 29, 31, 8, 1hoidmvn0val 47156 . . . . . . 7 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
24326prodeq1d 15964 . . . . . . 7 (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
244 volicore 47153 . . . . . . . . . 10 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
2459, 7, 244syl2anc 595 . . . . . . . . 9 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
246245recnd 11225 . . . . . . . 8 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ)
247117, 119oveq12d 7418 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
248247fveq2d 6875 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
249248prodsn 16006 . . . . . . . 8 ((𝑍 ∈ 𝑉 ∧ (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
2502, 246, 249syl2anc 595 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
251242, 243, 2503eqtrd 2804 . . . . . 6 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
252251adantr 485 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
253 volico 46555 . . . . . . 7 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
2549, 7, 253syl2anc 595 . . . . . 6 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
255254adantr 485 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
256 iftrue 4489 . . . . . 6 ((𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
257256adantl 486 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
258252, 255, 2573eqtrd 2804 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
25958fveq2d 6875 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
260259adantr 485 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
261258, 260breq12d 5118 . . 3 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ↔ ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))))
262241, 261mpbird 260 . 2 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
263242adantr 485 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
264243adantr 485 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
265250adantr 485 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
266254adantr 485 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
267 iffalse 4492 . . . . . 6 (¬ (𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
268267adantl 486 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
269265, 266, 2683eqtrd 2804 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
270263, 264, 2693eqtrd 2804 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
27123a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
272271, 75sge0ge0 46956 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
273272adantr 485 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
274270, 273eqbrtrd 5127 . 2 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
275262, 274pm2.61dan 824 1 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  {crab 3417  Vcvv 3457   ⊆ wss 3907  ∅c0 4288  ifcif 4483  {csn 4585  ⟨cop 4591  ∪ ciun 4952   class class class wbr 5105   ↦ cmpt 5186  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400   ∈ cmpo 7402   ↑m cmap 8812  Xcixp 8883  Fincfn 8931  supcsup 9388  ℂcc 11086  ℝcr 11087  0cc0 11088  +∞cpnf 11228  ℝ*cxr 11230   < clt 11231   ≤ cle 11232   − cmin 11429  ℕcn 12224  [,)cico 13365  [,]cicc 13366  ∏cprod 15947  volcvol 25583  Σ^csumge0 46934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-inf2 9598  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-se 5606  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-er 8682  df-map 8814  df-pm 8815  df-ixp 8884  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-fi 9359  df-sup 9390  df-inf 9391  df-oi 9460  df-dju 9875  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-3 12295  df-n0 12496  df-z 12583  df-uz 12854  df-q 12964  df-rp 13008  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ioo 13367  df-ico 13369  df-icc 13370  df-fz 13527  df-fzo 13674  df-fl 13816  df-seq 14029  df-exp 14089  df-hash 14358  df-cj 15140  df-re 15141  df-im 15142  df-sqrt 15276  df-abs 15277  df-clim 15529  df-rlim 15530  df-sum 15728  df-prod 15948  df-rest 17465  df-topgen 17486  df-psmet 21474  df-xmet 21475  df-met 21476  df-bl 21477  df-mopn 21478  df-top 23012  df-topon 23029  df-bases 23064  df-cmp 23505  df-ovol 25584  df-vol 25585  df-sumge0 46935
This theorem is referenced by:  hoidmvle  47172
  Copyright terms: Public domain W3C validator