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

Theorem hoidmvlelem1 42441
 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 4510 . . . . . . . . . 10 (𝑍 ∈ (𝑋𝑌) → 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (𝜑𝑍 ∈ {𝑍})
7 elun2 4080 . . . . . . . . 9 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍}))
86, 7syl 17 . . . . . . . 8 (𝜑𝑍 ∈ (𝑌 ∪ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 𝑊 = (𝑌 ∪ {𝑍})
108, 9syl6eleqr 2896 . . . . . . 7 (𝜑𝑍𝑊)
113, 10ffvelrnd 6724 . . . . . 6 (𝜑 → (𝐴𝑍) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (𝜑𝐵:𝑊⟶ℝ)
1312, 10ffvelrnd 6724 . . . . . 6 (𝜑 → (𝐵𝑍) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 𝑈 = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))}
15 ssrab2 3983 . . . . . . . 8 {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1614, 15eqsstri 3928 . . . . . . 7 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍))
1716a1i 11 . . . . . 6 (𝜑𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)))
1811leidd 11060 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐴𝑍))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (𝜑 → (𝐴𝑍) < (𝐵𝑍))
2011, 13, 19ltled 10641 . . . . . . . . . . 11 (𝜑 → (𝐴𝑍) ≤ (𝐵𝑍))
2111, 13, 11, 18, 20eliccd 41342 . . . . . . . . . 10 (𝜑 → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
2211recnd 10522 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝑍) ∈ ℂ)
2322subidd 10839 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑍) − (𝐴𝑍)) = 0)
2423oveq2d 7039 . . . . . . . . . . . 12 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = (𝐺 · 0))
25 rge0ssre 12698 . . . . . . . . . . . . . . 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 8594 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ Fin)
31 ssun1 4075 . . . . . . . . . . . . . . . . . . . 20 𝑌 ⊆ (𝑌 ∪ {𝑍})
3231, 9sseqtr4i 3931 . . . . . . . . . . . . . . . . . . 19 𝑌𝑊
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝑊)
343, 33fssresd 6420 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑌):𝑌⟶ℝ)
3512, 33fssresd 6420 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑌):𝑌⟶ℝ)
3627, 30, 34, 35hoidmvcl 42428 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑌)(𝐿𝑌)(𝐵𝑌)) ∈ (0[,)+∞))
3726, 36syl5eqel 2889 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ (0[,)+∞))
3825, 37sseldi 3893 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ ℝ)
3938recnd 10522 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℂ)
4039mul01d 10692 . . . . . . . . . . . 12 (𝜑 → (𝐺 · 0) = 0)
4124, 40eqtrd 2833 . . . . . . . . . . 11 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) = 0)
42 1red 10495 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
4443rpred 12285 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
4542, 44readdcld 10523 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
46 0red 10497 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
47 0lt1 11016 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
4942, 43ltaddrpd 12318 . . . . . . . . . . . . . 14 (𝜑 → 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 10654 . . . . . . . . . . . . 13 (𝜑 → 0 < (1 + 𝐸))
5146, 45, 50ltled 10641 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 + 𝐸))
52 nnex 11498 . . . . . . . . . . . . . . 15 ℕ ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ∈ V)
54 icossicc 12678 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ (0[,]+∞)
55 snfi 8449 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑍} ∈ Fin)
57 unfi 8638 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
599, 58syl5eqel 2889 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ Fin)
6059adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑊))
6261ffvelrnda 6723 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊))
63 elmapi 8285 . . . . . . . . . . . . . . . . . 18 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐶𝑗):𝑊⟶ℝ)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))))
66 eleq1w 2867 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑗𝑌𝑌))
67 fveq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → (𝑐𝑗) = (𝑐))
6867breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = → ((𝑐𝑗) ≤ 𝑥 ↔ (𝑐) ≤ 𝑥))
6968, 67ifbieq1d 4410 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = → if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥) = if((𝑐) ≤ 𝑥, (𝑐), 𝑥))
7066, 67, 69ifbieq12d 4414 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = → if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)) = if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7170cbvmptv 5068 . . . . . . . . . . . . . . . . . . . . 21 (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))) = (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))
7271mpteq2i 5059 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥))))
7372mpteq2i 5059 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗𝑊 ↦ if(𝑗𝑌, (𝑐𝑗), if((𝑐𝑗) ≤ 𝑥, (𝑐𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7465, 73eqtri 2821 . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑊 ↦ if(𝑌, (𝑐), if((𝑐) ≤ 𝑥, (𝑐), 𝑥)))))
7511adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐴𝑍) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑊))
7776ffvelrnda 6723 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊))
78 elmapi 8285 . . . . . . . . . . . . . . . . . . 19 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑊) → (𝐷𝑗):𝑊⟶ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
8074, 75, 60, 79hsphoif 42422 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)):𝑊⟶ℝ)
8127, 60, 64, 80hoidmvcl 42428 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,)+∞))
8254, 81sseldi 3893 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ∈ (0[,]+∞))
8382fmpttd 6749 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
8453, 83sge0cl 42227 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞))
8553, 83sge0xrcl 42231 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ*)
86 pnfxr 10548 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . . . 14 (𝜑 → +∞ ∈ ℝ*)
88 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ)
8988rexrd 10544 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
90 nfv 1896 . . . . . . . . . . . . . . . 16 𝑗𝜑
9127, 60, 64, 79hoidmvcl 42428 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,)+∞))
9254, 91sseldi 3893 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
934eldifbd 3878 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑍𝑌)
9410, 93eldifd 3876 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ (𝑊𝑌))
9594adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
9627, 60, 95, 9, 75, 74, 64, 79hsphoidmvle 42432 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
9790, 53, 82, 92, 96sge0lempt 42256 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
9888ltpnfd 12370 . . . . . . . . . . . . . . 15 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
9985, 89, 87, 97, 98xrlelttrd 12407 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) < +∞)
10085, 87, 99xrltned 41187 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞)
101 ge0xrre 41370 . . . . . . . . . . . . 13 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10284, 100, 101syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ)
10353, 83sge0ge0 42230 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
104 mulge0 11012 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≤ (1 + 𝐸)) ∧ ((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))) → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10545, 51, 102, 103, 104syl22anc 835 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10641, 105eqbrtrd 4990 . . . . . . . . . 10 (𝜑 → (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
10721, 106jca 512 . . . . . . . . 9 (𝜑 → ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
108 oveq1 7030 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (𝑧 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
109108oveq2d 7039 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · ((𝐴𝑍) − (𝐴𝑍))))
110 fveq2 6545 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐴𝑍) → (𝐻𝑧) = (𝐻‘(𝐴𝑍)))
111110fveq1d 6547 . . . . . . . . . . . . . . 15 (𝑧 = (𝐴𝑍) → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))
112111oveq2d 7039 . . . . . . . . . . . . . 14 (𝑧 = (𝐴𝑍) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))
113112mpteq2dv 5063 . . . . . . . . . . . . 13 (𝑧 = (𝐴𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))
114113fveq2d 6549 . . . . . . . . . . . 12 (𝑧 = (𝐴𝑍) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))
115114oveq2d 7039 . . . . . . . . . . 11 (𝑧 = (𝐴𝑍) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗)))))))
116109, 115breq12d 4981 . . . . . . . . . 10 (𝑧 = (𝐴𝑍) → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
117116elrab 3621 . . . . . . . . 9 ((𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ ((𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · ((𝐴𝑍) − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻‘(𝐴𝑍))‘(𝐷𝑗))))))))
118107, 117sylibr 235 . . . . . . . 8 (𝜑 → (𝐴𝑍) ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
119118, 14syl6eleqr 2896 . . . . . . 7 (𝜑 → (𝐴𝑍) ∈ 𝑈)
120 ne0i 4226 . . . . . . 7 ((𝐴𝑍) ∈ 𝑈𝑈 ≠ ∅)
121119, 120syl 17 . . . . . 6 (𝜑𝑈 ≠ ∅)
12211, 13, 17, 121supicc 12740 . . . . 5 (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1232, 122eqeltrd 2885 . . . 4 (𝜑𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
1242oveq1d 7038 . . . . . . 7 (𝜑 → (𝑆 − (𝐴𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴𝑍)))
125124oveq2d 7039 . . . . . 6 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))))
12611, 13iccssred 41343 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,](𝐵𝑍)) ⊆ ℝ)
12717, 126sstrd 3905 . . . . . . . 8 (𝜑𝑈 ⊆ ℝ)
12811, 13jca 512 . . . . . . . . . 10 (𝜑 → ((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ))
129 iccsupr 12684 . . . . . . . . . 10 ((((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐴𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
130128, 17, 119, 129syl3anc 1364 . . . . . . . . 9 (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦))
131130simp3d 1137 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
132 eqid 2797 . . . . . . . 8 {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} = {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
133127, 121, 131, 11, 132supsubc 41183 . . . . . . 7 (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴𝑍)) = sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < ))
134133oveq2d 7039 . . . . . 6 (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )))
13546rexrd 10544 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
136 icogelb 12642 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐺 ∈ (0[,)+∞)) → 0 ≤ 𝐺)
137135, 87, 37, 136syl3anc 1364 . . . . . . 7 (𝜑 → 0 ≤ 𝐺)
138 vex 3443 . . . . . . . . . . . 12 𝑟 ∈ V
139 eqeq1 2801 . . . . . . . . . . . . 13 (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑟 = (𝑢 − (𝐴𝑍))))
140139rexbidv 3262 . . . . . . . . . . . 12 (𝑤 = 𝑟 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍))))
141138, 140elab 3608 . . . . . . . . . . 11 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
142141biimpi 217 . . . . . . . . . 10 (𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
143142adantl 482 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)))
144 nfv 1896 . . . . . . . . . . 11 𝑢𝜑
145 nfcv 2951 . . . . . . . . . . . 12 𝑢𝑟
146 nfre1 3271 . . . . . . . . . . . . 13 𝑢𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))
147146nfab 2957 . . . . . . . . . . . 12 𝑢{𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
148145, 147nfel 2963 . . . . . . . . . . 11 𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
149144, 148nfan 1885 . . . . . . . . . 10 𝑢(𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
150 nfv 1896 . . . . . . . . . 10 𝑢0 ≤ 𝑟
15111rexrd 10544 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴𝑍) ∈ ℝ*)
152151adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ*)
15313rexrd 10544 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑍) ∈ ℝ*)
154153adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ*)
15517sselda 3895 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
156 iccgelb 12647 . . . . . . . . . . . . . . . 16 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → (𝐴𝑍) ≤ 𝑢)
157152, 154, 155, 156syl3anc 1364 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐴𝑍) ≤ 𝑢)
158127sselda 3895 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 𝑢 ∈ ℝ)
15911adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝐴𝑍) ∈ ℝ)
160158, 159subge0d 11084 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (0 ≤ (𝑢 − (𝐴𝑍)) ↔ (𝐴𝑍) ≤ 𝑢))
161157, 160mpbird 258 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → 0 ≤ (𝑢 − (𝐴𝑍)))
1621613adant3 1125 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ (𝑢 − (𝐴𝑍)))
163 id 22 . . . . . . . . . . . . . . 15 (𝑟 = (𝑢 − (𝐴𝑍)) → 𝑟 = (𝑢 − (𝐴𝑍)))
164163eqcomd 2803 . . . . . . . . . . . . . 14 (𝑟 = (𝑢 − (𝐴𝑍)) → (𝑢 − (𝐴𝑍)) = 𝑟)
1651643ad2ant3 1128 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) = 𝑟)
166162, 165breqtrd 4994 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑟 = (𝑢 − (𝐴𝑍))) → 0 ≤ 𝑟)
1671663exp 1112 . . . . . . . . . . 11 (𝜑 → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
168167adantr 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟)))
169149, 150, 168rexlimd 3280 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑟 = (𝑢 − (𝐴𝑍)) → 0 ≤ 𝑟))
170143, 169mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 0 ≤ 𝑟)
171170ralrimiva 3151 . . . . . . 7 (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟)
172 simp3 1131 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 = (𝑢 − (𝐴𝑍)))
173158, 159resubcld 10922 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
1741733adant3 1125 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
175172, 174eqeltrd 2885 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑤 = (𝑢 − (𝐴𝑍))) → 𝑤 ∈ ℝ)
1761753exp 1112 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ)))
177176rexlimdv 3248 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
178177alrimiv 1909 . . . . . . . 8 (𝜑 → ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
179 abss 3967 . . . . . . . 8 ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) → 𝑤 ∈ ℝ))
180178, 179sylibr 235 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ)
18123eqcomd 2803 . . . . . . . . . 10 (𝜑 → 0 = ((𝐴𝑍) − (𝐴𝑍)))
182 oveq1 7030 . . . . . . . . . . 11 (𝑢 = (𝐴𝑍) → (𝑢 − (𝐴𝑍)) = ((𝐴𝑍) − (𝐴𝑍)))
183182rspceeqv 3579 . . . . . . . . . 10 (((𝐴𝑍) ∈ 𝑈 ∧ 0 = ((𝐴𝑍) − (𝐴𝑍))) → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
184119, 181, 183syl2anc 584 . . . . . . . . 9 (𝜑 → ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
185 c0ex 10488 . . . . . . . . . 10 0 ∈ V
186 eqeq1 2801 . . . . . . . . . . 11 (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 0 = (𝑢 − (𝐴𝑍))))
187186rexbidv 3262 . . . . . . . . . 10 (𝑤 = 0 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍))))
188185, 187elab 3608 . . . . . . . . 9 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 0 = (𝑢 − (𝐴𝑍)))
189184, 188sylibr 235 . . . . . . . 8 (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
190 ne0i 4226 . . . . . . . 8 (0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
191189, 190syl 17 . . . . . . 7 (𝜑 → {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅)
19213, 11resubcld 10922 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
193 vex 3443 . . . . . . . . . . . . 13 𝑠 ∈ V
194 eqeq1 2801 . . . . . . . . . . . . . 14 (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑠 = (𝑢 − (𝐴𝑍))))
195194rexbidv 3262 . . . . . . . . . . . . 13 (𝑤 = 𝑠 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍))))
196193, 195elab 3608 . . . . . . . . . . . 12 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
197196biimpi 217 . . . . . . . . . . 11 (𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
198197adantl 482 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)))
199 nfcv 2951 . . . . . . . . . . . . 13 𝑢𝑠
200199, 147nfel 2963 . . . . . . . . . . . 12 𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}
201144, 200nfan 1885 . . . . . . . . . . 11 𝑢(𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))})
202 nfv 1896 . . . . . . . . . . 11 𝑢 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))
203 simp3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 = (𝑢 − (𝐴𝑍)))
2041593adant3 1125 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ℝ)
205133ad2ant1 1126 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐵𝑍) ∈ ℝ)
2061553adant3 1125 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)))
207213ad2ant1 1126 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝐴𝑍) ∈ ((𝐴𝑍)[,](𝐵𝑍)))
208204, 205, 206, 207iccsuble 41358 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
209203, 208eqbrtrd 4990 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑠 = (𝑢 − (𝐴𝑍))) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
2102093exp 1112 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
211210adantr 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑢𝑈 → (𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))))
212201, 202, 211rexlimd 3280 . . . . . . . . . 10 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑠 = (𝑢 − (𝐴𝑍)) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))))
213198, 212mpd 15 . . . . . . . . 9 ((𝜑𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → 𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
214213ralrimiva 3151 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍)))
215 brralrspcev 5028 . . . . . . . 8 ((((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠 ≤ ((𝐵𝑍) − (𝐴𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
216192, 214, 215syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)
217 eqid 2797 . . . . . . . 8 {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
218 biid 262 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)))
219217, 218supmul1 11464 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑠𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
22038, 137, 171, 180, 191, 216, 219syl33anc 1378 . . . . . 6 (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
221125, 134, 2203eqtrd 2837 . . . . 5 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ))
222 vex 3443 . . . . . . . . . . . 12 𝑐 ∈ V
223 eqeq1 2801 . . . . . . . . . . . . 13 (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡)))
224223rexbidv 3262 . . . . . . . . . . . 12 (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡)))
225222, 224elab 3608 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
226225biimpi 217 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
227 nfv 1896 . . . . . . . . . . . 12 𝑡𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))
228 vex 3443 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
229 eqeq1 2801 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴𝑍)) ↔ 𝑡 = (𝑢 − (𝐴𝑍))))
230229rexbidv 3262 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍)) ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍))))
231228, 230elab 3608 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ↔ ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
232231biimpi 217 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
233232adantr 481 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
234 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · 𝑡))
235 oveq2 7031 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝑢 − (𝐴𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
236235adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴𝑍))))
237234, 236eqtrd 2833 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
238237ex 413 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
239238reximdv 3238 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 · 𝑡) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
240239adantl 482 . . . . . . . . . . . . . 14 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
241233, 240mpd 15 . . . . . . . . . . . . 13 ((𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
242241ex 413 . . . . . . . . . . . 12 (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
243227, 242rexlimi 3278 . . . . . . . . . . 11 (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
244243a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))))
245226, 244mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
246245adantl 482 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
247 simp3 1131 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))))
24838adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 𝐺 ∈ ℝ)
249248, 173remulcld 10524 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ∈ ℝ)
25045adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (1 + 𝐸) ∈ ℝ)
25152a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → ℕ ∈ V)
25260adantlr 711 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
25364adantlr 711 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶𝑗):𝑊⟶ℝ)
254158adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ)
25579adantlr 711 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷𝑗):𝑊⟶ℝ)
25674, 254, 252, 255hsphoif 42422 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻𝑢)‘(𝐷𝑗)):𝑊⟶ℝ)
25727, 252, 253, 256hoidmvcl 42428 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,)+∞))
25854, 257sseldi 3893 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ∈ (0[,]+∞))
259258fmpttd 6749 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))):ℕ⟶(0[,]+∞))
260251, 259sge0cl 42227 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞))
261251, 259sge0xrcl 42231 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ*)
26286a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → +∞ ∈ ℝ*)
26389adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) ∈ ℝ*)
264 nfv 1896 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑢𝑈)
26592adantlr 711 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)) ∈ (0[,]+∞))
26695adantlr 711 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊𝑌))
26727, 252, 266, 9, 254, 74, 253, 255hsphoidmvle 42432 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))
268264, 251, 258, 265, 267sge0lempt 42256 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))))
26998adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)(𝐷𝑗)))) < +∞)
270261, 263, 262, 268, 269xrlelttrd 12407 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) < +∞)
271261, 262, 270xrltned 41187 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞)
272 ge0xrre 41370 . . . . . . . . . . . . . . . 16 (((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ (0[,]+∞) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≠ +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
273260, 271, 272syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ∈ ℝ)
274250, 273remulcld 10524 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ∈ ℝ)
275126, 123sseldd 3896 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ ℝ)
27627, 30, 94, 9, 61, 76, 88, 65, 275sge0hsphoire 42435 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
27745, 276remulcld 10524 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
278277adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ)
27914eleq2i 2876 . . . . . . . . . . . . . . . . . 18 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
280279biimpi 217 . . . . . . . . . . . . . . . . 17 (𝑢𝑈𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
281 oveq1 7030 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (𝑧 − (𝐴𝑍)) = (𝑢 − (𝐴𝑍)))
282281oveq2d 7039 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑢 − (𝐴𝑍))))
283 fveq2 6545 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑢 → (𝐻𝑧) = (𝐻𝑢))
284283fveq1d 6547 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑢 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑢)‘(𝐷𝑗)))
285284oveq2d 7039 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑢 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))
286285mpteq2dv 5063 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))
287286fveq2d 6549 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))
288287oveq2d 7039 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑢 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
289282, 288breq12d 4981 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
290289elrab 3621 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
291280, 290sylib 219 . . . . . . . . . . . . . . . 16 (𝑢𝑈 → (𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))))))
292291simprd 496 . . . . . . . . . . . . . . 15 (𝑢𝑈 → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
293292adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))))
294276adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))) ∈ ℝ)
29551adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → 0 ≤ (1 + 𝐸))
296275adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
29774, 296, 60, 79hsphoif 42422 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑆)‘(𝐷𝑗)):𝑊⟶ℝ)
29827, 60, 64, 297hoidmvcl 42428 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,)+∞))
29954, 298sseldi 3893 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
300299adantlr 711 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))) ∈ (0[,]+∞))
301296adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
302127adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ⊆ ℝ)
303121adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑈 ≠ ∅)
304131adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦)
305 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈) → 𝑢𝑈)
306 suprub 11456 . . . . . . . . . . . . . . . . . . . 20 (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧𝑈 𝑧𝑦) ∧ 𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
307302, 303, 304, 305, 306syl31anc 1366 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < ))
308307, 1syl6breqr 5010 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑈) → 𝑢𝑆)
309308adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢𝑆)
31027, 252, 266, 9, 254, 301, 309, 74, 253, 255hsphoidmvle2 42431 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))) ≤ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
311264, 251, 258, 300, 310sge0lempt 42256 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗))))) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
312273, 294, 250, 295, 311lemul2ad 11434 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈) → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑢)‘(𝐷𝑗)))))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
313249, 274, 278, 293, 312letrd 10650 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3143133adant3 1125 . . . . . . . . . . . 12 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
315247, 314eqbrtrd 4990 . . . . . . . . . . 11 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
3163153exp 1112 . . . . . . . . . 10 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))))
317316rexlimdv 3248 . . . . . . . . 9 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
318317adantr 481 . . . . . . . 8 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
319246, 318mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
320319ralrimiva 3151 . . . . . 6 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
321226adantl 482 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡))
322 nfv 1896 . . . . . . . . . . . 12 𝑡𝜑
323 nfcv 2951 . . . . . . . . . . . . 13 𝑡𝑐
324 nfre1 3271 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)
325324nfab 2957 . . . . . . . . . . . . 13 𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
326323, 325nfel 2963 . . . . . . . . . . . 12 𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}
327322, 326nfan 1885 . . . . . . . . . . 11 𝑡(𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
328 nfv 1896 . . . . . . . . . . 11 𝑡 𝑐 ∈ ℝ
329232adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → ∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)))
330 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡))
3312483adant3 1125 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝐺 ∈ ℝ)
332 simp3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 = (𝑢 − (𝐴𝑍)))
3331733adant3 1125 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑢 − (𝐴𝑍)) ∈ ℝ)
334332, 333eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → 𝑡 ∈ ℝ)
335331, 334remulcld 10524 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝐺 · 𝑡) ∈ ℝ)
336335adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ)
337330, 336eqeltrd 2885 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ)
338337ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈𝑡 = (𝑢 − (𝐴𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
3393383exp 1112 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑢𝑈 → (𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))))
340339rexlimdv 3248 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
341340adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (∃𝑢𝑈 𝑡 = (𝑢 − (𝐴𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
342329, 341mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
343342ex 413 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
344343adantr 481 . . . . . . . . . . 11 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))
345327, 328, 344rexlimd 3280 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))
346321, 345mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ)
347346ralrimiva 3151 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
348 dfss3 3884 . . . . . . . 8 ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ)
349347, 348sylibr 235 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ)
35040eqcomd 2803 . . . . . . . . . 10 (𝜑 → 0 = (𝐺 · 0))
351 oveq2 7031 . . . . . . . . . . 11 (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0))
352351rspceeqv 3579 . . . . . . . . . 10 ((0 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
353189, 350, 352syl2anc 584 . . . . . . . . 9 (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
354 eqeq1 2801 . . . . . . . . . . 11 (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡)))
355354rexbidv 3262 . . . . . . . . . 10 (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡)))
356185, 355elab 3608 . . . . . . . . 9 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}0 = (𝐺 · 𝑡))
357353, 356sylibr 235 . . . . . . . 8 (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)})
358 ne0i 4226 . . . . . . . 8 (0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
359357, 358syl 17 . . . . . . 7 (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅)
36038, 192remulcld 10524 . . . . . . . 8 (𝜑 → (𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ)
361192adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
362137adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → 0 ≤ 𝐺)
36313adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → (𝐵𝑍) ∈ ℝ)
364 iccleub 12646 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑍) ∈ ℝ* ∧ (𝐵𝑍) ∈ ℝ*𝑢 ∈ ((𝐴𝑍)[,](𝐵𝑍))) → 𝑢 ≤ (𝐵𝑍))
365152, 154, 155, 364syl3anc 1364 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑈) → 𝑢 ≤ (𝐵𝑍))
366158, 363, 159, 365lesub1dd 11110 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑈) → (𝑢 − (𝐴𝑍)) ≤ ((𝐵𝑍) − (𝐴𝑍)))
367173, 361, 248, 362, 366lemul2ad 11434 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑈) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3683673adant3 1125 . . . . . . . . . . . . . 14 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → (𝐺 · (𝑢 − (𝐴𝑍))) ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
369247, 368eqbrtrd 4990 . . . . . . . . . . . . 13 ((𝜑𝑢𝑈𝑐 = (𝐺 · (𝑢 − (𝐴𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
3703693exp 1112 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))))
371370rexlimdv 3248 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
372371adantr 481 . . . . . . . . . 10 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))))
373246, 372mpd 15 . . . . . . . . 9 ((𝜑𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
374373ralrimiva 3151 . . . . . . . 8 (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍))))
375 brralrspcev 5028 . . . . . . . 8 (((𝐺 · ((𝐵𝑍) − (𝐴𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵𝑍) − (𝐴𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
376360, 374, 375syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦)
377 suprleub 11461 . . . . . . 7 ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐𝑦) ∧ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
378349, 359, 376, 277, 377syl31anc 1366 . . . . . 6 (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
379320, 378mpbird 258 . . . . 5 (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢𝑈 𝑤 = (𝑢 − (𝐴𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
380221, 379eqbrtrd 4990 . . . 4 (𝜑 → (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
381123, 380jca 512 . . 3 (𝜑 → (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
382 oveq1 7030 . . . . . 6 (𝑧 = 𝑆 → (𝑧 − (𝐴𝑍)) = (𝑆 − (𝐴𝑍)))
383382oveq2d 7039 . . . . 5 (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴𝑍))) = (𝐺 · (𝑆 − (𝐴𝑍))))
384 fveq2 6545 . . . . . . . . . 10 (𝑧 = 𝑆 → (𝐻𝑧) = (𝐻𝑆))
385384fveq1d 6547 . . . . . . . . 9 (𝑧 = 𝑆 → ((𝐻𝑧)‘(𝐷𝑗)) = ((𝐻𝑆)‘(𝐷𝑗)))
386385oveq2d 7039 . . . . . . . 8 (𝑧 = 𝑆 → ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))) = ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))
387386mpteq2dv 5063 . . . . . . 7 (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))
388387fveq2d 6549 . . . . . 6 (𝑧 = 𝑆 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))) = (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))
389388oveq2d 7039 . . . . 5 (𝑧 = 𝑆 → ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) = ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗)))))))
390383, 389breq12d 4981 . . . 4 (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
391390elrab 3621 . . 3 (𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))} ↔ (𝑆 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∧ (𝐺 · (𝑆 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑆)‘(𝐷𝑗))))))))
392381, 391sylibr 235 . 2 (𝜑𝑆 ∈ {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝐺 · (𝑧 − (𝐴𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑊)((𝐻𝑧)‘(𝐷𝑗))))))})
393392, 14syl6eleqr 2896 1 (𝜑𝑆𝑈)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∀wal 1523   = wceq 1525   ∈ wcel 2083  {cab 2777   ≠ wne 2986  ∀wral 3107  ∃wrex 3108  {crab 3111  Vcvv 3440   ∖ cdif 3862   ∪ cun 3863   ⊆ wss 3865  ∅c0 4217  ifcif 4387  {csn 4478   class class class wbr 4968   ↦ cmpt 5047   ↾ cres 5452  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023   ∈ cmpo 7025   ↑𝑚 cmap 8263  Fincfn 8364  supcsup 8757  ℝcr 10389  0cc0 10390  1c1 10391   + caddc 10393   · cmul 10395  +∞cpnf 10525  ℝ*cxr 10527   < clt 10528   ≤ cle 10529   − cmin 10723  ℕcn 11492  ℝ+crp 12243  [,)cico 12594  [,]cicc 12595  ∏cprod 15096  volcvol 23751  Σ^csumge0 42208 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fi 8728  df-sup 8759  df-inf 8760  df-oi 8827  df-dju 9183  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-n0 11752  df-z 11836  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-ico 12598  df-icc 12599  df-fz 12747  df-fzo 12888  df-fl 13016  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-rlim 14684  df-sum 14881  df-prod 15097  df-rest 16529  df-topgen 16550  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-top 21190  df-topon 21207  df-bases 21242  df-cmp 21683  df-ovol 23752  df-vol 23753  df-sumge0 42209 This theorem is referenced by:  hoidmvlelem4  42444
 Copyright terms: Public domain W3C validator