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 39309
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 4152 . . . . . . . . . 10 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (𝜑𝑍 ∈ {𝑍})
7 elun2 3742 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
86, 7syl 17 . . . . . . . 8 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
108, 9syl6eleqr 2698 . . . . . . 7 (𝜑𝑍𝑊)
113, 10ffvelrnd 6253 . . . . . 6 (𝜑 → (𝐴𝑍) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (𝜑𝐵:𝑊⟶ℝ)
1312, 10ffvelrnd 6253 . . . . . 6 (𝜑 → (𝐵𝑍) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
15 ssrab2 3649 . . . . . . . 8 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1614, 15eqsstri 3597 . . . . . . 7 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1716a1i 11 . . . . . 6 (𝜑𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)))
1811leidd 10446 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐴𝑍))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (𝜑 → (𝐴𝑍) < (𝐵𝑍))
2011, 13, 19ltled 10037 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐵𝑍))
2111, 13, 11, 18, 20eliccd 38397 . . . . . . . . . 10 (𝜑 → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
2211recnd 9925 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝑍) ∈ ℂ)
2322subidd 10232 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑍) − (𝐴𝑍)) = 0)
2423oveq2d 6543 . . . . . . . . . . . 12 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = (𝐺 · 0))
25 rge0ssre 12110 . . . . . . . . . . . . . . 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 8046 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ Fin)
31 ssun1 3737 . . . . . . . . . . . . . . . . . . . 20 𝑌 ⊆ (𝑌 ∪ {𝑍})
3231, 9sseqtr4i 3600 . . . . . . . . . . . . . . . . . . 19 𝑌𝑊
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑊)
343, 33fssresd 5969 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
3512, 33fssresd 5969 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
3627, 30, 34, 35hoidmvcl 39296 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
3726, 36syl5eqel 2691 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ (0[,)+∞))
3825, 37sseldi 3565 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ ℝ)
3938recnd 9925 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℂ)
4039mul01d 10087 . . . . . . . . . . . 12 (𝜑 → (𝐺 · 0) = 0)
4124, 40eqtrd 2643 . . . . . . . . . . 11 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = 0)
42 1red 9912 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
4443rpred 11707 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
4542, 44readdcld 9926 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
46 0red 9898 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
47 0lt1 10402 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
4942, 43ltaddrpd 11740 . . . . . . . . . . . . . 14 (𝜑 → 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 10050 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 + 𝐸))
5146, 45, 50ltled 10037 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 + 𝐸))
52 nnex 10876 . . . . . . . . . . . . . . 15 ℕ ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
54 icossicc 12090 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ (0[,]+∞)
55 snfi 7901 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
57 unfi 8090 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 690 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
599, 58syl5eqel 2691 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ Fin)
6059adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
6261ffvelrnda 6252 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊))
63 elmapi 7743 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
66 eleq1 2675 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑗𝑌𝑌))
67 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑐𝑗) = (𝑐))
6867breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐) ≤ 𝑥))
6968, 67ifbieq1d 4058 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐) ≤ 𝑥, (𝑐), 𝑥))
7066, 67, 69ifbieq12d 4062 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7170cbvmptv 4672 . . . . . . . . . . . . . . . . . . . . 21 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7271mpteq2i 4663 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥))))
7372mpteq2i 4663 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7465, 73eqtri 2631 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7511adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐴𝑍) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
7776ffvelrnda 6252 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊))
78 elmapi 7743 . . . . . . . . . . . . . . . . . . 19 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
8074, 75, 60, 79hsphoif 39290 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)):𝑊⟶ℝ)
8127, 60, 64, 80hoidmvcl 39296 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,)+∞))
8254, 81sseldi 3565 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,]+∞))
83 eqid 2609 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
8482, 83fmptd 6277 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
8553, 84sge0cl 39098 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞))
8653, 84sge0xrcl 39102 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ*)
87 pnfxr 11784 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8887a1i 11 . . . . . . . . . . . . . 14 (𝜑 → +∞ ∈ ℝ*)
89 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
9089rexrd 9946 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
91 nfv 1829 . . . . . . . . . . . . . . . 16 𝑗𝜑
9227, 60, 64, 79hoidmvcl 39296 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,)+∞))
9354, 92sseldi 3565 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
944eldifbd 3552 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑍𝑌)
9510, 94eldifd 3550 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ (𝑊𝑌))
9695adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
9727, 60, 96, 9, 75, 74, 64, 79hsphoidmvle 39300 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
9891, 53, 82, 93, 97sge0lempt 39127 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
9989ltpnfd 11795 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
10086, 90, 88, 98, 99xrlelttrd 11829 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) < +∞)
10186, 88, 100xrltned 38338 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞)
102 ge0xrre 38429 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10385, 101, 102syl2anc 690 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10453, 84sge0ge0 39101 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
105 mulge0 10398 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≤ (1 + 𝐸)) ∧ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))) → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10645, 51, 103, 104, 105syl22anc 1318 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10741, 106eqbrtrd 4599 . . . . . . . . . 10 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10821, 107jca 552 . . . . . . . . 9 (𝜑 → ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
109 oveq1 6534 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (𝑧 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
110109oveq2d 6543 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · ((𝐴𝑍) − (𝐴𝑍))))
111 fveq2 6088 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐴𝑍) → (𝐻𝑧) = (𝐻‘(𝐴𝑍)))
112111fveq1d 6090 . . . . . . . . . . . . . . 15 (𝑧 = (𝐴𝑍) → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))
113112oveq2d 6543 . . . . . . . . . . . . . 14 (𝑧 = (𝐴𝑍) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
114113mpteq2dv 4667 . . . . . . . . . . . . 13 (𝑧 = (𝐴𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))
115114fveq2d 6092 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
116115oveq2d 6543 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
117110, 116breq12d 4590 . . . . . . . . . 10 (𝑧 = (𝐴𝑍) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
118117elrab 3330 . . . . . . . . 9 ((𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
119108, 118sylibr 222 . . . . . . . 8 (𝜑 → (𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
120119, 14syl6eleqr 2698 . . . . . . 7 (𝜑 → (𝐴𝑍) ∈ 𝑈)
121 ne0i 3879 . . . . . . 7 ((𝐴𝑍) ∈ 𝑈𝑈 ≠ ∅)
122120, 121syl 17 . . . . . 6 (𝜑𝑈 ≠ ∅)
12311, 13, 17, 122supicc 12150 . . . . 5 (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1242, 123eqeltrd 2687 . . . 4 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1252oveq1d 6542 . . . . . . 7 (𝜑 → (𝑆 − (𝐴𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴𝑍)))
126125oveq2d 6543 . . . . . 6 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))))
12711, 13iccssred 38398 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ)
12817, 127sstrd 3577 . . . . . . . 8 (𝜑𝑈 ⊆ ℝ)
12911, 13jca 552 . . . . . . . . . 10 (𝜑 → ((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ))
130 iccsupr 12096 . . . . . . . . . 10 ((((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐴𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
131129, 17, 120, 130syl3anc 1317 . . . . . . . . 9 (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
132131simp3d 1067 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
133 eqid 2609 . . . . . . . 8 {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} = {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
134128, 122, 132, 11, 133supsubc 38334 . . . . . . 7 (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴𝑍)) = sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < ))
135134oveq2d 6543 . . . . . 6 (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )))
13646rexrd 9946 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
137 icogelb 12055 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐺 ∈ (0[,)+∞)) → 0 ≤ 𝐺)
138136, 88, 37, 137syl3anc 1317 . . . . . . 7 (𝜑 → 0 ≤ 𝐺)
139 vex 3175 . . . . . . . . . . . 12 𝑟 ∈ V
140 eqeq1 2613 . . . . . . . . . . . . 13 (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑟 = (𝑢 − (𝐴𝑍))))
141140rexbidv 3033 . . . . . . . . . . . 12 (𝑤 = 𝑟 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍))))
142139, 141elab 3318 . . . . . . . . . . 11 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
143142biimpi 204 . . . . . . . . . 10 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
144143adantl 480 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
145 nfv 1829 . . . . . . . . . . 11 𝑢𝜑
146 nfcv 2750 . . . . . . . . . . . 12 𝑢𝑟
147 nfre1 2987 . . . . . . . . . . . . 13 𝑢𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))
148147nfab 2754 . . . . . . . . . . . 12 𝑢{𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
149146, 148nfel 2762 . . . . . . . . . . 11 𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
150145, 149nfan 1815 . . . . . . . . . 10 𝑢(𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
151 nfv 1829 . . . . . . . . . 10 𝑢0 ≤ 𝑟
15211rexrd 9946 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑍) ∈ ℝ*)
153152adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ*)
15413rexrd 9946 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑍) ∈ ℝ*)
155154adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ*)
15617sselda 3567 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
157 iccgelb 12060 . . . . . . . . . . . . . . . 16 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑢)
158153, 155, 156, 157syl3anc 1317 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴𝑍) ≤ 𝑢)
159128sselda 3567 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
16011adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ)
161159, 160subge0d 10469 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (0 ≤ (𝑢 − (𝐴𝑍)) ↔ (𝐴𝑍) ≤ 𝑢))
162158, 161mpbird 245 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 0 ≤ (𝑢 − (𝐴𝑍)))
1631623adant3 1073 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ (𝑢 − (𝐴𝑍)))
164 id 22 . . . . . . . . . . . . . . 15 (𝑟 = (𝑢 − (𝐴𝑍)) → 𝑟 = (𝑢 − (𝐴𝑍)))
165164eqcomd 2615 . . . . . . . . . . . . . 14 (𝑟 = (𝑢 − (𝐴𝑍)) → (𝑢 − (𝐴𝑍)) = 𝑟)
1661653ad2ant3 1076 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) = 𝑟)
167163, 166breqtrd 4603 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ 𝑟)
1681673exp 1255 . . . . . . . . . . 11 (𝜑 → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
169168adantr 479 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
170150, 151, 169rexlimd 3007 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟))
171144, 170mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 0 ≤ 𝑟)
172171ralrimiva 2948 . . . . . . 7 (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟)
173 simp3 1055 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 = (𝑢 − (𝐴𝑍)))
174159, 160resubcld 10310 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
1751743adant3 1073 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
176173, 175eqeltrd 2687 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 ∈ ℝ)
1771763exp 1255 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ)))
178177rexlimdv 3011 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
179178alrimiv 1841 . . . . . . . 8 (𝜑 → ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
180 abss 3633 . . . . . . . 8 ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
181179, 180sylibr 222 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ)
18223eqcomd 2615 . . . . . . . . . 10 (𝜑 → 0 = ((𝐴𝑍) − (𝐴𝑍)))
183 oveq1 6534 . . . . . . . . . . . 12 (𝑢 = (𝐴𝑍) → (𝑢 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
184183eqeq2d 2619 . . . . . . . . . . 11 (𝑢 = (𝐴𝑍) → (0 = (𝑢 − (𝐴𝑍)) ↔ 0 = ((𝐴𝑍) − (𝐴𝑍))))
185184rspcev 3281 . . . . . . . . . 10 (((𝐴𝑍) ∈ 𝑈 ∧ 0 = ((𝐴𝑍) − (𝐴𝑍))) → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
186120, 182, 185syl2anc 690 . . . . . . . . 9 (𝜑 → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
187 c0ex 9891 . . . . . . . . . 10 0 ∈ V
188 eqeq1 2613 . . . . . . . . . . 11 (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 0 = (𝑢 − (𝐴𝑍))))
189188rexbidv 3033 . . . . . . . . . 10 (𝑤 = 0 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍))))
190187, 189elab 3318 . . . . . . . . 9 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
191186, 190sylibr 222 . . . . . . . 8 (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
192 ne0i 3879 . . . . . . . 8 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
193191, 192syl 17 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
19413, 11resubcld 10310 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
195 vex 3175 . . . . . . . . . . . . 13 𝑠 ∈ V
196 eqeq1 2613 . . . . . . . . . . . . . 14 (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑠 = (𝑢 − (𝐴𝑍))))
197196rexbidv 3033 . . . . . . . . . . . . 13 (𝑤 = 𝑠 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍))))
198195, 197elab 3318 . . . . . . . . . . . 12 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
199198biimpi 204 . . . . . . . . . . 11 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
200199adantl 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
201 nfcv 2750 . . . . . . . . . . . . 13 𝑢𝑠
202201, 148nfel 2762 . . . . . . . . . . . 12 𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
203145, 202nfan 1815 . . . . . . . . . . 11 𝑢(𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
204 nfv 1829 . . . . . . . . . . 11 𝑢 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))
205 simp3 1055 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 = (𝑢 − (𝐴𝑍)))
2061603adant3 1073 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ℝ)
207133ad2ant1 1074 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐵𝑍) ∈ ℝ)
2081563adant3 1073 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
209213ad2ant1 1074 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
210206, 207, 208, 209iccsuble 38416 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
211205, 210eqbrtrd 4599 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
2122113exp 1255 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
213212adantr 479 . . . . . . . . . . 11 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
214203, 204, 213rexlimd 3007 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
215200, 214mpd 15 . . . . . . . . 9 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
216215ralrimiva 2948 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
217 breq2 4581 . . . . . . . . . 10 (𝑟 = ((𝐵𝑍) − (𝐴𝑍)) → (𝑠𝑟𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
218217ralbidv 2968 . . . . . . . . 9 (𝑟 = ((𝐵𝑍) − (𝐴𝑍)) → (∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟 ↔ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
219218rspcev 3281 . . . . . . . 8 ((((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
220194, 216, 219syl2anc 690 . . . . . . 7 (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
221 eqid 2609 . . . . . . . 8 {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
222 biid 249 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)))
223221, 222supmul1 10842 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
22438, 138, 172, 181, 193, 220, 223syl33anc 1332 . . . . . 6 (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
225126, 135, 2243eqtrd 2647 . . . . 5 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
226 vex 3175 . . . . . . . . . . . 12 𝑐 ∈ V
227 eqeq1 2613 . . . . . . . . . . . . 13 (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡)))
228227rexbidv 3033 . . . . . . . . . . . 12 (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡)))
229226, 228elab 3318 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
230229biimpi 204 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
231 nfv 1829 . . . . . . . . . . . 12 𝑡𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))
232 vex 3175 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
233 eqeq1 2613 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑡 = (𝑢 − (𝐴𝑍))))
234233rexbidv 3033 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍))))
235232, 234elab 3318 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
236235biimpi 204 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
237236adantr 479 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
238 simpl 471 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · 𝑡))
239 oveq2 6535 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝑢 − (𝐴𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
240239adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
241238, 240eqtrd 2643 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
242241ex 448 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
243242reximdv 2998 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 · 𝑡) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
244243adantl 480 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
245237, 244mpd 15 . . . . . . . . . . . . 13 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
246245ex 448 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
247231, 246rexlimi 3005 . . . . . . . . . . 11 (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
248247a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
249230, 248mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
250249adantl 480 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
251 simp3 1055 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
25238adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 𝐺 ∈ ℝ)
253252, 174remulcld 9927 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ∈ ℝ)
25445adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (1 + 𝐸) ∈ ℝ)
25552a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → ℕ ∈ V)
25660adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
25764adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
258159adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ)
25979adantlr 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
26074, 258, 256, 259hsphoif 39290 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻𝑢)‘(𝐷𝑗)):𝑊⟶ℝ)
26127, 256, 257, 260hoidmvcl 39296 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,)+∞))
26254, 261sseldi 3565 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,]+∞))
263 eqid 2609 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
264262, 263fmptd 6277 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
265255, 264sge0cl 39098 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞))
266255, 264sge0xrcl 39102 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ*)
26787a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → +∞ ∈ ℝ*)
26890adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
269 nfv 1829 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑢𝑈)
27093adantlr 746 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
27196adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
27227, 256, 271, 9, 258, 74, 257, 259hsphoidmvle 39300 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
273269, 255, 262, 270, 272sge0lempt 39127 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
27499adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
275266, 268, 267, 273, 274xrlelttrd 11829 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) < +∞)
276266, 267, 275xrltned 38338 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞)
277 ge0xrre 38429 . . . . . . . . . . . . . . . 16 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
278265, 276, 277syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
279254, 278remulcld 9927 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ∈ ℝ)
280127, 124sseldd 3568 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
28127, 30, 95, 9, 61, 76, 89, 65, 280sge0hsphoire 39303 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
28245, 281remulcld 9927 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
283282adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
28414eleq2i 2679 . . . . . . . . . . . . . . . . . 18 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
285284biimpi 204 . . . . . . . . . . . . . . . . 17 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
286 oveq1 6534 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (𝑧 − (𝐴𝑍)) = (𝑢 − (𝐴𝑍)))
287286oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑢 − (𝐴𝑍))))
288 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑢 → (𝐻𝑧) = (𝐻𝑢))
289288fveq1d 6090 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑢 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑢)‘(𝐷𝑗)))
290289oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑢 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
291290mpteq2dv 4667 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))
292291fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))
293292oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
294287, 293breq12d 4590 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
295294elrab 3330 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
296285, 295sylib 206 . . . . . . . . . . . . . . . 16 (𝑢𝑈 → (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
297296simprd 477 . . . . . . . . . . . . . . 15 (𝑢𝑈 → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
298297adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
299281adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
30051adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 0 ≤ (1 + 𝐸))
301280adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
30274, 301, 60, 79hsphoif 39290 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑆)‘(𝐷𝑗)):𝑊⟶ℝ)
30327, 60, 64, 302hoidmvcl 39296 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,)+∞))
30454, 303sseldi 3565 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
305304adantlr 746 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
306301adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
307128adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
308122adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
309132adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
310 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑢𝑈)
311 suprub 10836 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
312307, 308, 309, 310, 311syl31anc 1320 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
313312, 1syl6breqr 4619 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → 𝑢𝑆)
314313adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢𝑆)
31527, 256, 271, 9, 258, 306, 314, 74, 257, 259hsphoidmvle2 39299 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
316269, 255, 262, 305, 315sge0lempt 39127 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
317278, 299, 254, 300, 316lemul2ad 10816 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
318253, 279, 283, 298, 317letrd 10046 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3193183adant3 1073 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
320251, 319eqbrtrd 4599 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3213203exp 1255 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))))
322321rexlimdv 3011 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
323322adantr 479 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
324250, 323mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
325324ralrimiva 2948 . . . . . 6 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
326230adantl 480 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
327 nfv 1829 . . . . . . . . . . . 12 𝑡𝜑
328 nfcv 2750 . . . . . . . . . . . . 13 𝑡𝑐
329 nfre1 2987 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)
330329nfab 2754 . . . . . . . . . . . . 13 𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
331328, 330nfel 2762 . . . . . . . . . . . 12 𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
332327, 331nfan 1815 . . . . . . . . . . 11 𝑡(𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
333 nfv 1829 . . . . . . . . . . 11 𝑡 𝑐 ∈ ℝ
334236adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
335 simpr 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡))
3362523adant3 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝐺 ∈ ℝ)
337 simp3 1055 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 = (𝑢 − (𝐴𝑍)))
3381743adant3 1073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
339337, 338eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 ∈ ℝ)
340336, 339remulcld 9927 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) ∈ ℝ)
341340adantr 479 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ)
342335, 341eqeltrd 2687 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ)
343342ex 448 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
3443433exp 1255 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑢𝑈 → (𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))))
345344rexlimdv 3011 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
346345adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
347334, 346mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
348347ex 448 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
349348adantr 479 . . . . . . . . . . 11 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
350332, 333, 349rexlimd 3007 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
351326, 350mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ)
352351ralrimiva 2948 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
353 dfss3 3557 . . . . . . . 8 ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
354352, 353sylibr 222 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ)
35540eqcomd 2615 . . . . . . . . . 10 (𝜑 → 0 = (𝐺 · 0))
356 oveq2 6535 . . . . . . . . . . . 12 (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0))
357356eqeq2d 2619 . . . . . . . . . . 11 (𝑡 = 0 → (0 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 0)))
358357rspcev 3281 . . . . . . . . . 10 ((0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
359191, 355, 358syl2anc 690 . . . . . . . . 9 (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
360 eqeq1 2613 . . . . . . . . . . 11 (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡)))
361360rexbidv 3033 . . . . . . . . . 10 (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡)))
362187, 361elab 3318 . . . . . . . . 9 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
363359, 362sylibr 222 . . . . . . . 8 (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
364 ne0i 3879 . . . . . . . 8 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
365363, 364syl 17 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
36638, 194remulcld 9927 . . . . . . . 8 (𝜑 → (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ)
367194adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
368138adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 0 ≤ 𝐺)
36913adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ)
370 iccleub 12059 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → 𝑢 ≤ (𝐵𝑍))
371153, 155, 156, 370syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → 𝑢 ≤ (𝐵𝑍))
372159, 369, 160, 371lesub1dd 10495 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
373174, 367, 252, 368, 372lemul2ad 10816 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3743733adant3 1073 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
375251, 374eqbrtrd 4599 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3763753exp 1255 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))))
377376rexlimdv 3011 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
378377adantr 479 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
379250, 378mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
380379ralrimiva 2948 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
381 breq2 4581 . . . . . . . . . 10 (𝑦 = (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) → (𝑐𝑦𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
382381ralbidv 2968 . . . . . . . . 9 (𝑦 = (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) → (∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦 ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
383382rspcev 3281 . . . . . . . 8 (((𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
384366, 380, 383syl2anc 690 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
385 suprleub 10839 . . . . . . 7 ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦) ∧ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
386354, 365, 384, 282, 385syl31anc 1320 . . . . . 6 (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
387325, 386mpbird 245 . . . . 5 (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
388225, 387eqbrtrd 4599 . . . 4 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
389124, 388jca 552 . . 3 (𝜑 → (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
390 oveq1 6534 . . . . . 6 (𝑧 = 𝑆 → (𝑧 − (𝐴𝑍)) = (𝑆 − (𝐴𝑍)))
391390oveq2d 6543 . . . . 5 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑆 − (𝐴𝑍))))
392 fveq2 6088 . . . . . . . . . 10 (𝑧 = 𝑆 → (𝐻𝑧) = (𝐻𝑆))
393392fveq1d 6090 . . . . . . . . 9 (𝑧 = 𝑆 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑆)‘(𝐷𝑗)))
394393oveq2d 6543 . . . . . . . 8 (𝑧 = 𝑆 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
395394mpteq2dv 4667 . . . . . . 7 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))
396395fveq2d 6092 . . . . . 6 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
397396oveq2d 6543 . . . . 5 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
398391, 397breq12d 4590 . . . 4 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
399398elrab 3330 . . 3 (𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
400389, 399sylibr 222 . 2 (𝜑𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
401400, 14syl6eleqr 2698 1 (𝜑𝑆𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030  wal 1472   = wceq 1474  wcel 1976  {cab 2595  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  wss 3539  c0 3873  ifcif 4035  {csn 4124   class class class wbr 4577  cmpt 4637  cres 5030  wf 5786  cfv 5790  (class class class)co 6527  cmpt2 6529  𝑚 cmap 7722  Fincfn 7819  supcsup 8207  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798  +∞cpnf 9928  *cxr 9930   < clt 9931  cle 9932  cmin 10118  cn 10870  +crp 11667  [,)cico 12007  [,]cicc 12008  cprod 14423  volcvol 22984  Σ^csumge0 39079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-n0 11143  df-z 11214  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-rlim 14017  df-sum 14214  df-prod 14424  df-rest 15855  df-topgen 15876  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-top 20469  df-bases 20470  df-topon 20471  df-cmp 20948  df-ovol 22985  df-vol 22986  df-sumge0 39080
This theorem is referenced by:  hoidmvlelem4  39312
  Copyright terms: Public domain W3C validator