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 41292
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 ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hoidmvlelem1.x (𝜑𝑋 ∈ Fin)
hoidmvlelem1.y (𝜑𝑌𝑋)
hoidmvlelem1.z (𝜑𝑍 ∈ (𝑋𝑌))
hoidmvlelem1.w 𝑊 = (𝑌 ∪ {𝑍})
hoidmvlelem1.a (𝜑𝐴:𝑊⟶ℝ)
hoidmvlelem1.b (𝜑𝐵:𝑊⟶ℝ)
hoidmvlelem1.c (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
hoidmvlelem1.d (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
hoidmvlelem1.r (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
hoidmvlelem1.h 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ 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 4407 . . . . . . . . . 10 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (𝜑𝑍 ∈ {𝑍})
7 elun2 3987 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
86, 7syl 17 . . . . . . . 8 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
108, 9syl6eleqr 2903 . . . . . . 7 (𝜑𝑍𝑊)
113, 10ffvelrnd 6585 . . . . . 6 (𝜑 → (𝐴𝑍) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (𝜑𝐵:𝑊⟶ℝ)
1312, 10ffvelrnd 6585 . . . . . 6 (𝜑 → (𝐵𝑍) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
15 ssrab2 3891 . . . . . . . 8 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1614, 15eqsstri 3839 . . . . . . 7 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1716a1i 11 . . . . . 6 (𝜑𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)))
1811leidd 10882 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐴𝑍))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (𝜑 → (𝐴𝑍) < (𝐵𝑍))
2011, 13, 19ltled 10473 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐵𝑍))
2111, 13, 11, 18, 20eliccd 40211 . . . . . . . . . 10 (𝜑 → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
2211recnd 10356 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝑍) ∈ ℂ)
2322subidd 10668 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑍) − (𝐴𝑍)) = 0)
2423oveq2d 6893 . . . . . . . . . . . 12 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = (𝐺 · 0))
25 rge0ssre 12503 . . . . . . . . . . . . . . 15 (0[,)+∞) ⊆ ℝ
26 hoidmvlelem1.g . . . . . . . . . . . . . . . 16 𝐺 = ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌))
27 hoidmvlelem1.l . . . . . . . . . . . . . . . . 17 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
28 hoidmvlelem1.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ Fin)
29 hoidmvlelem1.y . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑋)
3028, 29ssfid 8425 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ Fin)
31 ssun1 3982 . . . . . . . . . . . . . . . . . . . 20 𝑌 ⊆ (𝑌 ∪ {𝑍})
3231, 9sseqtr4i 3842 . . . . . . . . . . . . . . . . . . 19 𝑌𝑊
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑊)
343, 33fssresd 6289 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
3512, 33fssresd 6289 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
3627, 30, 34, 35hoidmvcl 41279 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
3726, 36syl5eqel 2896 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ (0[,)+∞))
3825, 37sseldi 3803 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ ℝ)
3938recnd 10356 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℂ)
4039mul01d 10523 . . . . . . . . . . . 12 (𝜑 → (𝐺 · 0) = 0)
4124, 40eqtrd 2847 . . . . . . . . . . 11 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = 0)
42 1red 10329 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
4443rpred 12089 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
4542, 44readdcld 10357 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
46 0red 10331 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
47 0lt1 10838 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
4942, 43ltaddrpd 12122 . . . . . . . . . . . . . 14 (𝜑 → 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 10486 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 + 𝐸))
5146, 45, 50ltled 10473 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 + 𝐸))
52 nnex 11314 . . . . . . . . . . . . . . 15 ℕ ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
54 icossicc 12482 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ (0[,]+∞)
55 snfi 8280 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
57 unfi 8469 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
599, 58syl5eqel 2896 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ Fin)
6059adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
6261ffvelrnda 6584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊))
63 elmapi 8117 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
66 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑗𝑌𝑌))
67 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑐𝑗) = (𝑐))
6867breq1d 4861 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐) ≤ 𝑥))
6968, 67ifbieq1d 4309 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐) ≤ 𝑥, (𝑐), 𝑥))
7066, 67, 69ifbieq12d 4313 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7170cbvmptv 4951 . . . . . . . . . . . . . . . . . . . . 21 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7271mpteq2i 4942 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥))))
7372mpteq2i 4942 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7465, 73eqtri 2835 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7511adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐴𝑍) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
7776ffvelrnda 6584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊))
78 elmapi 8117 . . . . . . . . . . . . . . . . . . 19 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
8074, 75, 60, 79hsphoif 41273 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)):𝑊⟶ℝ)
8127, 60, 64, 80hoidmvcl 41279 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,)+∞))
8254, 81sseldi 3803 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,]+∞))
8382fmpttd 6610 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
8453, 83sge0cl 41078 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞))
8553, 83sge0xrcl 41082 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ*)
86 pnfxr 10380 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . . . 14 (𝜑 → +∞ ∈ ℝ*)
88 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
8988rexrd 10377 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
90 nfv 2005 . . . . . . . . . . . . . . . 16 𝑗𝜑
9127, 60, 64, 79hoidmvcl 41279 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,)+∞))
9254, 91sseldi 3803 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
934eldifbd 3789 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑍𝑌)
9410, 93eldifd 3787 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ (𝑊𝑌))
9594adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
9627, 60, 95, 9, 75, 74, 64, 79hsphoidmvle 41283 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
9790, 53, 82, 92, 96sge0lempt 41107 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
9888ltpnfd 12174 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
9985, 89, 87, 97, 98xrlelttrd 12212 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) < +∞)
10085, 87, 99xrltned 40054 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞)
101 ge0xrre 40239 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10284, 100, 101syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10353, 83sge0ge0 41081 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
104 mulge0 10834 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≤ (1 + 𝐸)) ∧ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))) → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10545, 51, 102, 103, 104syl22anc 858 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10641, 105eqbrtrd 4873 . . . . . . . . . 10 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10721, 106jca 503 . . . . . . . . 9 (𝜑 → ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
108 oveq1 6884 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (𝑧 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
109108oveq2d 6893 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · ((𝐴𝑍) − (𝐴𝑍))))
110 fveq2 6411 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐴𝑍) → (𝐻𝑧) = (𝐻‘(𝐴𝑍)))
111110fveq1d 6413 . . . . . . . . . . . . . . 15 (𝑧 = (𝐴𝑍) → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))
112111oveq2d 6893 . . . . . . . . . . . . . 14 (𝑧 = (𝐴𝑍) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
113112mpteq2dv 4946 . . . . . . . . . . . . 13 (𝑧 = (𝐴𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))
114113fveq2d 6415 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
115114oveq2d 6893 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
116109, 115breq12d 4864 . . . . . . . . . 10 (𝑧 = (𝐴𝑍) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
117116elrab 3566 . . . . . . . . 9 ((𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
118107, 117sylibr 225 . . . . . . . 8 (𝜑 → (𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
119118, 14syl6eleqr 2903 . . . . . . 7 (𝜑 → (𝐴𝑍) ∈ 𝑈)
120 ne0i 4129 . . . . . . 7 ((𝐴𝑍) ∈ 𝑈𝑈 ≠ ∅)
121119, 120syl 17 . . . . . 6 (𝜑𝑈 ≠ ∅)
12211, 13, 17, 121supicc 12546 . . . . 5 (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1232, 122eqeltrd 2892 . . . 4 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1242oveq1d 6892 . . . . . . 7 (𝜑 → (𝑆 − (𝐴𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴𝑍)))
125124oveq2d 6893 . . . . . 6 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))))
12611, 13iccssred 40212 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ)
12717, 126sstrd 3815 . . . . . . . 8 (𝜑𝑈 ⊆ ℝ)
12811, 13jca 503 . . . . . . . . . 10 (𝜑 → ((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ))
129 iccsupr 12488 . . . . . . . . . 10 ((((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐴𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
130128, 17, 119, 129syl3anc 1483 . . . . . . . . 9 (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
131130simp3d 1167 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
132 eqid 2813 . . . . . . . 8 {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} = {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
133127, 121, 131, 11, 132supsubc 40050 . . . . . . 7 (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴𝑍)) = sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < ))
134133oveq2d 6893 . . . . . 6 (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )))
13546rexrd 10377 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
136 icogelb 12446 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐺 ∈ (0[,)+∞)) → 0 ≤ 𝐺)
137135, 87, 37, 136syl3anc 1483 . . . . . . 7 (𝜑 → 0 ≤ 𝐺)
138 vex 3401 . . . . . . . . . . . 12 𝑟 ∈ V
139 eqeq1 2817 . . . . . . . . . . . . 13 (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑟 = (𝑢 − (𝐴𝑍))))
140139rexbidv 3247 . . . . . . . . . . . 12 (𝑤 = 𝑟 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍))))
141138, 140elab 3552 . . . . . . . . . . 11 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
142141biimpi 207 . . . . . . . . . 10 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
143142adantl 469 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
144 nfv 2005 . . . . . . . . . . 11 𝑢𝜑
145 nfcv 2955 . . . . . . . . . . . 12 𝑢𝑟
146 nfre1 3199 . . . . . . . . . . . . 13 𝑢𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))
147146nfab 2960 . . . . . . . . . . . 12 𝑢{𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
148145, 147nfel 2968 . . . . . . . . . . 11 𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
149144, 148nfan 1990 . . . . . . . . . 10 𝑢(𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
150 nfv 2005 . . . . . . . . . 10 𝑢0 ≤ 𝑟
15111rexrd 10377 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑍) ∈ ℝ*)
152151adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ*)
15313rexrd 10377 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑍) ∈ ℝ*)
154153adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ*)
15517sselda 3805 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
156 iccgelb 12451 . . . . . . . . . . . . . . . 16 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑢)
157152, 154, 155, 156syl3anc 1483 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴𝑍) ≤ 𝑢)
158127sselda 3805 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
15911adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ)
160158, 159subge0d 10905 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (0 ≤ (𝑢 − (𝐴𝑍)) ↔ (𝐴𝑍) ≤ 𝑢))
161157, 160mpbird 248 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 0 ≤ (𝑢 − (𝐴𝑍)))
1621613adant3 1155 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ (𝑢 − (𝐴𝑍)))
163 id 22 . . . . . . . . . . . . . . 15 (𝑟 = (𝑢 − (𝐴𝑍)) → 𝑟 = (𝑢 − (𝐴𝑍)))
164163eqcomd 2819 . . . . . . . . . . . . . 14 (𝑟 = (𝑢 − (𝐴𝑍)) → (𝑢 − (𝐴𝑍)) = 𝑟)
1651643ad2ant3 1158 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) = 𝑟)
166162, 165breqtrd 4877 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ 𝑟)
1671663exp 1141 . . . . . . . . . . 11 (𝜑 → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
168167adantr 468 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
169149, 150, 168rexlimd 3221 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟))
170143, 169mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 0 ≤ 𝑟)
171170ralrimiva 3161 . . . . . . 7 (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟)
172 simp3 1161 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 = (𝑢 − (𝐴𝑍)))
173158, 159resubcld 10746 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
1741733adant3 1155 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
175172, 174eqeltrd 2892 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 ∈ ℝ)
1761753exp 1141 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ)))
177176rexlimdv 3225 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
178177alrimiv 2018 . . . . . . . 8 (𝜑 → ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
179 abss 3875 . . . . . . . 8 ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
180178, 179sylibr 225 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ)
18123eqcomd 2819 . . . . . . . . . 10 (𝜑 → 0 = ((𝐴𝑍) − (𝐴𝑍)))
182 oveq1 6884 . . . . . . . . . . 11 (𝑢 = (𝐴𝑍) → (𝑢 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
183182rspceeqv 3527 . . . . . . . . . 10 (((𝐴𝑍) ∈ 𝑈 ∧ 0 = ((𝐴𝑍) − (𝐴𝑍))) → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
184119, 181, 183syl2anc 575 . . . . . . . . 9 (𝜑 → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
185 c0ex 10322 . . . . . . . . . 10 0 ∈ V
186 eqeq1 2817 . . . . . . . . . . 11 (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 0 = (𝑢 − (𝐴𝑍))))
187186rexbidv 3247 . . . . . . . . . 10 (𝑤 = 0 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍))))
188185, 187elab 3552 . . . . . . . . 9 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
189184, 188sylibr 225 . . . . . . . 8 (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
190 ne0i 4129 . . . . . . . 8 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
191189, 190syl 17 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
19213, 11resubcld 10746 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
193 vex 3401 . . . . . . . . . . . . 13 𝑠 ∈ V
194 eqeq1 2817 . . . . . . . . . . . . . 14 (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑠 = (𝑢 − (𝐴𝑍))))
195194rexbidv 3247 . . . . . . . . . . . . 13 (𝑤 = 𝑠 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍))))
196193, 195elab 3552 . . . . . . . . . . . 12 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
197196biimpi 207 . . . . . . . . . . 11 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
198197adantl 469 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
199 nfcv 2955 . . . . . . . . . . . . 13 𝑢𝑠
200199, 147nfel 2968 . . . . . . . . . . . 12 𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
201144, 200nfan 1990 . . . . . . . . . . 11 𝑢(𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
202 nfv 2005 . . . . . . . . . . 11 𝑢 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))
203 simp3 1161 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 = (𝑢 − (𝐴𝑍)))
2041593adant3 1155 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ℝ)
205133ad2ant1 1156 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐵𝑍) ∈ ℝ)
2061553adant3 1155 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
207213ad2ant1 1156 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
208204, 205, 206, 207iccsuble 40227 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
209203, 208eqbrtrd 4873 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
2102093exp 1141 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
211210adantr 468 . . . . . . . . . . 11 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
212201, 202, 211rexlimd 3221 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
213198, 212mpd 15 . . . . . . . . 9 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
214213ralrimiva 3161 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
215 brralrspcev 4911 . . . . . . . 8 ((((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
216192, 214, 215syl2anc 575 . . . . . . 7 (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
217 eqid 2813 . . . . . . . 8 {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
218 biid 252 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)))
219217, 218supmul1 11280 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
22038, 137, 171, 180, 191, 216, 219syl33anc 1497 . . . . . 6 (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
221125, 134, 2203eqtrd 2851 . . . . 5 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
222 vex 3401 . . . . . . . . . . . 12 𝑐 ∈ V
223 eqeq1 2817 . . . . . . . . . . . . 13 (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡)))
224223rexbidv 3247 . . . . . . . . . . . 12 (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡)))
225222, 224elab 3552 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
226225biimpi 207 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
227 nfv 2005 . . . . . . . . . . . 12 𝑡𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))
228 vex 3401 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
229 eqeq1 2817 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑡 = (𝑢 − (𝐴𝑍))))
230229rexbidv 3247 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍))))
231228, 230elab 3552 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
232231biimpi 207 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
233232adantr 468 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
234 simpl 470 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · 𝑡))
235 oveq2 6885 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝑢 − (𝐴𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
236235adantl 469 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
237234, 236eqtrd 2847 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
238237ex 399 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
239238reximdv 3210 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 · 𝑡) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
240239adantl 469 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
241233, 240mpd 15 . . . . . . . . . . . . 13 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
242241ex 399 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
243227, 242rexlimi 3219 . . . . . . . . . . 11 (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
244243a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
245226, 244mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
246245adantl 469 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
247 simp3 1161 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
24838adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 𝐺 ∈ ℝ)
249248, 173remulcld 10358 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ∈ ℝ)
25045adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (1 + 𝐸) ∈ ℝ)
25152a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → ℕ ∈ V)
25260adantlr 697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
25364adantlr 697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
254158adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ)
25579adantlr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
25674, 254, 252, 255hsphoif 41273 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻𝑢)‘(𝐷𝑗)):𝑊⟶ℝ)
25727, 252, 253, 256hoidmvcl 41279 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,)+∞))
25854, 257sseldi 3803 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,]+∞))
259258fmpttd 6610 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
260251, 259sge0cl 41078 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞))
261251, 259sge0xrcl 41082 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ*)
26286a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → +∞ ∈ ℝ*)
26389adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
264 nfv 2005 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑢𝑈)
26592adantlr 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
26695adantlr 697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
26727, 252, 266, 9, 254, 74, 253, 255hsphoidmvle 41283 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
268264, 251, 258, 265, 267sge0lempt 41107 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
26998adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
270261, 263, 262, 268, 269xrlelttrd 12212 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) < +∞)
271261, 262, 270xrltned 40054 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞)
272 ge0xrre 40239 . . . . . . . . . . . . . . . 16 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
273260, 271, 272syl2anc 575 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
274250, 273remulcld 10358 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ∈ ℝ)
275126, 123sseldd 3806 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
27627, 30, 94, 9, 61, 76, 88, 65, 275sge0hsphoire 41286 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
27745, 276remulcld 10358 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
278277adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
27914eleq2i 2884 . . . . . . . . . . . . . . . . . 18 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
280279biimpi 207 . . . . . . . . . . . . . . . . 17 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
281 oveq1 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (𝑧 − (𝐴𝑍)) = (𝑢 − (𝐴𝑍)))
282281oveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑢 − (𝐴𝑍))))
283 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑢 → (𝐻𝑧) = (𝐻𝑢))
284283fveq1d 6413 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑢 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑢)‘(𝐷𝑗)))
285284oveq2d 6893 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑢 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
286285mpteq2dv 4946 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))
287286fveq2d 6415 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))
288287oveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
289282, 288breq12d 4864 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
290289elrab 3566 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
291280, 290sylib 209 . . . . . . . . . . . . . . . 16 (𝑢𝑈 → (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
292291simprd 485 . . . . . . . . . . . . . . 15 (𝑢𝑈 → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
293292adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
294276adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
29551adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 0 ≤ (1 + 𝐸))
296275adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
29774, 296, 60, 79hsphoif 41273 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑆)‘(𝐷𝑗)):𝑊⟶ℝ)
29827, 60, 64, 297hoidmvcl 41279 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,)+∞))
29954, 298sseldi 3803 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
300299adantlr 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
301296adantlr 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
302127adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
303121adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
304131adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
305 simpr 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑢𝑈)
306 suprub 11272 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
307302, 303, 304, 305, 306syl31anc 1485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
308307, 1syl6breqr 4893 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → 𝑢𝑆)
309308adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢𝑆)
31027, 252, 266, 9, 254, 301, 309, 74, 253, 255hsphoidmvle2 41282 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
311264, 251, 258, 300, 310sge0lempt 41107 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
312273, 294, 250, 295, 311lemul2ad 11252 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
313249, 274, 278, 293, 312letrd 10482 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3143133adant3 1155 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
315247, 314eqbrtrd 4873 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3163153exp 1141 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))))
317316rexlimdv 3225 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
318317adantr 468 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
319246, 318mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
320319ralrimiva 3161 . . . . . 6 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
321226adantl 469 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
322 nfv 2005 . . . . . . . . . . . 12 𝑡𝜑
323 nfcv 2955 . . . . . . . . . . . . 13 𝑡𝑐
324 nfre1 3199 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)
325324nfab 2960 . . . . . . . . . . . . 13 𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
326323, 325nfel 2968 . . . . . . . . . . . 12 𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
327322, 326nfan 1990 . . . . . . . . . . 11 𝑡(𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
328 nfv 2005 . . . . . . . . . . 11 𝑡 𝑐 ∈ ℝ
329232adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
330 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡))
3312483adant3 1155 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝐺 ∈ ℝ)
332 simp3 1161 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 = (𝑢 − (𝐴𝑍)))
3331733adant3 1155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
334332, 333eqeltrd 2892 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 ∈ ℝ)
335331, 334remulcld 10358 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) ∈ ℝ)
336335adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ)
337330, 336eqeltrd 2892 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ)
338337ex 399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
3393383exp 1141 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑢𝑈 → (𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))))
340339rexlimdv 3225 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
341340adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
342329, 341mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
343342ex 399 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
344343adantr 468 . . . . . . . . . . 11 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
345327, 328, 344rexlimd 3221 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
346321, 345mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ)
347346ralrimiva 3161 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
348 dfss3 3794 . . . . . . . 8 ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
349347, 348sylibr 225 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ)
35040eqcomd 2819 . . . . . . . . . 10 (𝜑 → 0 = (𝐺 · 0))
351 oveq2 6885 . . . . . . . . . . 11 (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0))
352351rspceeqv 3527 . . . . . . . . . 10 ((0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
353189, 350, 352syl2anc 575 . . . . . . . . 9 (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
354 eqeq1 2817 . . . . . . . . . . 11 (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡)))
355354rexbidv 3247 . . . . . . . . . 10 (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡)))
356185, 355elab 3552 . . . . . . . . 9 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
357353, 356sylibr 225 . . . . . . . 8 (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
358 ne0i 4129 . . . . . . . 8 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
359357, 358syl 17 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
36038, 192remulcld 10358 . . . . . . . 8 (𝜑 → (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ)
361192adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
362137adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 0 ≤ 𝐺)
36313adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ)
364 iccleub 12450 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → 𝑢 ≤ (𝐵𝑍))
365152, 154, 155, 364syl3anc 1483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → 𝑢 ≤ (𝐵𝑍))
366158, 363, 159, 365lesub1dd 10931 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
367173, 361, 248, 362, 366lemul2ad 11252 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3683673adant3 1155 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
369247, 368eqbrtrd 4873 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3703693exp 1141 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))))
371370rexlimdv 3225 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
372371adantr 468 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
373246, 372mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
374373ralrimiva 3161 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
375 brralrspcev 4911 . . . . . . . 8 (((𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
376360, 374, 375syl2anc 575 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
377 suprleub 11277 . . . . . . 7 ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦) ∧ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
378349, 359, 376, 277, 377syl31anc 1485 . . . . . 6 (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
379320, 378mpbird 248 . . . . 5 (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
380221, 379eqbrtrd 4873 . . . 4 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
381123, 380jca 503 . . 3 (𝜑 → (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
382 oveq1 6884 . . . . . 6 (𝑧 = 𝑆 → (𝑧 − (𝐴𝑍)) = (𝑆 − (𝐴𝑍)))
383382oveq2d 6893 . . . . 5 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑆 − (𝐴𝑍))))
384 fveq2 6411 . . . . . . . . . 10 (𝑧 = 𝑆 → (𝐻𝑧) = (𝐻𝑆))
385384fveq1d 6413 . . . . . . . . 9 (𝑧 = 𝑆 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑆)‘(𝐷𝑗)))
386385oveq2d 6893 . . . . . . . 8 (𝑧 = 𝑆 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
387386mpteq2dv 4946 . . . . . . 7 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))
388387fveq2d 6415 . . . . . 6 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
389388oveq2d 6893 . . . . 5 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
390383, 389breq12d 4864 . . . 4 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
391390elrab 3566 . . 3 (𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
392381, 391sylibr 225 . 2 (𝜑𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
393392, 14syl6eleqr 2903 1 (𝜑𝑆𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100  wal 1635   = wceq 1637  wcel 2157  {cab 2799  wne 2985  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  cdif 3773  cun 3774  wss 3776  c0 4123  ifcif 4286  {csn 4377   class class class wbr 4851  cmpt 4930  cres 5320  wf 6100  cfv 6104  (class class class)co 6877  cmpt2 6879  𝑚 cmap 8095  Fincfn 8195  supcsup 8588  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229  +∞cpnf 10359  *cxr 10361   < clt 10362  cle 10363  cmin 10554  cn 11308  +crp 12049  [,)cico 12398  [,]cicc 12399  cprod 14859  volcvol 23450  Σ^csumge0 41059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-map 8097  df-pm 8098  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-fi 8559  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-n0 11563  df-z 11647  df-uz 11908  df-q 12011  df-rp 12050  df-xneg 12165  df-xadd 12166  df-xmul 12167  df-ioo 12400  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-fl 12820  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445  df-rlim 14446  df-sum 14643  df-prod 14860  df-rest 16291  df-topgen 16312  df-psmet 19949  df-xmet 19950  df-met 19951  df-bl 19952  df-mopn 19953  df-top 20916  df-topon 20933  df-bases 20968  df-cmp 21408  df-ovol 23451  df-vol 23452  df-sumge0 41060
This theorem is referenced by:  hoidmvlelem4  41295
  Copyright terms: Public domain W3C validator