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 47291
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 4627 . . . . . . . . . . . 12 (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
42, 3syl 18 . . . . . . . . . . 11 (𝜑 → 𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5eleqtrrdi 2874 . . . . . . . . . 10 (𝜑 → 𝑍 ∈ 𝑋)
71, 6ffvelcdmd 7082 . . . . . . . . 9 (𝜑 → (𝐵‘𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑 → 𝐴:𝑋⟶ℝ)
98, 6ffvelcdmd 7082 . . . . . . . . 9 (𝜑 → (𝐴‘𝑍) ∈ ℝ)
107, 9resubcld 11643 . . . . . . . 8 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ)
1110rexrd 11260 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ*)
12 pnfxr 11264 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 13147 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) < +∞)
1511, 13, 14xrltled 13176 . . . . . 6 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
1615ad2antrr 738 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
17 id 23 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
1817eqcomd 2769 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
1918adantl 486 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
2016, 19breqtrd 5138 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
21 simpl 487 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)))
22 simpr 489 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
23 nnex 12240 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝑋 = {𝑍})
27 snfi 9041 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2863 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ∈ Fin)
3029adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
316ne0d 4296 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ≠ ∅)
3231adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋))
3433ffvelcdmda 7081 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑋))
35 elmapi 8847 . . . . . . . . . . . . 13 ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
3634, 35syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
37 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋))
3837ffvelcdmda 7081 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑋))
39 elmapi 8847 . . . . . . . . . . . . 13 ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
4038, 39syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
4125, 30, 32, 36, 40hoidmvn0val 47281 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
425prodeq1i 15972 . . . . . . . . . . . 12 ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
4342a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
442adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑉)
456adantr 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑋)
4636, 45ffvelcdmd 7082 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
4740, 45ffvelcdmd 7082 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
48 volicore 47278 . . . . . . . . . . . . . 14 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
4946, 47, 48syl2anc 595 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
5049recnd 11238 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ)
51 fveq2 6883 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑍))
52 fveq2 6883 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑍))
5351, 52oveq12d 7430 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
5453fveq2d 6887 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5554prodsn 16018 . . . . . . . . . . . 12 ((𝑍 ∈ 𝑉 ∧ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5644, 50, 55syl2anc 595 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5741, 43, 563eqtrd 2802 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5857mpteq2dva 5205 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
59 fveq2 6883 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎‘𝑘) = (𝑎‘𝑙))
60 fveq2 6883 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏‘𝑘) = (𝑏‘𝑙))
6159, 60oveq12d 7430 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑎‘𝑙)[,)(𝑏‘𝑙)))
6261fveq2d 6887 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
6362cbvprodv 15970 . . . . . . . . . . . . . . . . 17 ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))
64 ifeq2 4493 . . . . . . . . . . . . . . . . 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 7490 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
6867mpteq2i 5208 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
6925, 68eqtri 2786 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
7069, 30, 36, 40hoidmvcl 47279 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
71 eqid 2763 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
7270, 71fmptd 7111 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
73 icossicc 13464 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7473a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7572, 74fssd 6725 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
7658, 75feq1dd 6690 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7776ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7824, 77sge0repnf 47083 . . . . . 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 2763 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))
8446, 83fmptd 7111 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
8584ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
86 eqid 2763 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))
8747, 86fmptd 7111 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
8887ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
89 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
905eleq2i 2855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ 𝑋 ↔ 𝑘 ∈ {𝑍})
9190biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ 𝑋 → 𝑘 ∈ {𝑍})
92 elsni 4607 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9391, 92syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → 𝑘 = 𝑍)
9493, 53syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9594rgen 3081 . . . . . . . . . . . . . . . . . . . . 21 ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
96 ixpeq2 8910 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
9897a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9998iuneq2i 4979 . . . . . . . . . . . . . . . . . 18 ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
10099a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
10189, 100sseqtrd 3974 . . . . . . . . . . . . . . . 16 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
102101adantr 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
103 id 23 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
104 eqidd 2764 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105 opeq2 4840 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106105sneqd 4602 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107106rspceeqv 3605 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108103, 104, 107syl2anc 595 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109108adantl 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110 elixpsn 8936 . . . . . . . . . . . . . . . . . . 19 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1112, 110syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112111adantr 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113109, 112mpbird 260 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
1145eqcomi 2772 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
115 ixpeq1 8907 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍))
117 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍))
11893, 117syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐴‘𝑘) = (𝐴‘𝑍))
119 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍))
12093, 119syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐵‘𝑘) = (𝐵‘𝑍))
121118, 120oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
122121eqcomd 2769 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝑋 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
123122rgen 3081 . . . . . . . . . . . . . . . . . . . 20 ∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))
124 ixpeq2 8910 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
126116, 125eqtri 2786 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
127126a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
128127adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
129113, 128eleqtrd 2865 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
130102, 129sseldd 3939 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
131 eliun 4961 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
132130, 131sylib 221 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
133 ixpeq1 8907 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = {𝑍} → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1345, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
135134eleq2i 2855 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
136135bilani 509 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
137 elixpsn 8936 . . . . . . . . . . . . . . . . . . . 20 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1382, 137syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
139138adantr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140136, 139mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
141 opex 5447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⟨𝑍, 𝑥⟩ ∈ V
142141sneqr 4806 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
143142adantl 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144 vex 3459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝑥 ∈ V)
146 opthg 5461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
1472, 145, 146syl2anc 595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
148147adantr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
149143, 148mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))
150149simprd 500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1511503adant2 1149 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
152 simp2 1155 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
153151, 152eqeltrd 2863 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1541533exp 1137 . . . . . . . . . . . . . . . . . . 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 4961 . . . . . . . . . . . 12 (𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
163161, 162sylibr 237 . . . . . . . . . . 11 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → 𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
164163ralrimiva 3157 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
165 dfss3 3927 . . . . . . . . . 10 (((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
166164, 165sylibr 237 . . . . . . . . 9 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
167 eqidd 2764 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)))
168 fveq2 6883 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
169168fveq1d 6885 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
170169adantl 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
171 simpr 489 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
172 fvexd 6898 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ V)
173167, 170, 171, 172fvmptd 6999 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
174 eqidd 2764 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)))
175 fveq2 6883 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
176175fveq1d 6885 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
177176adantl 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
178 fvexd 6898 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ V)
179174, 177, 171, 178fvmptd 6999 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
180173, 179oveq12d 7430 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
181180iuneq2dv 4982 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
182169, 176oveq12d 7430 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
183182cbviunv 5004 . . . . . . . . . . . 12 ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))
184183eqcomi 2772 . . . . . . . . . . 11 ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
185184a1i 11 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
186181, 185eqtr2d 2799 . . . . . . . . 9 (𝜑 → ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
187166, 186sseqtrd 3974 . . . . . . . 8 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
188187ad2antrr 738 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
189 fvex 6896 . . . . . . . . . . . . . . 15 ((𝐶‘𝑖)‘𝑍) ∈ V
190169, 83, 189fvmpt 6991 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
191 fvex 6896 . . . . . . . . . . . . . . 15 ((𝐷‘𝑖)‘𝑍) ∈ V
192176, 86, 191fvmpt 6991 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
193190, 192oveq12d 7430 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
194193fveq2d 6887 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
195194mpteq2ia 5207 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
196 eqcom 2770 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 ↔ 𝑖 = 𝑗)
197196imbi1i 352 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
198 eqcom 2770 . . . . . . . . . . . . . . . 16 ((((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) ↔ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
199198imbi2i 339 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
200197, 199bitri 278 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
201182, 200mpbi 233 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
202201fveq2d 6887 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
203202cbvmptv 5216 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
204195, 203eqtri 2786 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
205204fveq2i 6886 . . . . . . . . 9 (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
206205a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
207 simpr 489 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
208206, 207eqeltrd 2863 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
209 oveq1 7419 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
210192breq1d 5120 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷‘𝑖)‘𝑍) ≤ 𝑧))
211210, 192ifbieq1d 4513 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))
212190, 211oveq12d 7430 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))
213212fveq2d 6887 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
214213mpteq2ia 5207 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
215 fveq2 6883 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (𝐶‘𝑖) = (𝐶‘ℎ))
216215fveq1d 6885 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → ((𝐶‘𝑖)‘𝑍) = ((𝐶‘ℎ)‘𝑍))
217 fveq2 6883 . . . . . . . . . . . . . . . . . . 19 (𝑖 = ℎ → (𝐷‘𝑖) = (𝐷‘ℎ))
218217fveq1d 6885 . . . . . . . . . . . . . . . . . 18 (𝑖 = ℎ → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘ℎ)‘𝑍))
219218breq1d 5120 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (((𝐷‘𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
220219, 218ifbieq1d 4513 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
221216, 220oveq12d 7430 . . . . . . . . . . . . . . 15 (𝑖 = ℎ → (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))
222221fveq2d 6887 . . . . . . . . . . . . . 14 (𝑖 = ℎ → (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
223222cbvmptv 5216 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
224214, 223eqtri 2786 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
225224a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))))
226 breq2 5114 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷‘ℎ)‘𝑍) ≤ 𝑤 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
227 id 23 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → 𝑤 = 𝑧)
228226, 227ifbieq2d 4515 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
229228eqcomd 2769 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))
230229oveq2d 7428 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))
231230fveq2d 6887 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))
232231mpteq2dv 5206 . . . . . . . . . . 11 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))
233225, 232eqtr2d 2799 . . . . . . . . . 10 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))
234233fveq2d 6887 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))))
235209, 234breq12d 5123 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))))
236235cbvrabv 3426 . . . . . . 7 {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))}
237 eqid 2763 . . . . . . 7 sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < )
23880, 81, 82, 85, 88, 188, 208, 236, 237hoidmv1lelem3 47290 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))))
239238, 206breqtrd 5138 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24021, 79, 239syl2anc 595 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24120, 240pm2.61dan 824 . . 3 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24225, 29, 31, 8, 1hoidmvn0val 47281 . . . . . . 7 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
24326prodeq1d 15976 . . . . . . 7 (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
244 volicore 47278 . . . . . . . . . 10 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
2459, 7, 244syl2anc 595 . . . . . . . . 9 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
246245recnd 11238 . . . . . . . 8 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ)
247117, 119oveq12d 7430 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
248247fveq2d 6887 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
249248prodsn 16018 . . . . . . . 8 ((𝑍 ∈ 𝑉 ∧ (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
2502, 246, 249syl2anc 595 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
251242, 243, 2503eqtrd 2802 . . . . . 6 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
252251adantr 485 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
253 volico 46680 . . . . . . 7 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
2549, 7, 253syl2anc 595 . . . . . 6 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
255254adantr 485 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
256 iftrue 4494 . . . . . 6 ((𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
257256adantl 486 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
258252, 255, 2573eqtrd 2802 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
25958fveq2d 6887 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
260259adantr 485 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
261258, 260breq12d 5123 . . 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 4497 . . . . . 6 (¬ (𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
268267adantl 486 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
269265, 266, 2683eqtrd 2802 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
270263, 264, 2693eqtrd 2802 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
27123a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
272271, 75sge0ge0 47081 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
273272adantr 485 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
274270, 273eqbrtrd 5134 . 2 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
275262, 274pm2.61dan 824 1 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  {crab 3416  Vcvv 3455   ⊆ wss 3906  ∅c0 4287  ifcif 4488  {csn 4590  ⟨cop 4596  ∪ ciun 4957   class class class wbr 5110   ↦ cmpt 5193  ⟶wf 6534  ‘cfv 6538  (class class class)co 7412   ∈ cmpo 7414   ↑m cmap 8825  Xcixp 8896  Fincfn 8944  supcsup 9401  ℂcc 11099  ℝcr 11100  0cc0 11101  +∞cpnf 11241  ℝ*cxr 11243   < clt 11244   ≤ cle 11245   − cmin 11442  ℕcn 12234  [,)cico 13375  [,]cicc 13376  ∏cprod 15959  volcvol 25603  Σ^csumge0 47059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-inf2 9611  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178  ax-pre-sup 11179
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  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 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7676  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-2o 8455  df-er 8695  df-map 8827  df-pm 8828  df-ixp 8897  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-fi 9372  df-sup 9403  df-inf 9404  df-oi 9473  df-dju 9888  df-card 9926  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-div 11873  df-nn 12235  df-2 12304  df-3 12305  df-n0 12506  df-z 12593  df-uz 12864  df-q 12974  df-rp 13018  df-xneg 13138  df-xadd 13139  df-xmul 13140  df-ioo 13377  df-ico 13379  df-icc 13380  df-fz 13537  df-fzo 13685  df-fl 13827  df-seq 14040  df-exp 14100  df-hash 14369  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-rlim 15542  df-sum 15740  df-prod 15960  df-rest 17476  df-topgen 17497  df-psmet 21495  df-xmet 21496  df-met 21497  df-bl 21498  df-mopn 21499  df-top 23032  df-topon 23049  df-bases 23084  df-cmp 23525  df-ovol 25604  df-vol 25605  df-sumge0 47060
This theorem is referenced by:  hoidmvle  47297
  Copyright terms: Public domain W3C validator