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

Theorem hoidmvlelem1 44478
Description: The supremum of 𝑈 belongs to 𝑈. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvlelem1.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hoidmvlelem1.x (𝜑𝑋 ∈ Fin)
hoidmvlelem1.y (𝜑𝑌𝑋)
hoidmvlelem1.z (𝜑𝑍 ∈ (𝑋𝑌))
hoidmvlelem1.w 𝑊 = (𝑌 ∪ {𝑍})
hoidmvlelem1.a (𝜑𝐴:𝑊⟶ℝ)
hoidmvlelem1.b (𝜑𝐵:𝑊⟶ℝ)
hoidmvlelem1.c (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑊))
hoidmvlelem1.d (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑊))
hoidmvlelem1.r (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
hoidmvlelem1.h 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
hoidmvlelem1.g 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
hoidmvlelem1.e (𝜑𝐸 ∈ ℝ+)
hoidmvlelem1.u 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
hoidmvlelem1.s 𝑆 = sup(𝑈, ℝ, < )
hoidmvlelem1.ab (𝜑 → (𝐴𝑍) < (𝐵𝑍))
Assertion
Ref Expression
hoidmvlelem1 (𝜑𝑆𝑈)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑗,𝑘,𝑥   𝐴,𝑐,𝑗,𝑘,𝑥   𝑧,𝐴,𝑗   𝐵,𝑎,𝑏,𝑘   𝐵,𝑐   𝑧,𝐵   𝐶,𝑎,𝑏,𝑘   𝐶,𝑐   𝑧,𝐶   𝐷,𝑎,𝑏,𝑘   𝐷,𝑐   𝑧,𝐷   𝐸,𝑐   𝑧,𝐸   𝐺,𝑐   𝑧,𝐺   𝐻,𝑎,𝑏,𝑘   𝐻,𝑐   𝑧,𝐻   𝐿,𝑐   𝑧,𝐿   𝑆,𝑎,𝑏,𝑗,𝑘,𝑥   𝑆,𝑐   𝑧,𝑆   𝑈,𝑎,𝑏,𝑗,𝑘,𝑥   𝑈,𝑐   𝑧,𝑈   𝑊,𝑎,𝑏,𝑗,𝑘,𝑥   𝑊,𝑐   𝑧,𝑊   𝑌,𝑎,𝑏,𝑗,𝑘,𝑥   𝑌,𝑐   𝑍,𝑎,𝑏,𝑗,𝑘,𝑥   𝑍,𝑐   𝑧,𝑍   𝜑,𝑎,𝑏,𝑗,𝑘,𝑥   𝜑,𝑐
Allowed substitution hints:   𝜑(𝑧)   𝐵(𝑥,𝑗)   𝐶(𝑥,𝑗)   𝐷(𝑥,𝑗)   𝐸(𝑥,𝑗,𝑘,𝑎,𝑏)   𝐺(𝑥,𝑗,𝑘,𝑎,𝑏)   𝐻(𝑥,𝑗)   𝐿(𝑥,𝑗,𝑘,𝑎,𝑏)   𝑋(𝑥,𝑧,𝑗,𝑘,𝑎,𝑏,𝑐)   𝑌(𝑧)

Proof of Theorem hoidmvlelem1
Dummy variables 𝑢 𝑟 𝑠 𝑡 𝑣 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmvlelem1.s . . . . . 6 𝑆 = sup(𝑈, ℝ, < )
21a1i 11 . . . . 5 (𝜑𝑆 = sup(𝑈, ℝ, < ))
3 hoidmvlelem1.a . . . . . . 7 (𝜑𝐴:𝑊⟶ℝ)
4 hoidmvlelem1.z . . . . . . . . . 10 (𝜑𝑍 ∈ (𝑋𝑌))
5 snidg 4607 . . . . . . . . . 10 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (𝜑𝑍 ∈ {𝑍})
7 elun2 4124 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
86, 7syl 17 . . . . . . . 8 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
108, 9eleqtrrdi 2848 . . . . . . 7 (𝜑𝑍𝑊)
113, 10ffvelcdmd 7018 . . . . . 6 (𝜑 → (𝐴𝑍) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (𝜑𝐵:𝑊⟶ℝ)
1312, 10ffvelcdmd 7018 . . . . . 6 (𝜑 → (𝐵𝑍) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
15 ssrab2 4025 . . . . . . . 8 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1614, 15eqsstri 3966 . . . . . . 7 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1716a1i 11 . . . . . 6 (𝜑𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)))
1811leidd 11642 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐴𝑍))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (𝜑 → (𝐴𝑍) < (𝐵𝑍))
2011, 13, 19ltled 11224 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐵𝑍))
2111, 13, 11, 18, 20eliccd 43386 . . . . . . . . . 10 (𝜑 → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
2211recnd 11104 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝑍) ∈ ℂ)
2322subidd 11421 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑍) − (𝐴𝑍)) = 0)
2423oveq2d 7353 . . . . . . . . . . . 12 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = (𝐺 · 0))
25 rge0ssre 13289 . . . . . . . . . . . . . . 15 (0[,)+∞) ⊆ ℝ
26 hoidmvlelem1.g . . . . . . . . . . . . . . . 16 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
27 hoidmvlelem1.l . . . . . . . . . . . . . . . . 17 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
28 hoidmvlelem1.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ Fin)
29 hoidmvlelem1.y . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑋)
3028, 29ssfid 9132 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ Fin)
31 ssun1 4119 . . . . . . . . . . . . . . . . . . . 20 𝑌 ⊆ (𝑌 ∪ {𝑍})
3231, 9sseqtrri 3969 . . . . . . . . . . . . . . . . . . 19 𝑌𝑊
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑊)
343, 33fssresd 6692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
3512, 33fssresd 6692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
3627, 30, 34, 35hoidmvcl 44465 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
3726, 36eqeltrid 2841 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ (0[,)+∞))
3825, 37sselid 3930 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ ℝ)
3938recnd 11104 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℂ)
4039mul01d 11275 . . . . . . . . . . . 12 (𝜑 → (𝐺 · 0) = 0)
4124, 40eqtrd 2776 . . . . . . . . . . 11 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = 0)
42 1red 11077 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
4443rpred 12873 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
4542, 44readdcld 11105 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
46 0red 11079 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
47 0lt1 11598 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
4942, 43ltaddrpd 12906 . . . . . . . . . . . . . 14 (𝜑 → 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 11237 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 + 𝐸))
5146, 45, 50ltled 11224 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 + 𝐸))
52 nnex 12080 . . . . . . . . . . . . . . 15 ℕ ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
54 icossicc 13269 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ (0[,]+∞)
55 snfi 8909 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
57 unfi 9037 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
599, 58eqeltrid 2841 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ Fin)
6059adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑊))
6261ffvelcdmda 7017 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑m 𝑊))
63 elmapi 8708 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑗) ∈ (ℝ ↑m 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
66 eleq1w 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑗𝑌𝑌))
67 fveq2 6825 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑐𝑗) = (𝑐))
6867breq1d 5102 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐) ≤ 𝑥))
6968, 67ifbieq1d 4497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐) ≤ 𝑥, (𝑐), 𝑥))
7066, 67, 69ifbieq12d 4501 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7170cbvmptv 5205 . . . . . . . . . . . . . . . . . . . . 21 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7271mpteq2i 5197 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥))))
7372mpteq2i 5197 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7465, 73eqtri 2764 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7511adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐴𝑍) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑊))
7776ffvelcdmda 7017 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑m 𝑊))
78 elmapi 8708 . . . . . . . . . . . . . . . . . . 19 ((𝐷𝑗) ∈ (ℝ ↑m 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
8074, 75, 60, 79hsphoif 44459 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)):𝑊⟶ℝ)
8127, 60, 64, 80hoidmvcl 44465 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,)+∞))
8254, 81sselid 3930 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,]+∞))
8382fmpttd 7045 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
8453, 83sge0cl 44264 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞))
8553, 83sge0xrcl 44268 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ*)
86 pnfxr 11130 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . . . 14 (𝜑 → +∞ ∈ ℝ*)
88 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
8988rexrd 11126 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
90 nfv 1916 . . . . . . . . . . . . . . . 16 𝑗𝜑
9127, 60, 64, 79hoidmvcl 44465 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,)+∞))
9254, 91sselid 3930 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
934eldifbd 3911 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑍𝑌)
9410, 93eldifd 3909 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ (𝑊𝑌))
9594adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
9627, 60, 95, 9, 75, 74, 64, 79hsphoidmvle 44469 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
9790, 53, 82, 92, 96sge0lempt 44293 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
9888ltpnfd 12958 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
9985, 89, 87, 97, 98xrlelttrd 12995 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) < +∞)
10085, 87, 99xrltned 43239 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞)
101 ge0xrre 43413 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10284, 100, 101syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10353, 83sge0ge0 44267 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
104 mulge0 11594 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≤ (1 + 𝐸)) ∧ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))) → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10545, 51, 102, 103, 104syl22anc 836 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10641, 105eqbrtrd 5114 . . . . . . . . . 10 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10721, 106jca 512 . . . . . . . . 9 (𝜑 → ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
108 oveq1 7344 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (𝑧 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
109108oveq2d 7353 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · ((𝐴𝑍) − (𝐴𝑍))))
110 fveq2 6825 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐴𝑍) → (𝐻𝑧) = (𝐻‘(𝐴𝑍)))
111110fveq1d 6827 . . . . . . . . . . . . . . 15 (𝑧 = (𝐴𝑍) → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))
112111oveq2d 7353 . . . . . . . . . . . . . 14 (𝑧 = (𝐴𝑍) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
113112mpteq2dv 5194 . . . . . . . . . . . . 13 (𝑧 = (𝐴𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))
114113fveq2d 6829 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
115114oveq2d 7353 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
116109, 115breq12d 5105 . . . . . . . . . 10 (𝑧 = (𝐴𝑍) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
117116elrab 3634 . . . . . . . . 9 ((𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
118107, 117sylibr 233 . . . . . . . 8 (𝜑 → (𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
119118, 14eleqtrrdi 2848 . . . . . . 7 (𝜑 → (𝐴𝑍) ∈ 𝑈)
120 ne0i 4281 . . . . . . 7 ((𝐴𝑍) ∈ 𝑈𝑈 ≠ ∅)
121119, 120syl 17 . . . . . 6 (𝜑𝑈 ≠ ∅)
12211, 13, 17, 121supicc 13334 . . . . 5 (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1232, 122eqeltrd 2837 . . . 4 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1242oveq1d 7352 . . . . . . 7 (𝜑 → (𝑆 − (𝐴𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴𝑍)))
125124oveq2d 7353 . . . . . 6 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))))
12611, 13iccssred 13267 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ)
12717, 126sstrd 3942 . . . . . . . 8 (𝜑𝑈 ⊆ ℝ)
12811, 13jca 512 . . . . . . . . . 10 (𝜑 → ((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ))
129 iccsupr 13275 . . . . . . . . . 10 ((((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐴𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
130128, 17, 119, 129syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
131130simp3d 1143 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
132 eqid 2736 . . . . . . . 8 {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} = {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
133127, 121, 131, 11, 132supsubc 43235 . . . . . . 7 (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴𝑍)) = sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < ))
134133oveq2d 7353 . . . . . 6 (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )))
13546rexrd 11126 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
136 icogelb 13231 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐺 ∈ (0[,)+∞)) → 0 ≤ 𝐺)
137135, 87, 37, 136syl3anc 1370 . . . . . . 7 (𝜑 → 0 ≤ 𝐺)
138 vex 3445 . . . . . . . . . . . 12 𝑟 ∈ V
139 eqeq1 2740 . . . . . . . . . . . . 13 (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑟 = (𝑢 − (𝐴𝑍))))
140139rexbidv 3171 . . . . . . . . . . . 12 (𝑤 = 𝑟 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍))))
141138, 140elab 3619 . . . . . . . . . . 11 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
142141biimpi 215 . . . . . . . . . 10 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
143142adantl 482 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
144 nfv 1916 . . . . . . . . . . 11 𝑢𝜑
145 nfcv 2904 . . . . . . . . . . . 12 𝑢𝑟
146 nfre1 3264 . . . . . . . . . . . . 13 𝑢𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))
147146nfab 2910 . . . . . . . . . . . 12 𝑢{𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
148145, 147nfel 2918 . . . . . . . . . . 11 𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
149144, 148nfan 1901 . . . . . . . . . 10 𝑢(𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
150 nfv 1916 . . . . . . . . . 10 𝑢0 ≤ 𝑟
15111rexrd 11126 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑍) ∈ ℝ*)
152151adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ*)
15313rexrd 11126 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑍) ∈ ℝ*)
154153adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ*)
15517sselda 3932 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
156 iccgelb 13236 . . . . . . . . . . . . . . . 16 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑢)
157152, 154, 155, 156syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴𝑍) ≤ 𝑢)
158127sselda 3932 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
15911adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ)
160158, 159subge0d 11666 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (0 ≤ (𝑢 − (𝐴𝑍)) ↔ (𝐴𝑍) ≤ 𝑢))
161157, 160mpbird 256 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 0 ≤ (𝑢 − (𝐴𝑍)))
1621613adant3 1131 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ (𝑢 − (𝐴𝑍)))
163 id 22 . . . . . . . . . . . . . . 15 (𝑟 = (𝑢 − (𝐴𝑍)) → 𝑟 = (𝑢 − (𝐴𝑍)))
164163eqcomd 2742 . . . . . . . . . . . . . 14 (𝑟 = (𝑢 − (𝐴𝑍)) → (𝑢 − (𝐴𝑍)) = 𝑟)
1651643ad2ant3 1134 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) = 𝑟)
166162, 165breqtrd 5118 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ 𝑟)
1671663exp 1118 . . . . . . . . . . 11 (𝜑 → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
168167adantr 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
169149, 150, 168rexlimd 3245 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟))
170143, 169mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 0 ≤ 𝑟)
171170ralrimiva 3139 . . . . . . 7 (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟)
172 simp3 1137 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 = (𝑢 − (𝐴𝑍)))
173158, 159resubcld 11504 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
1741733adant3 1131 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
175172, 174eqeltrd 2837 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 ∈ ℝ)
1761753exp 1118 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ)))
177176rexlimdv 3146 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
178177alrimiv 1929 . . . . . . . 8 (𝜑 → ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
179 abss 4005 . . . . . . . 8 ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
180178, 179sylibr 233 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ)
18123eqcomd 2742 . . . . . . . . . 10 (𝜑 → 0 = ((𝐴𝑍) − (𝐴𝑍)))
182 oveq1 7344 . . . . . . . . . . 11 (𝑢 = (𝐴𝑍) → (𝑢 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
183182rspceeqv 3584 . . . . . . . . . 10 (((𝐴𝑍) ∈ 𝑈 ∧ 0 = ((𝐴𝑍) − (𝐴𝑍))) → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
184119, 181, 183syl2anc 584 . . . . . . . . 9 (𝜑 → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
185 eqeq1 2740 . . . . . . . . . 10 (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 0 = (𝑢 − (𝐴𝑍))))
186185rexbidv 3171 . . . . . . . . 9 (𝑤 = 0 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍))))
18746, 184, 186elabd 3622 . . . . . . . 8 (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
188 ne0i 4281 . . . . . . . 8 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
189187, 188syl 17 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
19013, 11resubcld 11504 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
191 vex 3445 . . . . . . . . . . . . 13 𝑠 ∈ V
192 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑠 = (𝑢 − (𝐴𝑍))))
193192rexbidv 3171 . . . . . . . . . . . . 13 (𝑤 = 𝑠 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍))))
194191, 193elab 3619 . . . . . . . . . . . 12 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
195194biimpi 215 . . . . . . . . . . 11 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
196195adantl 482 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
197 nfcv 2904 . . . . . . . . . . . . 13 𝑢𝑠
198197, 147nfel 2918 . . . . . . . . . . . 12 𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
199144, 198nfan 1901 . . . . . . . . . . 11 𝑢(𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
200 nfv 1916 . . . . . . . . . . 11 𝑢 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))
201 simp3 1137 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 = (𝑢 − (𝐴𝑍)))
2021593adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ℝ)
203133ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐵𝑍) ∈ ℝ)
2041553adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
205213ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
206202, 203, 204, 205iccsuble 43401 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
207201, 206eqbrtrd 5114 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
2082073exp 1118 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
209208adantr 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
210199, 200, 209rexlimd 3245 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
211196, 210mpd 15 . . . . . . . . 9 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
212211ralrimiva 3139 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
213 brralrspcev 5152 . . . . . . . 8 ((((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
214190, 212, 213syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
215 eqid 2736 . . . . . . . 8 {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
216 biid 260 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)))
217215, 216supmul1 12045 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
21838, 137, 171, 180, 189, 214, 217syl33anc 1384 . . . . . 6 (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
219125, 134, 2183eqtrd 2780 . . . . 5 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
220 vex 3445 . . . . . . . . . . . 12 𝑐 ∈ V
221 eqeq1 2740 . . . . . . . . . . . . 13 (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡)))
222221rexbidv 3171 . . . . . . . . . . . 12 (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡)))
223220, 222elab 3619 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
224223biimpi 215 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
225 nfv 1916 . . . . . . . . . . . 12 𝑡𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))
226 vex 3445 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
227 eqeq1 2740 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑡 = (𝑢 − (𝐴𝑍))))
228227rexbidv 3171 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍))))
229226, 228elab 3619 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
230229biimpi 215 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
231230adantr 481 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
232 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · 𝑡))
233 oveq2 7345 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝑢 − (𝐴𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
234233adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
235232, 234eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
236235ex 413 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
237236reximdv 3163 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 · 𝑡) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
238237adantl 482 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
239231, 238mpd 15 . . . . . . . . . . . . 13 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
240239ex 413 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
241225, 240rexlimi 3238 . . . . . . . . . . 11 (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
242241a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
243224, 242mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
244243adantl 482 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
245 simp3 1137 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
24638adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 𝐺 ∈ ℝ)
247246, 173remulcld 11106 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ∈ ℝ)
24845adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (1 + 𝐸) ∈ ℝ)
24952a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → ℕ ∈ V)
25060adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
25164adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
252158adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ)
25379adantlr 712 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
25474, 252, 250, 253hsphoif 44459 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻𝑢)‘(𝐷𝑗)):𝑊⟶ℝ)
25527, 250, 251, 254hoidmvcl 44465 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,)+∞))
25654, 255sselid 3930 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,]+∞))
257256fmpttd 7045 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
258249, 257sge0cl 44264 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞))
259249, 257sge0xrcl 44268 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ*)
26086a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → +∞ ∈ ℝ*)
26189adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
262 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑢𝑈)
26392adantlr 712 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
26495adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
26527, 250, 264, 9, 252, 74, 251, 253hsphoidmvle 44469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
266262, 249, 256, 263, 265sge0lempt 44293 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
26798adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
268259, 261, 260, 266, 267xrlelttrd 12995 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) < +∞)
269259, 260, 268xrltned 43239 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞)
270 ge0xrre 43413 . . . . . . . . . . . . . . . 16 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
271258, 269, 270syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
272248, 271remulcld 11106 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ∈ ℝ)
273126, 123sseldd 3933 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
27427, 30, 94, 9, 61, 76, 88, 65, 273sge0hsphoire 44472 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
27545, 274remulcld 11106 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
276275adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
27714eleq2i 2828 . . . . . . . . . . . . . . . . . 18 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
278277biimpi 215 . . . . . . . . . . . . . . . . 17 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
279 oveq1 7344 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (𝑧 − (𝐴𝑍)) = (𝑢 − (𝐴𝑍)))
280279oveq2d 7353 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑢 − (𝐴𝑍))))
281 fveq2 6825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑢 → (𝐻𝑧) = (𝐻𝑢))
282281fveq1d 6827 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑢 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑢)‘(𝐷𝑗)))
283282oveq2d 7353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑢 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
284283mpteq2dv 5194 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))
285284fveq2d 6829 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))
286285oveq2d 7353 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
287280, 286breq12d 5105 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
288287elrab 3634 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
289278, 288sylib 217 . . . . . . . . . . . . . . . 16 (𝑢𝑈 → (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
290289simprd 496 . . . . . . . . . . . . . . 15 (𝑢𝑈 → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
291290adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
292274adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
29351adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 0 ≤ (1 + 𝐸))
294273adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
29574, 294, 60, 79hsphoif 44459 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑆)‘(𝐷𝑗)):𝑊⟶ℝ)
29627, 60, 64, 295hoidmvcl 44465 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,)+∞))
29754, 296sselid 3930 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
298297adantlr 712 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
299294adantlr 712 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
300127adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
301121adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
302131adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
303 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑢𝑈)
304 suprub 12037 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
305300, 301, 302, 303, 304syl31anc 1372 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
306305, 1breqtrrdi 5134 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → 𝑢𝑆)
307306adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢𝑆)
30827, 250, 264, 9, 252, 299, 307, 74, 251, 253hsphoidmvle2 44468 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
309262, 249, 256, 298, 308sge0lempt 44293 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
310271, 292, 248, 293, 309lemul2ad 12016 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
311247, 272, 276, 291, 310letrd 11233 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3123113adant3 1131 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
313245, 312eqbrtrd 5114 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3143133exp 1118 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))))
315314rexlimdv 3146 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
316315adantr 481 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
317244, 316mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
318317ralrimiva 3139 . . . . . 6 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
319224adantl 482 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
320 nfv 1916 . . . . . . . . . . . 12 𝑡𝜑
321 nfcv 2904 . . . . . . . . . . . . 13 𝑡𝑐
322 nfre1 3264 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)
323322nfab 2910 . . . . . . . . . . . . 13 𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
324321, 323nfel 2918 . . . . . . . . . . . 12 𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
325320, 324nfan 1901 . . . . . . . . . . 11 𝑡(𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
326 nfv 1916 . . . . . . . . . . 11 𝑡 𝑐 ∈ ℝ
327230adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
328 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡))
3292463adant3 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝐺 ∈ ℝ)
330 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 = (𝑢 − (𝐴𝑍)))
3311733adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
332330, 331eqeltrd 2837 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 ∈ ℝ)
333329, 332remulcld 11106 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) ∈ ℝ)
334333adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ)
335328, 334eqeltrd 2837 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ)
336335ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
3373363exp 1118 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑢𝑈 → (𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))))
338337rexlimdv 3146 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
339338adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
340327, 339mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
341340ex 413 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
342341adantr 481 . . . . . . . . . . 11 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
343325, 326, 342rexlimd 3245 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
344319, 343mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ)
345344ralrimiva 3139 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
346 dfss3 3920 . . . . . . . 8 ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
347345, 346sylibr 233 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ)
34840eqcomd 2742 . . . . . . . . . 10 (𝜑 → 0 = (𝐺 · 0))
349 oveq2 7345 . . . . . . . . . . 11 (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0))
350349rspceeqv 3584 . . . . . . . . . 10 ((0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
351187, 348, 350syl2anc 584 . . . . . . . . 9 (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
352 eqeq1 2740 . . . . . . . . . 10 (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡)))
353352rexbidv 3171 . . . . . . . . 9 (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡)))
35446, 351, 353elabd 3622 . . . . . . . 8 (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
355 ne0i 4281 . . . . . . . 8 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
356354, 355syl 17 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
35738, 190remulcld 11106 . . . . . . . 8 (𝜑 → (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ)
358190adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
359137adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 0 ≤ 𝐺)
36013adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ)
361 iccleub 13235 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → 𝑢 ≤ (𝐵𝑍))
362152, 154, 155, 361syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → 𝑢 ≤ (𝐵𝑍))
363158, 360, 159, 362lesub1dd 11692 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
364173, 358, 246, 359, 363lemul2ad 12016 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3653643adant3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
366245, 365eqbrtrd 5114 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3673663exp 1118 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))))
368367rexlimdv 3146 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
369368adantr 481 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
370244, 369mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
371370ralrimiva 3139 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
372 brralrspcev 5152 . . . . . . . 8 (((𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
373357, 371, 372syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
374 suprleub 12042 . . . . . . 7 ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦) ∧ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
375347, 356, 373, 275, 374syl31anc 1372 . . . . . 6 (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
376318, 375mpbird 256 . . . . 5 (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
377219, 376eqbrtrd 5114 . . . 4 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
378123, 377jca 512 . . 3 (𝜑 → (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
379 oveq1 7344 . . . . . 6 (𝑧 = 𝑆 → (𝑧 − (𝐴𝑍)) = (𝑆 − (𝐴𝑍)))
380379oveq2d 7353 . . . . 5 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑆 − (𝐴𝑍))))
381 fveq2 6825 . . . . . . . . . 10 (𝑧 = 𝑆 → (𝐻𝑧) = (𝐻𝑆))
382381fveq1d 6827 . . . . . . . . 9 (𝑧 = 𝑆 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑆)‘(𝐷𝑗)))
383382oveq2d 7353 . . . . . . . 8 (𝑧 = 𝑆 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
384383mpteq2dv 5194 . . . . . . 7 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))
385384fveq2d 6829 . . . . . 6 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
386385oveq2d 7353 . . . . 5 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
387380, 386breq12d 5105 . . . 4 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
388387elrab 3634 . . 3 (𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
389378, 388sylibr 233 . 2 (𝜑𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
390389, 14eleqtrrdi 2848 1 (𝜑𝑆𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086  wal 1538   = wceq 1540  wcel 2105  {cab 2713  wne 2940  wral 3061  wrex 3070  {crab 3403  Vcvv 3441  cdif 3895  cun 3896  wss 3898  c0 4269  ifcif 4473  {csn 4573   class class class wbr 5092  cmpt 5175  cres 5622  wf 6475  cfv 6479  (class class class)co 7337  cmpo 7339  m cmap 8686  Fincfn 8804  supcsup 9297  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977  +∞cpnf 11107  *cxr 11109   < clt 11110  cle 11111  cmin 11306  cn 12074  +crp 12831  [,)cico 13182  [,]cicc 13183  cprod 15714  volcvol 24733  Σ^csumge0 44245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-dju 9758  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-rlim 15297  df-sum 15497  df-prod 15715  df-rest 17230  df-topgen 17251  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-top 22149  df-topon 22166  df-bases 22202  df-cmp 22644  df-ovol 24734  df-vol 24735  df-sumge0 44246
This theorem is referenced by:  hoidmvlelem4  44481
  Copyright terms: Public domain W3C validator