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

Theorem hoidmv1lelem3 41601
Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmv1lelem3.a (𝜑𝐴 ∈ ℝ)
hoidmv1lelem3.b (𝜑𝐵 ∈ ℝ)
hoidmv1lelem3.l (𝜑𝐴 < 𝐵)
hoidmv1lelem3.c (𝜑𝐶:ℕ⟶ℝ)
hoidmv1lelem3.d (𝜑𝐷:ℕ⟶ℝ)
hoidmv1lelem3.x (𝜑 → (𝐴[,)𝐵) ⊆ 𝑗 ∈ ℕ ((𝐶𝑗)[,)(𝐷𝑗)))
hoidmv1lelem3.r (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
hoidmv1lelem3.u 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
hoidmv1lelem3.s 𝑆 = sup(𝑈, ℝ, < )
Assertion
Ref Expression
hoidmv1lelem3 (𝜑 → (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
Distinct variable groups:   𝐴,𝑗,𝑧   𝐵,𝑗,𝑧   𝐶,𝑗,𝑧   𝐷,𝑗,𝑧   𝑆,𝑗,𝑧   𝑈,𝑗,𝑧   𝜑,𝑗,𝑧

Proof of Theorem hoidmv1lelem3
Dummy variables 𝑦 𝑖 𝑢 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmv1lelem3.b . . 3 (𝜑𝐵 ∈ ℝ)
2 hoidmv1lelem3.a . . 3 (𝜑𝐴 ∈ ℝ)
31, 2resubcld 10782 . 2 (𝜑 → (𝐵𝐴) ∈ ℝ)
4 nnex 11357 . . . . . . 7 ℕ ∈ V
54a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
6 icossicc 12549 . . . . . . . 8 (0[,)+∞) ⊆ (0[,]+∞)
7 0xr 10403 . . . . . . . . . 10 0 ∈ ℝ*
87a1i 11 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 0 ∈ ℝ*)
9 pnfxr 10410 . . . . . . . . . 10 +∞ ∈ ℝ*
109a1i 11 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → +∞ ∈ ℝ*)
11 hoidmv1lelem3.c . . . . . . . . . . . 12 (𝜑𝐶:ℕ⟶ℝ)
1211ffvelrnda 6608 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ)
13 hoidmv1lelem3.d . . . . . . . . . . . . 13 (𝜑𝐷:ℕ⟶ℝ)
1413ffvelrnda 6608 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ)
151adantr 474 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝐵 ∈ ℝ)
1614, 15ifcld 4351 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ∈ ℝ)
17 volicore 41589 . . . . . . . . . . 11 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ∈ ℝ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ∈ ℝ)
1812, 16, 17syl2anc 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ∈ ℝ)
1918rexrd 10406 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ∈ ℝ*)
2016rexrd 10406 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ∈ ℝ*)
21 icombl 23730 . . . . . . . . . . 11 (((𝐶𝑗) ∈ ℝ ∧ if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ∈ ℝ*) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ∈ dom vol)
2212, 20, 21syl2anc 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ∈ dom vol)
23 volge0 40971 . . . . . . . . . 10 (((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ∈ dom vol → 0 ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))
2422, 23syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 0 ≤ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))
2518ltpnfd 12241 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) < +∞)
268, 10, 19, 24, 25elicod 12512 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ∈ (0[,)+∞))
276, 26sseldi 3825 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ∈ (0[,]+∞))
28 eqid 2825 . . . . . . 7 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))
2927, 28fmptd 6633 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))):ℕ⟶(0[,]+∞))
305, 29sge0xrcl 41393 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) ∈ ℝ*)
319a1i 11 . . . . 5 (𝜑 → +∞ ∈ ℝ*)
32 hoidmv1lelem3.r . . . . . . 7 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ)
3332rexrd 10406 . . . . . 6 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) ∈ ℝ*)
34 nfv 2015 . . . . . . 7 𝑗𝜑
35 volf 23695 . . . . . . . . 9 vol:dom vol⟶(0[,]+∞)
3635a1i 11 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
3714rexrd 10406 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ ℝ*)
38 icombl 23730 . . . . . . . . 9 (((𝐶𝑗) ∈ ℝ ∧ (𝐷𝑗) ∈ ℝ*) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
3912, 37, 38syl2anc 581 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol)
4036, 39ffvelrnd 6609 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)(𝐷𝑗))) ∈ (0[,]+∞))
4112rexrd 10406 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ ℝ*)
4212leidd 10918 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ≤ (𝐶𝑗))
43 min1 12308 . . . . . . . . . 10 (((𝐷𝑗) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ≤ (𝐷𝑗))
4414, 15, 43syl2anc 581 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ≤ (𝐷𝑗))
45 icossico 12531 . . . . . . . . 9 ((((𝐶𝑗) ∈ ℝ* ∧ (𝐷𝑗) ∈ ℝ*) ∧ ((𝐶𝑗) ≤ (𝐶𝑗) ∧ if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) ≤ (𝐷𝑗))) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
4641, 37, 42, 44, 45syl22anc 874 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗)))
47 volss 23699 . . . . . . . 8 ((((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ∈ dom vol ∧ ((𝐶𝑗)[,)(𝐷𝑗)) ∈ dom vol ∧ ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)) ⊆ ((𝐶𝑗)[,)(𝐷𝑗))) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
4822, 39, 46, 47syl3anc 1496 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))) ≤ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
4934, 5, 27, 40, 48sge0lempt 41418 . . . . . 6 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
5032ltpnfd 12241 . . . . . 6 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))) < +∞)
5130, 33, 31, 49, 50xrlelttrd 12279 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) < +∞)
5230, 31, 51xrltned 40370 . . . 4 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) ≠ +∞)
5352neneqd 3004 . . 3 (𝜑 → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) = +∞)
545, 29sge0repnf 41394 . . 3 (𝜑 → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) = +∞))
5553, 54mpbird 249 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))) ∈ ℝ)
561rexrd 10406 . . . . . . 7 (𝜑𝐵 ∈ ℝ*)
572, 1iccssred 40526 . . . . . . . . 9 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
58 hoidmv1lelem3.u . . . . . . . . . . 11 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))}
59 ssrab2 3912 . . . . . . . . . . 11 {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵)
6058, 59eqsstri 3860 . . . . . . . . . 10 𝑈 ⊆ (𝐴[,]𝐵)
61 hoidmv1lelem3.l . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
62 hoidmv1lelem3.s . . . . . . . . . . . 12 𝑆 = sup(𝑈, ℝ, < )
632, 1, 61, 11, 13, 32, 58, 62hoidmv1lelem1 41599 . . . . . . . . . . 11 (𝜑 → (𝑆𝑈𝐴𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥))
6463simp1d 1178 . . . . . . . . . 10 (𝜑𝑆𝑈)
6560, 64sseldi 3825 . . . . . . . . 9 (𝜑𝑆 ∈ (𝐴[,]𝐵))
6657, 65sseldd 3828 . . . . . . . 8 (𝜑𝑆 ∈ ℝ)
6766rexrd 10406 . . . . . . 7 (𝜑𝑆 ∈ ℝ*)
68 simpl 476 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵𝑆) → 𝜑)
69 simpr 479 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵𝑆) → ¬ 𝐵𝑆)
7068, 66syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵𝑆) → 𝑆 ∈ ℝ)
7168, 1syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵𝑆) → 𝐵 ∈ ℝ)
7270, 71ltnled 10503 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵𝑆) → (𝑆 < 𝐵 ↔ ¬ 𝐵𝑆))
7369, 72mpbird 249 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵𝑆) → 𝑆 < 𝐵)
74 hoidmv1lelem3.x . . . . . . . . . . . . 13 (𝜑 → (𝐴[,)𝐵) ⊆ 𝑗 ∈ ℕ ((𝐶𝑗)[,)(𝐷𝑗)))
7574adantr 474 . . . . . . . . . . . 12 ((𝜑𝑆 < 𝐵) → (𝐴[,)𝐵) ⊆ 𝑗 ∈ ℕ ((𝐶𝑗)[,)(𝐷𝑗)))
762rexrd 10406 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ*)
7776adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑆 < 𝐵) → 𝐴 ∈ ℝ*)
7856adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑆 < 𝐵) → 𝐵 ∈ ℝ*)
7967adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑆 < 𝐵) → 𝑆 ∈ ℝ*)
8060, 57syl5ss 3838 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ⊆ ℝ)
8164ne0d 4151 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ≠ ∅)
8263simp3d 1180 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥)
8363simp2d 1179 . . . . . . . . . . . . . . . 16 (𝜑𝐴𝑈)
84 suprub 11314 . . . . . . . . . . . . . . . 16 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥) ∧ 𝐴𝑈) → 𝐴 ≤ sup(𝑈, ℝ, < ))
8580, 81, 82, 83, 84syl31anc 1498 . . . . . . . . . . . . . . 15 (𝜑𝐴 ≤ sup(𝑈, ℝ, < ))
8685, 62syl6breqr 4915 . . . . . . . . . . . . . 14 (𝜑𝐴𝑆)
8786adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑆 < 𝐵) → 𝐴𝑆)
88 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑆 < 𝐵) → 𝑆 < 𝐵)
8977, 78, 79, 87, 88elicod 12512 . . . . . . . . . . . 12 ((𝜑𝑆 < 𝐵) → 𝑆 ∈ (𝐴[,)𝐵))
9075, 89sseldd 3828 . . . . . . . . . . 11 ((𝜑𝑆 < 𝐵) → 𝑆 𝑗 ∈ ℕ ((𝐶𝑗)[,)(𝐷𝑗)))
91 eliun 4744 . . . . . . . . . . 11 (𝑆 𝑗 ∈ ℕ ((𝐶𝑗)[,)(𝐷𝑗)) ↔ ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗)))
9290, 91sylib 210 . . . . . . . . . 10 ((𝜑𝑆 < 𝐵) → ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗)))
932adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → 𝐴 ∈ ℝ)
94933ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝐴 ∈ ℝ)
951adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → 𝐵 ∈ ℝ)
96953ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝐵 ∈ ℝ)
9711adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → 𝐶:ℕ⟶ℝ)
98973ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝐶:ℕ⟶ℝ)
9913adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → 𝐷:ℕ⟶ℝ)
100993ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝐷:ℕ⟶ℝ)
101 fveq2 6433 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝐶𝑖) = (𝐶𝑗))
102 fveq2 6433 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝐷𝑖) = (𝐷𝑗))
103101, 102oveq12d 6923 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝐶𝑖)[,)(𝐷𝑖)) = ((𝐶𝑗)[,)(𝐷𝑗)))
104103fveq2d 6437 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (vol‘((𝐶𝑖)[,)(𝐷𝑖))) = (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
105104cbvmptv 4973 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)(𝐷𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))
106105fveq2i 6436 . . . . . . . . . . . . . . . 16 ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)(𝐷𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗)))))
107106, 32syl5eqel 2910 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)(𝐷𝑖))))) ∈ ℝ)
108107adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)(𝐷𝑖))))) ∈ ℝ)
1091083ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)(𝐷𝑖))))) ∈ ℝ)
110102breq1d 4883 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑗 → ((𝐷𝑖) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝑧))
111110, 102ifbieq1d 4329 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗 → if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧) = if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))
112101, 111oveq12d 6923 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → ((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))
113112fveq2d 6437 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))
114113cbvmptv 4973 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))
115114eqcomi 2834 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧))))
116115fveq2i 6436 . . . . . . . . . . . . . . . 16 ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧)))))
117116breq2i 4881 . . . . . . . . . . . . . . 15 ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝑧𝐴) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧))))))
118117rabbii 3398 . . . . . . . . . . . . . 14 {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧)))))}
11958, 118eqtri 2849 . . . . . . . . . . . . 13 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶𝑖)[,)if((𝐷𝑖) ≤ 𝑧, (𝐷𝑖), 𝑧)))))}
12064adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑆 < 𝐵) → 𝑆𝑈)
1211203ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑆𝑈)
122873ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝐴𝑆)
123883ad2ant1 1169 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑆 < 𝐵)
124 simp2 1173 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑗 ∈ ℕ)
125 simp3 1174 . . . . . . . . . . . . 13 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗)))
126 eqid 2825 . . . . . . . . . . . . 13 if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵) = if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)
12794, 96, 98, 100, 109, 119, 121, 122, 123, 124, 125, 126hoidmv1lelem2 41600 . . . . . . . . . . . 12 (((𝜑𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗))) → ∃𝑢𝑈 𝑆 < 𝑢)
1281273exp 1154 . . . . . . . . . . 11 ((𝜑𝑆 < 𝐵) → (𝑗 ∈ ℕ → (𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢)))
129128rexlimdv 3239 . . . . . . . . . 10 ((𝜑𝑆 < 𝐵) → (∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶𝑗)[,)(𝐷𝑗)) → ∃𝑢𝑈 𝑆 < 𝑢))
13092, 129mpd 15 . . . . . . . . 9 ((𝜑𝑆 < 𝐵) → ∃𝑢𝑈 𝑆 < 𝑢)
13168, 73, 130syl2anc 581 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵𝑆) → ∃𝑢𝑈 𝑆 < 𝑢)
13257adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴[,]𝐵) ⊆ ℝ)
13360, 132syl5ss 3838 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
13481adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
1352, 1jca 509 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
136135adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
13760a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑈 ⊆ (𝐴[,]𝐵))
13864adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑆𝑈)
139 iccsupr 12555 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝑆𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥))
140136, 137, 138, 139syl3anc 1496 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥))
141140simp3d 1180 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥)
142 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 𝑢𝑈)
143 suprub 11314 . . . . . . . . . . . . . 14 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑈 𝑦𝑥) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
144133, 134, 141, 142, 143syl31anc 1498 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
145144, 62syl6breqr 4915 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → 𝑢𝑆)
146145ralrimiva 3175 . . . . . . . . . . 11 (𝜑 → ∀𝑢𝑈 𝑢𝑆)
14760sseli 3823 . . . . . . . . . . . . . . 15 (𝑢𝑈𝑢 ∈ (𝐴[,]𝐵))
148147adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 𝑢 ∈ (𝐴[,]𝐵))
149132, 148sseldd 3828 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
15066adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → 𝑆 ∈ ℝ)
151149, 150lenltd 10502 . . . . . . . . . . . 12 ((𝜑𝑢𝑈) → (𝑢𝑆 ↔ ¬ 𝑆 < 𝑢))
152151ralbidva 3194 . . . . . . . . . . 11 (𝜑 → (∀𝑢𝑈 𝑢𝑆 ↔ ∀𝑢𝑈 ¬ 𝑆 < 𝑢))
153146, 152mpbid 224 . . . . . . . . . 10 (𝜑 → ∀𝑢𝑈 ¬ 𝑆 < 𝑢)
154 ralnex 3201 . . . . . . . . . 10 (∀𝑢𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃𝑢𝑈 𝑆 < 𝑢)
155153, 154sylib 210 . . . . . . . . 9 (𝜑 → ¬ ∃𝑢𝑈 𝑆 < 𝑢)
156155adantr 474 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵𝑆) → ¬ ∃𝑢𝑈 𝑆 < 𝑢)
157131, 156condan 854 . . . . . . 7 (𝜑𝐵𝑆)
158 iccleub 12517 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑆 ∈ (𝐴[,]𝐵)) → 𝑆𝐵)
15976, 56, 65, 158syl3anc 1496 . . . . . . 7 (𝜑𝑆𝐵)
16056, 67, 157, 159xrletrid 12274 . . . . . 6 (𝜑𝐵 = 𝑆)
161160, 64eqeltrd 2906 . . . . 5 (𝜑𝐵𝑈)
162161, 58syl6eleq 2916 . . . 4 (𝜑𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))})
163 oveq1 6912 . . . . . 6 (𝑧 = 𝐵 → (𝑧𝐴) = (𝐵𝐴))
164 breq2 4877 . . . . . . . . . . 11 (𝑧 = 𝐵 → ((𝐷𝑗) ≤ 𝑧 ↔ (𝐷𝑗) ≤ 𝐵))
165 id 22 . . . . . . . . . . 11 (𝑧 = 𝐵𝑧 = 𝐵)
166164, 165ifbieq2d 4331 . . . . . . . . . 10 (𝑧 = 𝐵 → if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧) = if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))
167166oveq2d 6921 . . . . . . . . 9 (𝑧 = 𝐵 → ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)) = ((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))
168167fveq2d 6437 . . . . . . . 8 (𝑧 = 𝐵 → (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))) = (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))
169168mpteq2dv 4968 . . . . . . 7 (𝑧 = 𝐵 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))))
170169fveq2d 6437 . . . . . 6 (𝑧 = 𝐵 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))))
171163, 170breq12d 4886 . . . . 5 (𝑧 = 𝐵 → ((𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧))))) ↔ (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))))))
172171elrab 3585 . . . 4 (𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝑧, (𝐷𝑗), 𝑧)))))} ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))))))
173162, 172sylib 210 . . 3 (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵)))))))
174173simprd 491 . 2 (𝜑 → (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)if((𝐷𝑗) ≤ 𝐵, (𝐷𝑗), 𝐵))))))
1753, 55, 32, 174, 49letrd 10513 1 (𝜑 → (𝐵𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶𝑗)[,)(𝐷𝑗))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  w3a 1113   = wceq 1658  wcel 2166  wne 2999  wral 3117  wrex 3118  {crab 3121  Vcvv 3414  wss 3798  c0 4144  ifcif 4306   ciun 4740   class class class wbr 4873  cmpt 4952  dom cdm 5342  wf 6119  cfv 6123  (class class class)co 6905  supcsup 8615  cr 10251  0cc0 10252  +∞cpnf 10388  *cxr 10390   < clt 10391  cle 10392  cmin 10585  cn 11350  [,)cico 12465  [,]cicc 12466  volcvol 23629  Σ^csumge0 41370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fi 8586  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-n0 11619  df-z 11705  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-ioo 12467  df-ico 12469  df-icc 12470  df-fz 12620  df-fzo 12761  df-fl 12888  df-seq 13096  df-exp 13155  df-hash 13411  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-clim 14596  df-rlim 14597  df-sum 14794  df-rest 16436  df-topgen 16457  df-psmet 20098  df-xmet 20099  df-met 20100  df-bl 20101  df-mopn 20102  df-top 21069  df-topon 21086  df-bases 21121  df-cmp 21561  df-ovol 23630  df-vol 23631  df-sumge0 41371
This theorem is referenced by:  hoidmv1le  41602
  Copyright terms: Public domain W3C validator