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 46609
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 4660 . . . . . . . . . . . 12 (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑 → 𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5eleqtrrdi 2852 . . . . . . . . . 10 (𝜑 → 𝑍 ∈ 𝑋)
71, 6ffvelcdmd 7105 . . . . . . . . 9 (𝜑 → (𝐵‘𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑 → 𝐴:𝑋⟶ℝ)
98, 6ffvelcdmd 7105 . . . . . . . . 9 (𝜑 → (𝐴‘𝑍) ∈ ℝ)
107, 9resubcld 11691 . . . . . . . 8 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ)
1110rexrd 11311 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ*)
12 pnfxr 11315 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 13163 . . . . . . 7 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) < +∞)
1511, 13, 14xrltled 13192 . . . . . 6 (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
1615ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
1817eqcomd 2743 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
1918adantl 481 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
2016, 19breqtrd 5169 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
21 simpl 482 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)))
22 simpr 484 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞)
23 nnex 12272 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝑋 = {𝑍})
27 snfi 9083 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2841 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ∈ Fin)
3029adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
316ne0d 4342 . . . . . . . . . . . . 13 (𝜑 → 𝑋 ≠ ∅)
3231adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋))
3433ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑋))
35 elmapi 8889 . . . . . . . . . . . . 13 ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
3634, 35syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
37 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋))
3837ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑋))
39 elmapi 8889 . . . . . . . . . . . . 13 ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
4038, 39syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
4125, 30, 32, 36, 40hoidmvn0val 46599 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
425prodeq1i 15952 . . . . . . . . . . . 12 ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
4342a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
442adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑉)
456adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑋)
4636, 45ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ)
4740, 45ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ)
48 volicore 46596 . . . . . . . . . . . . . 14 ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
4946, 47, 48syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℝ)
5049recnd 11289 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ)
51 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑍))
52 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑍))
5351, 52oveq12d 7449 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
5453fveq2d 6910 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5554prodsn 15998 . . . . . . . . . . . 12 ((𝑍 ∈ 𝑉 ∧ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5644, 50, 55syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5741, 43, 563eqtrd 2781 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
5857mpteq2dva 5242 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
59 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎‘𝑘) = (𝑎‘𝑙))
60 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏‘𝑘) = (𝑏‘𝑙))
6159, 60oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑎‘𝑙)[,)(𝑏‘𝑙)))
6261fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))
6362cbvprodv 15950 . . . . . . . . . . . . . . . . 17 ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))
64 ifeq2 4530 . . . . . . . . . . . . . . . . 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 7511 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙)))))
6867mpteq2i 5247 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
6925, 68eqtri 2765 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙 ∈ 𝑥 (vol‘((𝑎‘𝑙)[,)(𝑏‘𝑙))))))
7069, 30, 36, 40hoidmvcl 46597 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
71 eqid 2737 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
7270, 71fmptd 7134 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
73 icossicc 13476 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7473a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7572, 74fssd 6753 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
7658, 75feq1dd 6721 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7776ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7824, 77sge0repnf 46401 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞))
7922, 78mpbird 257 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
809ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) ∈ ℝ)
817ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐵‘𝑍) ∈ ℝ)
82 simplr 769 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝐴‘𝑍) < (𝐵‘𝑍))
83 eqid 2737 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))
8446, 83fmptd 7134 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
8584ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)):ℕ⟶ℝ)
86 eqid 2737 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))
8747, 86fmptd 7134 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
8887ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)):ℕ⟶ℝ)
89 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
905eleq2i 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ 𝑋 ↔ 𝑘 ∈ {𝑍})
9190biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ 𝑋 → 𝑘 ∈ {𝑍})
92 elsni 4643 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → 𝑘 = 𝑍)
9493, 53syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9594rgen 3063 . . . . . . . . . . . . . . . . . . . . 21 ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
96 ixpeq2 8951 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
9897a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
9998iuneq2i 5013 . . . . . . . . . . . . . . . . . 18 ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
10099a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
10189, 100sseqtrd 4020 . . . . . . . . . . . . . . . 16 (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
102101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
103 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
104 eqidd 2738 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105 opeq2 4874 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106105sneqd 4638 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107106rspceeqv 3645 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108103, 104, 107syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109108adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110 elixpsn 8977 . . . . . . . . . . . . . . . . . . 19 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1112, 110syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112111adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ↔ ∃𝑦 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113109, 112mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
1145eqcomi 2746 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
115 ixpeq1 8948 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍))
117 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍))
11893, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐴‘𝑘) = (𝐴‘𝑍))
119 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍))
12093, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ 𝑋 → (𝐵‘𝑘) = (𝐵‘𝑍))
121118, 120oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ 𝑋 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
122121eqcomd 2743 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝑋 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
123122rgen 3063 . . . . . . . . . . . . . . . . . . . 20 ∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))
124 ixpeq2 8951 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ 𝑋 ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
126116, 125eqtri 2765 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))
127126a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
128127adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → X𝑘 ∈ {𝑍} ((𝐴‘𝑍)[,)(𝐵‘𝑍)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
129113, 128eleqtrd 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
130102, 129sseldd 3984 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
131 eliun 4995 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
132130, 131sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
133 ixpeq1 8948 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1345, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
135134eleq2i 2833 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
136135biimpi 216 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
137136adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
138 elixpsn 8977 . . . . . . . . . . . . . . . . . . . 20 (𝑍 ∈ 𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1392, 138syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140139adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
141137, 140mpbid 232 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
142 opex 5469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⟨𝑍, 𝑥⟩ ∈ V
143142sneqr 4840 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144143adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
145 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
146145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝑥 ∈ V)
147 opthg 5482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍 ∈ 𝑉 ∧ 𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
1482, 146, 147syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
149148adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍 ∧ 𝑥 = 𝑦)))
150144, 149mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍 ∧ 𝑥 = 𝑦))
151150simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1521513adant2 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
153 simp2 1138 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
154152, 153eqeltrd 2841 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
1551543exp 1120 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
156155adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
157156rexlimdv 3153 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
158141, 157mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
159158ex 412 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
160159ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
161160reximdva 3168 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
162132, 161mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
163 eliun 4995 . . . . . . . . . . . 12 (𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
164162, 163sylibr 234 . . . . . . . . . . 11 ((𝜑 ∧ 𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))) → 𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
165164ralrimiva 3146 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
166 dfss3 3972 . . . . . . . . . 10 (((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴‘𝑍)[,)(𝐵‘𝑍))𝑥 ∈ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
167165, 166sylibr 234 . . . . . . . . 9 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
168 eqidd 2738 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍)))
169 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
170169fveq1d 6908 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
171170adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍))
172 simpr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
173 fvexd 6921 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ V)
174168, 171, 172, 173fvmptd 7023 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
175 eqidd 2738 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍)))
176 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
177176fveq1d 6908 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
178177adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍))
179 fvexd 6921 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ V)
180175, 178, 172, 179fvmptd 7023 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
181174, 180oveq12d 7449 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
182181iuneq2dv 5016 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
183170, 177oveq12d 7449 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
184183cbviunv 5040 . . . . . . . . . . . 12 ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))
185184eqcomi 2746 . . . . . . . . . . 11 ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))
186185a1i 11 . . . . . . . . . 10 (𝜑 → ∪ 𝑖 ∈ ℕ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
187182, 186eqtr2d 2778 . . . . . . . . 9 (𝜑 → ∪ 𝑗 ∈ ℕ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
188167, 187sseqtrd 4020 . . . . . . . 8 (𝜑 → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
189188ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴‘𝑍)[,)(𝐵‘𝑍)) ⊆ ∪ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))
190 fvex 6919 . . . . . . . . . . . . . . 15 ((𝐶‘𝑖)‘𝑍) ∈ V
191170, 83, 190fvmpt 7016 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖) = ((𝐶‘𝑖)‘𝑍))
192 fvex 6919 . . . . . . . . . . . . . . 15 ((𝐷‘𝑖)‘𝑍) ∈ V
193177, 86, 192fvmpt 7016 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) = ((𝐷‘𝑖)‘𝑍))
194191, 193oveq12d 7449 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))
195194fveq2d 6910 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
196195mpteq2ia 5245 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
197 eqcom 2744 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 ↔ 𝑖 = 𝑗)
198197imbi1i 349 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))))
199 eqcom 2744 . . . . . . . . . . . . . . . 16 ((((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) ↔ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
200199imbi2i 336 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
201198, 200bitri 275 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
202183, 201mpbi 230 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))
203202fveq2d 6910 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
204203cbvmptv 5255 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
205196, 204eqtri 2765 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))
206205fveq2i 6909 . . . . . . . . 9 (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))
207206a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
208 simpr 484 . . . . . . . 8 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ)
209207, 208eqeltrd 2841 . . . . . . 7 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
210 oveq1 7438 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
211193breq1d 5153 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷‘𝑖)‘𝑍) ≤ 𝑧))
212211, 193ifbieq1d 4550 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))
213191, 212oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))
214213fveq2d 6910 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
215214mpteq2ia 5245 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))))
216 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (𝐶‘𝑖) = (𝐶‘ℎ))
217216fveq1d 6908 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → ((𝐶‘𝑖)‘𝑍) = ((𝐶‘ℎ)‘𝑍))
218 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑖 = ℎ → (𝐷‘𝑖) = (𝐷‘ℎ))
219218fveq1d 6908 . . . . . . . . . . . . . . . . . 18 (𝑖 = ℎ → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘ℎ)‘𝑍))
220219breq1d 5153 . . . . . . . . . . . . . . . . 17 (𝑖 = ℎ → (((𝐷‘𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
221220, 219ifbieq1d 4550 . . . . . . . . . . . . . . . 16 (𝑖 = ℎ → if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
222217, 221oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑖 = ℎ → (((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))
223222fveq2d 6910 . . . . . . . . . . . . . 14 (𝑖 = ℎ → (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
224223cbvmptv 5255 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶‘𝑖)‘𝑍)[,)if(((𝐷‘𝑖)‘𝑍) ≤ 𝑧, ((𝐷‘𝑖)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
225215, 224eqtri 2765 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))))
226225a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))))
227 breq2 5147 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷‘ℎ)‘𝑍) ≤ 𝑤 ↔ ((𝐷‘ℎ)‘𝑍) ≤ 𝑧))
228 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → 𝑤 = 𝑧)
229227, 228ifbieq2d 4552 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))
230229eqcomd 2743 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧) = if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))
231230oveq2d 7447 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)) = (((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))
232231fveq2d 6910 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧))) = (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))
233232mpteq2dv 5244 . . . . . . . . . . 11 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑧, ((𝐷‘ℎ)‘𝑍), 𝑧)))) = (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))
234226, 233eqtr2d 2778 . . . . . . . . . 10 (𝑤 = 𝑧 → (ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))
235234fveq2d 6910 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧))))))
236210, 235breq12d 5156 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))))
237236cbvrabv 3447 . . . . . . 7 {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑧 − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖), 𝑧)))))}
238 eqid 2737 . . . . . . 7 sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝑤 − (𝐴‘𝑍)) ≤ (Σ^‘(ℎ ∈ ℕ ↦ (vol‘(((𝐶‘ℎ)‘𝑍)[,)if(((𝐷‘ℎ)‘𝑍) ≤ 𝑤, ((𝐷‘ℎ)‘𝑍), 𝑤)))))}, ℝ, < )
23980, 81, 82, 85, 88, 189, 209, 237, 238hoidmv1lelem3 46608 . . . . . 6 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷‘𝑗)‘𝑍))‘𝑖))))))
240239, 207breqtrd 5169 . . . . 5 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24121, 79, 240syl2anc 584 . . . 4 (((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))) = +∞) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24220, 241pm2.61dan 813 . . 3 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
24325, 29, 31, 8, 1hoidmvn0val 46599 . . . . . . 7 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
24426prodeq1d 15956 . . . . . . 7 (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
245 volicore 46596 . . . . . . . . . 10 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
2469, 7, 245syl2anc 584 . . . . . . . . 9 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ)
247246recnd 11289 . . . . . . . 8 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ)
248117, 119oveq12d 7449 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍)))
249248fveq2d 6910 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
250249prodsn 15998 . . . . . . . 8 ((𝑍 ∈ 𝑉 ∧ (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
2512, 247, 250syl2anc 584 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
252243, 244, 2513eqtrd 2781 . . . . . 6 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
253252adantr 480 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
254 volico 45998 . . . . . . 7 (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
2559, 7, 254syl2anc 584 . . . . . 6 (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
256255adantr 480 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
257 iftrue 4531 . . . . . 6 ((𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
258257adantl 481 . . . . 5 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
259253, 256, 2583eqtrd 2781 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ((𝐵‘𝑍) − (𝐴‘𝑍)))
26058fveq2d 6910 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
261260adantr 480 . . . 4 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))))))
262259, 261breq12d 5156 . . 3 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → ((𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ↔ ((𝐵‘𝑍) − (𝐴‘𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))))))
263242, 262mpbird 257 . 2 ((𝜑 ∧ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
264243adantr 480 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
265244adantr 480 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
266251adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))
267255adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) = if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0))
268 iffalse 4534 . . . . . 6 (¬ (𝐴‘𝑍) < (𝐵‘𝑍) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
269268adantl 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → if((𝐴‘𝑍) < (𝐵‘𝑍), ((𝐵‘𝑍) − (𝐴‘𝑍)), 0) = 0)
270266, 267, 2693eqtrd 2781 . . . 4 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)
271264, 265, 2703eqtrd 2781 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) = 0)
27223a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
273272, 75sge0ge0 46399 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
274273adantr 480 . . 3 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
275271, 274eqbrtrd 5165 . 2 ((𝜑 ∧ ¬ (𝐴‘𝑍) < (𝐵‘𝑍)) → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
276263, 275pm2.61dan 813 1 (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3436  Vcvv 3480   ⊆ wss 3951  ∅c0 4333  ifcif 4525  {csn 4626  ⟨cop 4632  ∪ ciun 4991   class class class wbr 5143   ↦ cmpt 5225  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431   ∈ cmpo 7433   ↑m cmap 8866  Xcixp 8937  Fincfn 8985  supcsup 9480  ℂcc 11153  ℝcr 11154  0cc0 11155  +∞cpnf 11292  ℝ*cxr 11294   < clt 11295   ≤ cle 11296   − cmin 11492  ℕcn 12266  [,)cico 13389  [,]cicc 13390  ∏cprod 15939  volcvol 25498  Σ^csumge0 46377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-prod 15940  df-rest 17467  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953  df-cmp 23395  df-ovol 25499  df-vol 25500  df-sumge0 46378
This theorem is referenced by:  hoidmvle  46615
  Copyright terms: Public domain W3C validator