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 43808
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 4575 . . . . . . . . . 10 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (𝜑𝑍 ∈ {𝑍})
7 elun2 4091 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
86, 7syl 17 . . . . . . . 8 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
108, 9eleqtrrdi 2849 . . . . . . 7 (𝜑𝑍𝑊)
113, 10ffvelrnd 6905 . . . . . 6 (𝜑 → (𝐴𝑍) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (𝜑𝐵:𝑊⟶ℝ)
1312, 10ffvelrnd 6905 . . . . . 6 (𝜑 → (𝐵𝑍) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
15 ssrab2 3993 . . . . . . . 8 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1614, 15eqsstri 3935 . . . . . . 7 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1716a1i 11 . . . . . 6 (𝜑𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)))
1811leidd 11398 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐴𝑍))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (𝜑 → (𝐴𝑍) < (𝐵𝑍))
2011, 13, 19ltled 10980 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐵𝑍))
2111, 13, 11, 18, 20eliccd 42717 . . . . . . . . . 10 (𝜑 → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
2211recnd 10861 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝑍) ∈ ℂ)
2322subidd 11177 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑍) − (𝐴𝑍)) = 0)
2423oveq2d 7229 . . . . . . . . . . . 12 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = (𝐺 · 0))
25 rge0ssre 13044 . . . . . . . . . . . . . . 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 8898 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ Fin)
31 ssun1 4086 . . . . . . . . . . . . . . . . . . . 20 𝑌 ⊆ (𝑌 ∪ {𝑍})
3231, 9sseqtrri 3938 . . . . . . . . . . . . . . . . . . 19 𝑌𝑊
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑊)
343, 33fssresd 6586 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
3512, 33fssresd 6586 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
3627, 30, 34, 35hoidmvcl 43795 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
3726, 36eqeltrid 2842 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ (0[,)+∞))
3825, 37sseldi 3899 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ ℝ)
3938recnd 10861 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℂ)
4039mul01d 11031 . . . . . . . . . . . 12 (𝜑 → (𝐺 · 0) = 0)
4124, 40eqtrd 2777 . . . . . . . . . . 11 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = 0)
42 1red 10834 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
4443rpred 12628 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
4542, 44readdcld 10862 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
46 0red 10836 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
47 0lt1 11354 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
4942, 43ltaddrpd 12661 . . . . . . . . . . . . . 14 (𝜑 → 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 10993 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 + 𝐸))
5146, 45, 50ltled 10980 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 + 𝐸))
52 nnex 11836 . . . . . . . . . . . . . . 15 ℕ ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
54 icossicc 13024 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ (0[,]+∞)
55 snfi 8721 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
57 unfi 8850 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
599, 58eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ Fin)
6059adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑊))
6261ffvelrnda 6904 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑m 𝑊))
63 elmapi 8530 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑗) ∈ (ℝ ↑m 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
66 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑗𝑌𝑌))
67 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑐𝑗) = (𝑐))
6867breq1d 5063 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐) ≤ 𝑥))
6968, 67ifbieq1d 4463 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐) ≤ 𝑥, (𝑐), 𝑥))
7066, 67, 69ifbieq12d 4467 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7170cbvmptv 5158 . . . . . . . . . . . . . . . . . . . . 21 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7271mpteq2i 5147 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥))))
7372mpteq2i 5147 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7465, 73eqtri 2765 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7511adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐴𝑍) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑊))
7776ffvelrnda 6904 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑m 𝑊))
78 elmapi 8530 . . . . . . . . . . . . . . . . . . 19 ((𝐷𝑗) ∈ (ℝ ↑m 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
8074, 75, 60, 79hsphoif 43789 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)):𝑊⟶ℝ)
8127, 60, 64, 80hoidmvcl 43795 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,)+∞))
8254, 81sseldi 3899 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,]+∞))
8382fmpttd 6932 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
8453, 83sge0cl 43594 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞))
8553, 83sge0xrcl 43598 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ*)
86 pnfxr 10887 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . . . 14 (𝜑 → +∞ ∈ ℝ*)
88 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
8988rexrd 10883 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
90 nfv 1922 . . . . . . . . . . . . . . . 16 𝑗𝜑
9127, 60, 64, 79hoidmvcl 43795 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,)+∞))
9254, 91sseldi 3899 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
934eldifbd 3879 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑍𝑌)
9410, 93eldifd 3877 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ (𝑊𝑌))
9594adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
9627, 60, 95, 9, 75, 74, 64, 79hsphoidmvle 43799 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
9790, 53, 82, 92, 96sge0lempt 43623 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
9888ltpnfd 12713 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
9985, 89, 87, 97, 98xrlelttrd 12750 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) < +∞)
10085, 87, 99xrltned 42569 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞)
101 ge0xrre 42744 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10284, 100, 101syl2anc 587 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10353, 83sge0ge0 43597 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
104 mulge0 11350 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≤ (1 + 𝐸)) ∧ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))) → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10545, 51, 102, 103, 104syl22anc 839 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10641, 105eqbrtrd 5075 . . . . . . . . . 10 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10721, 106jca 515 . . . . . . . . 9 (𝜑 → ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
108 oveq1 7220 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (𝑧 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
109108oveq2d 7229 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · ((𝐴𝑍) − (𝐴𝑍))))
110 fveq2 6717 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐴𝑍) → (𝐻𝑧) = (𝐻‘(𝐴𝑍)))
111110fveq1d 6719 . . . . . . . . . . . . . . 15 (𝑧 = (𝐴𝑍) → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))
112111oveq2d 7229 . . . . . . . . . . . . . 14 (𝑧 = (𝐴𝑍) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
113112mpteq2dv 5151 . . . . . . . . . . . . 13 (𝑧 = (𝐴𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))
114113fveq2d 6721 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
115114oveq2d 7229 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
116109, 115breq12d 5066 . . . . . . . . . 10 (𝑧 = (𝐴𝑍) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
117116elrab 3602 . . . . . . . . 9 ((𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
118107, 117sylibr 237 . . . . . . . 8 (𝜑 → (𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
119118, 14eleqtrrdi 2849 . . . . . . 7 (𝜑 → (𝐴𝑍) ∈ 𝑈)
120 ne0i 4249 . . . . . . 7 ((𝐴𝑍) ∈ 𝑈𝑈 ≠ ∅)
121119, 120syl 17 . . . . . 6 (𝜑𝑈 ≠ ∅)
12211, 13, 17, 121supicc 13089 . . . . 5 (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1232, 122eqeltrd 2838 . . . 4 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1242oveq1d 7228 . . . . . . 7 (𝜑 → (𝑆 − (𝐴𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴𝑍)))
125124oveq2d 7229 . . . . . 6 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))))
12611, 13iccssred 13022 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ)
12717, 126sstrd 3911 . . . . . . . 8 (𝜑𝑈 ⊆ ℝ)
12811, 13jca 515 . . . . . . . . . 10 (𝜑 → ((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ))
129 iccsupr 13030 . . . . . . . . . 10 ((((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐴𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
130128, 17, 119, 129syl3anc 1373 . . . . . . . . 9 (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
131130simp3d 1146 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
132 eqid 2737 . . . . . . . 8 {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} = {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
133127, 121, 131, 11, 132supsubc 42565 . . . . . . 7 (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴𝑍)) = sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < ))
134133oveq2d 7229 . . . . . 6 (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )))
13546rexrd 10883 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
136 icogelb 12986 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐺 ∈ (0[,)+∞)) → 0 ≤ 𝐺)
137135, 87, 37, 136syl3anc 1373 . . . . . . 7 (𝜑 → 0 ≤ 𝐺)
138 vex 3412 . . . . . . . . . . . 12 𝑟 ∈ V
139 eqeq1 2741 . . . . . . . . . . . . 13 (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑟 = (𝑢 − (𝐴𝑍))))
140139rexbidv 3216 . . . . . . . . . . . 12 (𝑤 = 𝑟 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍))))
141138, 140elab 3587 . . . . . . . . . . 11 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
142141biimpi 219 . . . . . . . . . 10 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
143142adantl 485 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
144 nfv 1922 . . . . . . . . . . 11 𝑢𝜑
145 nfcv 2904 . . . . . . . . . . . 12 𝑢𝑟
146 nfre1 3225 . . . . . . . . . . . . 13 𝑢𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))
147146nfab 2910 . . . . . . . . . . . 12 𝑢{𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
148145, 147nfel 2918 . . . . . . . . . . 11 𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
149144, 148nfan 1907 . . . . . . . . . 10 𝑢(𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
150 nfv 1922 . . . . . . . . . 10 𝑢0 ≤ 𝑟
15111rexrd 10883 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑍) ∈ ℝ*)
152151adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ*)
15313rexrd 10883 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑍) ∈ ℝ*)
154153adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ*)
15517sselda 3901 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
156 iccgelb 12991 . . . . . . . . . . . . . . . 16 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑢)
157152, 154, 155, 156syl3anc 1373 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴𝑍) ≤ 𝑢)
158127sselda 3901 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
15911adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ)
160158, 159subge0d 11422 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (0 ≤ (𝑢 − (𝐴𝑍)) ↔ (𝐴𝑍) ≤ 𝑢))
161157, 160mpbird 260 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 0 ≤ (𝑢 − (𝐴𝑍)))
1621613adant3 1134 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ (𝑢 − (𝐴𝑍)))
163 id 22 . . . . . . . . . . . . . . 15 (𝑟 = (𝑢 − (𝐴𝑍)) → 𝑟 = (𝑢 − (𝐴𝑍)))
164163eqcomd 2743 . . . . . . . . . . . . . 14 (𝑟 = (𝑢 − (𝐴𝑍)) → (𝑢 − (𝐴𝑍)) = 𝑟)
1651643ad2ant3 1137 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) = 𝑟)
166162, 165breqtrd 5079 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ 𝑟)
1671663exp 1121 . . . . . . . . . . 11 (𝜑 → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
168167adantr 484 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
169149, 150, 168rexlimd 3236 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟))
170143, 169mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 0 ≤ 𝑟)
171170ralrimiva 3105 . . . . . . 7 (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟)
172 simp3 1140 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 = (𝑢 − (𝐴𝑍)))
173158, 159resubcld 11260 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
1741733adant3 1134 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
175172, 174eqeltrd 2838 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 ∈ ℝ)
1761753exp 1121 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ)))
177176rexlimdv 3202 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
178177alrimiv 1935 . . . . . . . 8 (𝜑 → ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
179 abss 3974 . . . . . . . 8 ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
180178, 179sylibr 237 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ)
18123eqcomd 2743 . . . . . . . . . 10 (𝜑 → 0 = ((𝐴𝑍) − (𝐴𝑍)))
182 oveq1 7220 . . . . . . . . . . 11 (𝑢 = (𝐴𝑍) → (𝑢 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
183182rspceeqv 3552 . . . . . . . . . 10 (((𝐴𝑍) ∈ 𝑈 ∧ 0 = ((𝐴𝑍) − (𝐴𝑍))) → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
184119, 181, 183syl2anc 587 . . . . . . . . 9 (𝜑 → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
185 eqeq1 2741 . . . . . . . . . 10 (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 0 = (𝑢 − (𝐴𝑍))))
186185rexbidv 3216 . . . . . . . . 9 (𝑤 = 0 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍))))
18746, 184, 186elabd 3590 . . . . . . . 8 (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
188 ne0i 4249 . . . . . . . 8 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
189187, 188syl 17 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
19013, 11resubcld 11260 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
191 vex 3412 . . . . . . . . . . . . 13 𝑠 ∈ V
192 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑠 = (𝑢 − (𝐴𝑍))))
193192rexbidv 3216 . . . . . . . . . . . . 13 (𝑤 = 𝑠 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍))))
194191, 193elab 3587 . . . . . . . . . . . 12 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
195194biimpi 219 . . . . . . . . . . 11 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
196195adantl 485 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
197 nfcv 2904 . . . . . . . . . . . . 13 𝑢𝑠
198197, 147nfel 2918 . . . . . . . . . . . 12 𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
199144, 198nfan 1907 . . . . . . . . . . 11 𝑢(𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
200 nfv 1922 . . . . . . . . . . 11 𝑢 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))
201 simp3 1140 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 = (𝑢 − (𝐴𝑍)))
2021593adant3 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ℝ)
203133ad2ant1 1135 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐵𝑍) ∈ ℝ)
2041553adant3 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
205213ad2ant1 1135 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
206202, 203, 204, 205iccsuble 42732 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
207201, 206eqbrtrd 5075 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
2082073exp 1121 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
209208adantr 484 . . . . . . . . . . 11 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
210199, 200, 209rexlimd 3236 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
211196, 210mpd 15 . . . . . . . . 9 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
212211ralrimiva 3105 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
213 brralrspcev 5113 . . . . . . . 8 ((((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
214190, 212, 213syl2anc 587 . . . . . . 7 (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
215 eqid 2737 . . . . . . . 8 {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
216 biid 264 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)))
217215, 216supmul1 11801 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
21838, 137, 171, 180, 189, 214, 217syl33anc 1387 . . . . . 6 (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
219125, 134, 2183eqtrd 2781 . . . . 5 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
220 vex 3412 . . . . . . . . . . . 12 𝑐 ∈ V
221 eqeq1 2741 . . . . . . . . . . . . 13 (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡)))
222221rexbidv 3216 . . . . . . . . . . . 12 (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡)))
223220, 222elab 3587 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
224223biimpi 219 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
225 nfv 1922 . . . . . . . . . . . 12 𝑡𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))
226 vex 3412 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
227 eqeq1 2741 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑡 = (𝑢 − (𝐴𝑍))))
228227rexbidv 3216 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍))))
229226, 228elab 3587 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
230229biimpi 219 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
231230adantr 484 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
232 simpl 486 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · 𝑡))
233 oveq2 7221 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝑢 − (𝐴𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
234233adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
235232, 234eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
236235ex 416 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
237236reximdv 3192 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 · 𝑡) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
238237adantl 485 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
239231, 238mpd 15 . . . . . . . . . . . . 13 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
240239ex 416 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
241225, 240rexlimi 3234 . . . . . . . . . . 11 (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
242241a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
243224, 242mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
244243adantl 485 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
245 simp3 1140 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
24638adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 𝐺 ∈ ℝ)
247246, 173remulcld 10863 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ∈ ℝ)
24845adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (1 + 𝐸) ∈ ℝ)
24952a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → ℕ ∈ V)
25060adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
25164adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
252158adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ)
25379adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
25474, 252, 250, 253hsphoif 43789 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻𝑢)‘(𝐷𝑗)):𝑊⟶ℝ)
25527, 250, 251, 254hoidmvcl 43795 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,)+∞))
25654, 255sseldi 3899 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,]+∞))
257256fmpttd 6932 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
258249, 257sge0cl 43594 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞))
259249, 257sge0xrcl 43598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ*)
26086a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → +∞ ∈ ℝ*)
26189adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
262 nfv 1922 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑢𝑈)
26392adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
26495adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
26527, 250, 264, 9, 252, 74, 251, 253hsphoidmvle 43799 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
266262, 249, 256, 263, 265sge0lempt 43623 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
26798adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
268259, 261, 260, 266, 267xrlelttrd 12750 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) < +∞)
269259, 260, 268xrltned 42569 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞)
270 ge0xrre 42744 . . . . . . . . . . . . . . . 16 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
271258, 269, 270syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
272248, 271remulcld 10863 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ∈ ℝ)
273126, 123sseldd 3902 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
27427, 30, 94, 9, 61, 76, 88, 65, 273sge0hsphoire 43802 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
27545, 274remulcld 10863 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
276275adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
27714eleq2i 2829 . . . . . . . . . . . . . . . . . 18 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
278277biimpi 219 . . . . . . . . . . . . . . . . 17 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
279 oveq1 7220 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (𝑧 − (𝐴𝑍)) = (𝑢 − (𝐴𝑍)))
280279oveq2d 7229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑢 − (𝐴𝑍))))
281 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑢 → (𝐻𝑧) = (𝐻𝑢))
282281fveq1d 6719 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑢 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑢)‘(𝐷𝑗)))
283282oveq2d 7229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑢 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
284283mpteq2dv 5151 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))
285284fveq2d 6721 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))
286285oveq2d 7229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
287280, 286breq12d 5066 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
288287elrab 3602 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
289278, 288sylib 221 . . . . . . . . . . . . . . . 16 (𝑢𝑈 → (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
290289simprd 499 . . . . . . . . . . . . . . 15 (𝑢𝑈 → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
291290adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
292274adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
29351adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 0 ≤ (1 + 𝐸))
294273adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
29574, 294, 60, 79hsphoif 43789 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑆)‘(𝐷𝑗)):𝑊⟶ℝ)
29627, 60, 64, 295hoidmvcl 43795 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,)+∞))
29754, 296sseldi 3899 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
298297adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
299294adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
300127adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
301121adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
302131adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
303 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑢𝑈)
304 suprub 11793 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
305300, 301, 302, 303, 304syl31anc 1375 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
306305, 1breqtrrdi 5095 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → 𝑢𝑆)
307306adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢𝑆)
30827, 250, 264, 9, 252, 299, 307, 74, 251, 253hsphoidmvle2 43798 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
309262, 249, 256, 298, 308sge0lempt 43623 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
310271, 292, 248, 293, 309lemul2ad 11772 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
311247, 272, 276, 291, 310letrd 10989 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3123113adant3 1134 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
313245, 312eqbrtrd 5075 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3143133exp 1121 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))))
315314rexlimdv 3202 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
316315adantr 484 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
317244, 316mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
318317ralrimiva 3105 . . . . . 6 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
319224adantl 485 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
320 nfv 1922 . . . . . . . . . . . 12 𝑡𝜑
321 nfcv 2904 . . . . . . . . . . . . 13 𝑡𝑐
322 nfre1 3225 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)
323322nfab 2910 . . . . . . . . . . . . 13 𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
324321, 323nfel 2918 . . . . . . . . . . . 12 𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
325320, 324nfan 1907 . . . . . . . . . . 11 𝑡(𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
326 nfv 1922 . . . . . . . . . . 11 𝑡 𝑐 ∈ ℝ
327230adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
328 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡))
3292463adant3 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝐺 ∈ ℝ)
330 simp3 1140 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 = (𝑢 − (𝐴𝑍)))
3311733adant3 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
332330, 331eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 ∈ ℝ)
333329, 332remulcld 10863 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) ∈ ℝ)
334333adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ)
335328, 334eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ)
336335ex 416 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
3373363exp 1121 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑢𝑈 → (𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))))
338337rexlimdv 3202 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
339338adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
340327, 339mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
341340ex 416 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
342341adantr 484 . . . . . . . . . . 11 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
343325, 326, 342rexlimd 3236 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
344319, 343mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ)
345344ralrimiva 3105 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
346 dfss3 3888 . . . . . . . 8 ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
347345, 346sylibr 237 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ)
34840eqcomd 2743 . . . . . . . . . 10 (𝜑 → 0 = (𝐺 · 0))
349 oveq2 7221 . . . . . . . . . . 11 (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0))
350349rspceeqv 3552 . . . . . . . . . 10 ((0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
351187, 348, 350syl2anc 587 . . . . . . . . 9 (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
352 eqeq1 2741 . . . . . . . . . 10 (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡)))
353352rexbidv 3216 . . . . . . . . 9 (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡)))
35446, 351, 353elabd 3590 . . . . . . . 8 (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
355 ne0i 4249 . . . . . . . 8 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
356354, 355syl 17 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
35738, 190remulcld 10863 . . . . . . . 8 (𝜑 → (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ)
358190adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
359137adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 0 ≤ 𝐺)
36013adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ)
361 iccleub 12990 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → 𝑢 ≤ (𝐵𝑍))
362152, 154, 155, 361syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → 𝑢 ≤ (𝐵𝑍))
363158, 360, 159, 362lesub1dd 11448 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
364173, 358, 246, 359, 363lemul2ad 11772 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3653643adant3 1134 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
366245, 365eqbrtrd 5075 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3673663exp 1121 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))))
368367rexlimdv 3202 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
369368adantr 484 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
370244, 369mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
371370ralrimiva 3105 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
372 brralrspcev 5113 . . . . . . . 8 (((𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
373357, 371, 372syl2anc 587 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
374 suprleub 11798 . . . . . . 7 ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦) ∧ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
375347, 356, 373, 275, 374syl31anc 1375 . . . . . 6 (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
376318, 375mpbird 260 . . . . 5 (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
377219, 376eqbrtrd 5075 . . . 4 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
378123, 377jca 515 . . 3 (𝜑 → (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
379 oveq1 7220 . . . . . 6 (𝑧 = 𝑆 → (𝑧 − (𝐴𝑍)) = (𝑆 − (𝐴𝑍)))
380379oveq2d 7229 . . . . 5 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑆 − (𝐴𝑍))))
381 fveq2 6717 . . . . . . . . . 10 (𝑧 = 𝑆 → (𝐻𝑧) = (𝐻𝑆))
382381fveq1d 6719 . . . . . . . . 9 (𝑧 = 𝑆 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑆)‘(𝐷𝑗)))
383382oveq2d 7229 . . . . . . . 8 (𝑧 = 𝑆 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
384383mpteq2dv 5151 . . . . . . 7 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))
385384fveq2d 6721 . . . . . 6 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
386385oveq2d 7229 . . . . 5 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
387380, 386breq12d 5066 . . . 4 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
388387elrab 3602 . . 3 (𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
389378, 388sylibr 237 . 2 (𝜑𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
390389, 14eleqtrrdi 2849 1 (𝜑𝑆𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089  wal 1541   = wceq 1543  wcel 2110  {cab 2714  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3408  cdif 3863  cun 3864  wss 3866  c0 4237  ifcif 4439  {csn 4541   class class class wbr 5053  cmpt 5135  cres 5553  wf 6376  cfv 6380  (class class class)co 7213  cmpo 7215  m cmap 8508  Fincfn 8626  supcsup 9056  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  +∞cpnf 10864  *cxr 10866   < clt 10867  cle 10868  cmin 11062  cn 11830  +crp 12586  [,)cico 12937  [,]cicc 12938  cprod 15467  volcvol 24360  Σ^csumge0 43575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-pm 8511  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-rlim 15050  df-sum 15250  df-prod 15468  df-rest 16927  df-topgen 16948  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-top 21791  df-topon 21808  df-bases 21843  df-cmp 22284  df-ovol 24361  df-vol 24362  df-sumge0 43576
This theorem is referenced by:  hoidmvlelem4  43811
  Copyright terms: Public domain W3C validator