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 45794
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 11639 . 2 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
4 nnex 12215 . . . . . . 7 β„• ∈ V
54a1i 11 . . . . . 6 (πœ‘ β†’ β„• ∈ V)
6 icossicc 13410 . . . . . . . 8 (0[,)+∞) βŠ† (0[,]+∞)
7 0xr 11258 . . . . . . . . . 10 0 ∈ ℝ*
87a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 0 ∈ ℝ*)
9 pnfxr 11265 . . . . . . . . . 10 +∞ ∈ ℝ*
109a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ +∞ ∈ ℝ*)
11 hoidmv1lelem3.c . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢:β„•βŸΆβ„)
1211ffvelcdmda 7076 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—) ∈ ℝ)
13 hoidmv1lelem3.d . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷:β„•βŸΆβ„)
1413ffvelcdmda 7076 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—) ∈ ℝ)
151adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝐡 ∈ ℝ)
1614, 15ifcld 4566 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ∈ ℝ)
17 volicore 45782 . . . . . . . . . . 11 (((πΆβ€˜π‘—) ∈ ℝ ∧ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ∈ ℝ) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ∈ ℝ)
1812, 16, 17syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ∈ ℝ)
1918rexrd 11261 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ∈ ℝ*)
2016rexrd 11261 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ∈ ℝ*)
21 icombl 25415 . . . . . . . . . . 11 (((πΆβ€˜π‘—) ∈ ℝ ∧ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ∈ ℝ*) β†’ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) ∈ dom vol)
2212, 20, 21syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) ∈ dom vol)
23 volge0 45162 . . . . . . . . . 10 (((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) ∈ dom vol β†’ 0 ≀ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))
2422, 23syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))
2518ltpnfd 13098 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) < +∞)
268, 10, 19, 24, 25elicod 13371 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ∈ (0[,)+∞))
276, 26sselid 3972 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ∈ (0[,]+∞))
28 eqid 2724 . . . . . . 7 (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))) = (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))
2927, 28fmptd 7105 . . . . . 6 (πœ‘ β†’ (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))):β„•βŸΆ(0[,]+∞))
305, 29sge0xrcl 45586 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) ∈ ℝ*)
319a1i 11 . . . . 5 (πœ‘ β†’ +∞ ∈ ℝ*)
32 hoidmv1lelem3.r . . . . . . 7 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))) ∈ ℝ)
3332rexrd 11261 . . . . . 6 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))) ∈ ℝ*)
34 nfv 1909 . . . . . . 7 β„²π‘—πœ‘
35 volf 25380 . . . . . . . . 9 vol:dom vol⟢(0[,]+∞)
3635a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ vol:dom vol⟢(0[,]+∞))
3714rexrd 11261 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—) ∈ ℝ*)
38 icombl 25415 . . . . . . . . 9 (((πΆβ€˜π‘—) ∈ ℝ ∧ (π·β€˜π‘—) ∈ ℝ*) β†’ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) ∈ dom vol)
3912, 37, 38syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) ∈ dom vol)
4036, 39ffvelcdmd 7077 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∈ (0[,]+∞))
4112rexrd 11261 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—) ∈ ℝ*)
4212leidd 11777 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—) ≀ (πΆβ€˜π‘—))
43 min1 13165 . . . . . . . . . 10 (((π·β€˜π‘—) ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ≀ (π·β€˜π‘—))
4414, 15, 43syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ≀ (π·β€˜π‘—))
45 icossico 13391 . . . . . . . . 9 ((((πΆβ€˜π‘—) ∈ ℝ* ∧ (π·β€˜π‘—) ∈ ℝ*) ∧ ((πΆβ€˜π‘—) ≀ (πΆβ€˜π‘—) ∧ if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) ≀ (π·β€˜π‘—))) β†’ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) βŠ† ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
4641, 37, 42, 44, 45syl22anc 836 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) βŠ† ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
47 volss 25384 . . . . . . . 8 ((((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) ∈ dom vol ∧ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) ∈ dom vol ∧ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)) βŠ† ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ≀ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))
4822, 39, 46, 47syl3anc 1368 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))) ≀ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))
4934, 5, 27, 40, 48sge0lempt 45611 . . . . . 6 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))))
5032ltpnfd 13098 . . . . . 6 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))) < +∞)
5130, 33, 31, 49, 50xrlelttrd 13136 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) < +∞)
5230, 31, 51xrltned 44552 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) β‰  +∞)
5352neneqd 2937 . . 3 (πœ‘ β†’ Β¬ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) = +∞)
545, 29sge0repnf 45587 . . 3 (πœ‘ β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) ∈ ℝ ↔ Β¬ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) = +∞))
5553, 54mpbird 257 . 2 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))) ∈ ℝ)
561rexrd 11261 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ ℝ*)
572, 1iccssred 13408 . . . . . . . . 9 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
58 hoidmv1lelem3.u . . . . . . . . . . 11 π‘ˆ = {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))))}
59 ssrab2 4069 . . . . . . . . . . 11 {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))))} βŠ† (𝐴[,]𝐡)
6058, 59eqsstri 4008 . . . . . . . . . 10 π‘ˆ βŠ† (𝐴[,]𝐡)
61 hoidmv1lelem3.l . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
62 hoidmv1lelem3.s . . . . . . . . . . . 12 𝑆 = sup(π‘ˆ, ℝ, < )
632, 1, 61, 11, 13, 32, 58, 62hoidmv1lelem1 45792 . . . . . . . . . . 11 (πœ‘ β†’ (𝑆 ∈ π‘ˆ ∧ 𝐴 ∈ π‘ˆ ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯))
6463simp1d 1139 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ π‘ˆ)
6560, 64sselid 3972 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ (𝐴[,]𝐡))
6657, 65sseldd 3975 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ ℝ)
6766rexrd 11261 . . . . . . 7 (πœ‘ β†’ 𝑆 ∈ ℝ*)
68 simpl 482 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ πœ‘)
69 simpr 484 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ Β¬ 𝐡 ≀ 𝑆)
7068, 66syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ 𝑆 ∈ ℝ)
7168, 1syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ 𝐡 ∈ ℝ)
7270, 71ltnled 11358 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ (𝑆 < 𝐡 ↔ Β¬ 𝐡 ≀ 𝑆))
7369, 72mpbird 257 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ 𝑆 < 𝐡)
74 hoidmv1lelem3.x . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴[,)𝐡) βŠ† βˆͺ 𝑗 ∈ β„• ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
7574adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ (𝐴[,)𝐡) βŠ† βˆͺ 𝑗 ∈ β„• ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
762rexrd 11261 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ ℝ*)
7776adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐴 ∈ ℝ*)
7856adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐡 ∈ ℝ*)
7967adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝑆 ∈ ℝ*)
8060, 57sstrid 3985 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘ˆ βŠ† ℝ)
8164ne0d 4327 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘ˆ β‰  βˆ…)
8263simp3d 1141 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯)
8363simp2d 1140 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ π‘ˆ)
84 suprub 12172 . . . . . . . . . . . . . . . 16 (((π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯) ∧ 𝐴 ∈ π‘ˆ) β†’ 𝐴 ≀ sup(π‘ˆ, ℝ, < ))
8580, 81, 82, 83, 84syl31anc 1370 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 ≀ sup(π‘ˆ, ℝ, < ))
8685, 62breqtrrdi 5180 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ≀ 𝑆)
8786adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐴 ≀ 𝑆)
88 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝑆 < 𝐡)
8977, 78, 79, 87, 88elicod 13371 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝑆 ∈ (𝐴[,)𝐡))
9075, 89sseldd 3975 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝑆 ∈ βˆͺ 𝑗 ∈ β„• ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
91 eliun 4991 . . . . . . . . . . 11 (𝑆 ∈ βˆͺ 𝑗 ∈ β„• ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) ↔ βˆƒπ‘— ∈ β„• 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
9290, 91sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ βˆƒπ‘— ∈ β„• 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
932adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐴 ∈ ℝ)
94933ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝐴 ∈ ℝ)
951adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐡 ∈ ℝ)
96953ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝐡 ∈ ℝ)
9711adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐢:β„•βŸΆβ„)
98973ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝐢:β„•βŸΆβ„)
9913adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝐷:β„•βŸΆβ„)
100993ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝐷:β„•βŸΆβ„)
101 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 β†’ (πΆβ€˜π‘–) = (πΆβ€˜π‘—))
102 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 β†’ (π·β€˜π‘–) = (π·β€˜π‘—))
103101, 102oveq12d 7419 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 β†’ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) = ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
104103fveq2d 6885 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 β†’ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) = (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))
105104cbvmptv 5251 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))) = (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))
106105fveq2i 6884 . . . . . . . . . . . . . . . 16 (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))))
107106, 32eqeltrid 2829 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–))))) ∈ ℝ)
108107adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–))))) ∈ ℝ)
1091083ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)(π·β€˜π‘–))))) ∈ ℝ)
110102breq1d 5148 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑗 β†’ ((π·β€˜π‘–) ≀ 𝑧 ↔ (π·β€˜π‘—) ≀ 𝑧))
111110, 102ifbieq1d 4544 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗 β†’ if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧) = if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))
112101, 111oveq12d 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 β†’ ((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧)) = ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))
113112fveq2d 6885 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 β†’ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧))) = (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))
114113cbvmptv 5251 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧)))) = (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))
115114eqcomi 2733 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))) = (𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧))))
116115fveq2i 6884 . . . . . . . . . . . . . . . 16 (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))) = (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧)))))
117116breq2i 5146 . . . . . . . . . . . . . . 15 ((𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))) ↔ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧))))))
118117rabbii 3430 . . . . . . . . . . . . . 14 {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))))} = {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧)))))}
11958, 118eqtri 2752 . . . . . . . . . . . . 13 π‘ˆ = {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑖 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘–)[,)if((π·β€˜π‘–) ≀ 𝑧, (π·β€˜π‘–), 𝑧)))))}
12064adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ 𝑆 ∈ π‘ˆ)
1211203ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑆 ∈ π‘ˆ)
122873ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝐴 ≀ 𝑆)
123883ad2ant1 1130 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑆 < 𝐡)
124 simp2 1134 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑗 ∈ β„•)
125 simp3 1135 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
126 eqid 2724 . . . . . . . . . . . . 13 if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡) = if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)
12794, 96, 98, 100, 109, 119, 121, 122, 123, 124, 125, 126hoidmv1lelem2 45793 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑆 < 𝐡) ∧ 𝑗 ∈ β„• ∧ 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
1281273exp 1116 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ (𝑗 ∈ β„• β†’ (𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)))
129128rexlimdv 3145 . . . . . . . . . 10 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ (βˆƒπ‘— ∈ β„• 𝑆 ∈ ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒))
13092, 129mpd 15 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 < 𝐡) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
13168, 73, 130syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
13257adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
13360, 132sstrid 3985 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ π‘ˆ βŠ† ℝ)
13481adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ π‘ˆ β‰  βˆ…)
1352, 1jca 511 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ))
136135adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ))
13760a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ π‘ˆ βŠ† (𝐴[,]𝐡))
13864adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑆 ∈ π‘ˆ)
139 iccsupr 13416 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ π‘ˆ βŠ† (𝐴[,]𝐡) ∧ 𝑆 ∈ π‘ˆ) β†’ (π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯))
140136, 137, 138, 139syl3anc 1368 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯))
141140simp3d 1141 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯)
142 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ π‘ˆ)
143 suprub 12172 . . . . . . . . . . . . . 14 (((π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ π‘ˆ 𝑦 ≀ π‘₯) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ sup(π‘ˆ, ℝ, < ))
144133, 134, 141, 142, 143syl31anc 1370 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ sup(π‘ˆ, ℝ, < ))
145144, 62breqtrrdi 5180 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ 𝑆)
146145ralrimiva 3138 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘’ ∈ π‘ˆ 𝑒 ≀ 𝑆)
14760sseli 3970 . . . . . . . . . . . . . . 15 (𝑒 ∈ π‘ˆ β†’ 𝑒 ∈ (𝐴[,]𝐡))
148147adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ (𝐴[,]𝐡))
149132, 148sseldd 3975 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ ℝ)
15066adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑆 ∈ ℝ)
151149, 150lenltd 11357 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 ≀ 𝑆 ↔ Β¬ 𝑆 < 𝑒))
152151ralbidva 3167 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ€π‘’ ∈ π‘ˆ 𝑒 ≀ 𝑆 ↔ βˆ€π‘’ ∈ π‘ˆ Β¬ 𝑆 < 𝑒))
153146, 152mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘’ ∈ π‘ˆ Β¬ 𝑆 < 𝑒)
154 ralnex 3064 . . . . . . . . . 10 (βˆ€π‘’ ∈ π‘ˆ Β¬ 𝑆 < 𝑒 ↔ Β¬ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
155153, 154sylib 217 . . . . . . . . 9 (πœ‘ β†’ Β¬ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
156155adantr 480 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐡 ≀ 𝑆) β†’ Β¬ βˆƒπ‘’ ∈ π‘ˆ 𝑆 < 𝑒)
157131, 156condan 815 . . . . . . 7 (πœ‘ β†’ 𝐡 ≀ 𝑆)
158 iccleub 13376 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑆 ∈ (𝐴[,]𝐡)) β†’ 𝑆 ≀ 𝐡)
15976, 56, 65, 158syl3anc 1368 . . . . . . 7 (πœ‘ β†’ 𝑆 ≀ 𝐡)
16056, 67, 157, 159xrletrid 13131 . . . . . 6 (πœ‘ β†’ 𝐡 = 𝑆)
161160, 64eqeltrd 2825 . . . . 5 (πœ‘ β†’ 𝐡 ∈ π‘ˆ)
162161, 58eleqtrdi 2835 . . . 4 (πœ‘ β†’ 𝐡 ∈ {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))))})
163 oveq1 7408 . . . . . 6 (𝑧 = 𝐡 β†’ (𝑧 βˆ’ 𝐴) = (𝐡 βˆ’ 𝐴))
164 breq2 5142 . . . . . . . . . . 11 (𝑧 = 𝐡 β†’ ((π·β€˜π‘—) ≀ 𝑧 ↔ (π·β€˜π‘—) ≀ 𝐡))
165 id 22 . . . . . . . . . . 11 (𝑧 = 𝐡 β†’ 𝑧 = 𝐡)
166164, 165ifbieq2d 4546 . . . . . . . . . 10 (𝑧 = 𝐡 β†’ if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧) = if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))
167166oveq2d 7417 . . . . . . . . 9 (𝑧 = 𝐡 β†’ ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)) = ((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))
168167fveq2d 6885 . . . . . . . 8 (𝑧 = 𝐡 β†’ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))) = (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))
169168mpteq2dv 5240 . . . . . . 7 (𝑧 = 𝐡 β†’ (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))) = (𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))))
170169fveq2d 6885 . . . . . 6 (𝑧 = 𝐡 β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))))
171163, 170breq12d 5151 . . . . 5 (𝑧 = 𝐡 β†’ ((𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧))))) ↔ (𝐡 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))))))
172171elrab 3675 . . . 4 (𝐡 ∈ {𝑧 ∈ (𝐴[,]𝐡) ∣ (𝑧 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝑧, (π·β€˜π‘—), 𝑧)))))} ↔ (𝐡 ∈ (𝐴[,]𝐡) ∧ (𝐡 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))))))
173162, 172sylib 217 . . 3 (πœ‘ β†’ (𝐡 ∈ (𝐴[,]𝐡) ∧ (𝐡 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡)))))))
174173simprd 495 . 2 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)if((π·β€˜π‘—) ≀ 𝐡, (π·β€˜π‘—), 𝐡))))))
1753, 55, 32, 174, 49letrd 11368 1 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (volβ€˜((πΆβ€˜π‘—)[,)(π·β€˜π‘—))))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βŠ† wss 3940  βˆ…c0 4314  ifcif 4520  βˆͺ ciun 4987   class class class wbr 5138   ↦ cmpt 5221  dom cdm 5666  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  supcsup 9431  β„cr 11105  0cc0 11106  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441  β„•cn 12209  [,)cico 13323  [,]cicc 13324  volcvol 25314  Ξ£^csumge0 45563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-rlim 15430  df-sum 15630  df-rest 17367  df-topgen 17388  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-top 22718  df-topon 22735  df-bases 22771  df-cmp 23213  df-ovol 25315  df-vol 25316  df-sumge0 45564
This theorem is referenced by:  hoidmv1le  45795
  Copyright terms: Public domain W3C validator