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 44737
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 4618 . . . . . . . . . 10 (𝑍 ∈ (𝑋 βˆ– π‘Œ) β†’ 𝑍 ∈ {𝑍})
64, 5syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑍 ∈ {𝑍})
7 elun2 4135 . . . . . . . . 9 (𝑍 ∈ {𝑍} β†’ 𝑍 ∈ (π‘Œ βˆͺ {𝑍}))
86, 7syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ (π‘Œ βˆͺ {𝑍}))
9 hoidmvlelem1.w . . . . . . . 8 π‘Š = (π‘Œ βˆͺ {𝑍})
108, 9eleqtrrdi 2849 . . . . . . 7 (πœ‘ β†’ 𝑍 ∈ π‘Š)
113, 10ffvelcdmd 7032 . . . . . 6 (πœ‘ β†’ (π΄β€˜π‘) ∈ ℝ)
12 hoidmvlelem1.b . . . . . . 7 (πœ‘ β†’ 𝐡:π‘ŠβŸΆβ„)
1312, 10ffvelcdmd 7032 . . . . . 6 (πœ‘ β†’ (π΅β€˜π‘) ∈ ℝ)
14 hoidmvlelem1.u . . . . . . . 8 π‘ˆ = {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))}
15 ssrab2 4035 . . . . . . . 8 {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))} βŠ† ((π΄β€˜π‘)[,](π΅β€˜π‘))
1614, 15eqsstri 3976 . . . . . . 7 π‘ˆ βŠ† ((π΄β€˜π‘)[,](π΅β€˜π‘))
1716a1i 11 . . . . . 6 (πœ‘ β†’ π‘ˆ βŠ† ((π΄β€˜π‘)[,](π΅β€˜π‘)))
1811leidd 11679 . . . . . . . . . . 11 (πœ‘ β†’ (π΄β€˜π‘) ≀ (π΄β€˜π‘))
19 hoidmvlelem1.ab . . . . . . . . . . . 12 (πœ‘ β†’ (π΄β€˜π‘) < (π΅β€˜π‘))
2011, 13, 19ltled 11261 . . . . . . . . . . 11 (πœ‘ β†’ (π΄β€˜π‘) ≀ (π΅β€˜π‘))
2111, 13, 11, 18, 20eliccd 43643 . . . . . . . . . 10 (πœ‘ β†’ (π΄β€˜π‘) ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
2211recnd 11141 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π΄β€˜π‘) ∈ β„‚)
2322subidd 11458 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘)) = 0)
2423oveq2d 7367 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) = (𝐺 Β· 0))
25 rge0ssre 13327 . . . . . . . . . . . . . . 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 9169 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Œ ∈ Fin)
31 ssun1 4130 . . . . . . . . . . . . . . . . . . . 20 π‘Œ βŠ† (π‘Œ βˆͺ {𝑍})
3231, 9sseqtrri 3979 . . . . . . . . . . . . . . . . . . 19 π‘Œ βŠ† π‘Š
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘Œ βŠ† π‘Š)
343, 33fssresd 6706 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 β†Ύ π‘Œ):π‘ŒβŸΆβ„)
3512, 33fssresd 6706 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 β†Ύ π‘Œ):π‘ŒβŸΆβ„)
3627, 30, 34, 35hoidmvcl 44724 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝐴 β†Ύ π‘Œ)(πΏβ€˜π‘Œ)(𝐡 β†Ύ π‘Œ)) ∈ (0[,)+∞))
3726, 36eqeltrid 2842 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐺 ∈ (0[,)+∞))
3825, 37sselid 3940 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺 ∈ ℝ)
3938recnd 11141 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐺 ∈ β„‚)
4039mul01d 11312 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐺 Β· 0) = 0)
4124, 40eqtrd 2777 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) = 0)
42 1red 11114 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ ℝ)
43 hoidmvlelem1.e . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐸 ∈ ℝ+)
4443rpred 12911 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐸 ∈ ℝ)
4542, 44readdcld 11142 . . . . . . . . . . . 12 (πœ‘ β†’ (1 + 𝐸) ∈ ℝ)
46 0red 11116 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ ℝ)
47 0lt1 11635 . . . . . . . . . . . . . . 15 0 < 1
4847a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < 1)
4942, 43ltaddrpd 12944 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 < (1 + 𝐸))
5046, 42, 45, 48, 49lttrd 11274 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < (1 + 𝐸))
5146, 45, 50ltled 11261 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ≀ (1 + 𝐸))
52 nnex 12117 . . . . . . . . . . . . . . 15 β„• ∈ V
5352a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ β„• ∈ V)
54 icossicc 13307 . . . . . . . . . . . . . . . 16 (0[,)+∞) βŠ† (0[,]+∞)
55 snfi 8946 . . . . . . . . . . . . . . . . . . . . 21 {𝑍} ∈ Fin
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ {𝑍} ∈ Fin)
57 unfi 9074 . . . . . . . . . . . . . . . . . . . 20 ((π‘Œ ∈ Fin ∧ {𝑍} ∈ Fin) β†’ (π‘Œ βˆͺ {𝑍}) ∈ Fin)
5830, 56, 57syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘Œ βˆͺ {𝑍}) ∈ Fin)
599, 58eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘Š ∈ Fin)
6059adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ π‘Š ∈ Fin)
61 hoidmvlelem1.c . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐢:β„•βŸΆ(ℝ ↑m π‘Š))
6261ffvelcdmda 7031 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—) ∈ (ℝ ↑m π‘Š))
63 elmapi 8745 . . . . . . . . . . . . . . . . . 18 ((πΆβ€˜π‘—) ∈ (ℝ ↑m π‘Š) β†’ (πΆβ€˜π‘—):π‘ŠβŸΆβ„)
6462, 63syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—):π‘ŠβŸΆβ„)
65 hoidmvlelem1.h . . . . . . . . . . . . . . . . . . 19 𝐻 = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (𝑗 ∈ π‘Š ↦ if(𝑗 ∈ π‘Œ, (π‘β€˜π‘—), if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯)))))
66 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = β„Ž β†’ (𝑗 ∈ π‘Œ ↔ β„Ž ∈ π‘Œ))
67 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = β„Ž β†’ (π‘β€˜π‘—) = (π‘β€˜β„Ž))
6867breq1d 5113 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = β„Ž β†’ ((π‘β€˜π‘—) ≀ π‘₯ ↔ (π‘β€˜β„Ž) ≀ π‘₯))
6968, 67ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = β„Ž β†’ if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯) = if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯))
7066, 67, 69ifbieq12d 4512 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = β„Ž β†’ if(𝑗 ∈ π‘Œ, (π‘β€˜π‘—), if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯)) = if(β„Ž ∈ π‘Œ, (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯)))
7170cbvmptv 5216 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ π‘Š ↦ if(𝑗 ∈ π‘Œ, (π‘β€˜π‘—), if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯))) = (β„Ž ∈ π‘Š ↦ if(β„Ž ∈ π‘Œ, (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯)))
7271mpteq2i 5208 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (𝑗 ∈ π‘Š ↦ if(𝑗 ∈ π‘Œ, (π‘β€˜π‘—), if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯)))) = (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (β„Ž ∈ π‘Š ↦ if(β„Ž ∈ π‘Œ, (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯))))
7372mpteq2i 5208 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (𝑗 ∈ π‘Š ↦ if(𝑗 ∈ π‘Œ, (π‘β€˜π‘—), if((π‘β€˜π‘—) ≀ π‘₯, (π‘β€˜π‘—), π‘₯))))) = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (β„Ž ∈ π‘Š ↦ if(β„Ž ∈ π‘Œ, (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯)))))
7465, 73eqtri 2765 . . . . . . . . . . . . . . . . . 18 𝐻 = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m π‘Š) ↦ (β„Ž ∈ π‘Š ↦ if(β„Ž ∈ π‘Œ, (π‘β€˜β„Ž), if((π‘β€˜β„Ž) ≀ π‘₯, (π‘β€˜β„Ž), π‘₯)))))
7511adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π΄β€˜π‘) ∈ ℝ)
76 hoidmvlelem1.d . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐷:β„•βŸΆ(ℝ ↑m π‘Š))
7776ffvelcdmda 7031 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—) ∈ (ℝ ↑m π‘Š))
78 elmapi 8745 . . . . . . . . . . . . . . . . . . 19 ((π·β€˜π‘—) ∈ (ℝ ↑m π‘Š) β†’ (π·β€˜π‘—):π‘ŠβŸΆβ„)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):π‘ŠβŸΆβ„)
8074, 75, 60, 79hsphoif 44718 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)):π‘ŠβŸΆβ„)
8127, 60, 64, 80hoidmvcl 44724 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))) ∈ (0[,)+∞))
8254, 81sselid 3940 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
8382fmpttd 7059 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))):β„•βŸΆ(0[,]+∞))
8453, 83sge0cl 44523 . . . . . . . . . . . . 13 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞))
8553, 83sge0xrcl 44527 . . . . . . . . . . . . . 14 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ ℝ*)
86 pnfxr 11167 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ +∞ ∈ ℝ*)
88 hoidmvlelem1.r . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))) ∈ ℝ)
8988rexrd 11163 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))) ∈ ℝ*)
90 nfv 1917 . . . . . . . . . . . . . . . 16 β„²π‘—πœ‘
9127, 60, 64, 79hoidmvcl 44724 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)) ∈ (0[,)+∞))
9254, 91sselid 3940 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)) ∈ (0[,]+∞))
934eldifbd 3921 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Β¬ 𝑍 ∈ π‘Œ)
9410, 93eldifd 3919 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑍 ∈ (π‘Š βˆ– π‘Œ))
9594adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑍 ∈ (π‘Š βˆ– π‘Œ))
9627, 60, 95, 9, 75, 74, 64, 79hsphoidmvle 44728 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))
9790, 53, 82, 92, 96sge0lempt 44552 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))))
9888ltpnfd 12996 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))) < +∞)
9985, 89, 87, 97, 98xrlelttrd 13033 . . . . . . . . . . . . . 14 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) < +∞)
10085, 87, 99xrltned 43496 . . . . . . . . . . . . 13 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) β‰  +∞)
101 ge0xrre 43670 . . . . . . . . . . . . 13 (((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) β‰  +∞) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ ℝ)
10284, 100, 101syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ ℝ)
10353, 83sge0ge0 44526 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))
104 mulge0 11631 . . . . . . . . . . . 12 ((((1 + 𝐸) ∈ ℝ ∧ 0 ≀ (1 + 𝐸)) ∧ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))) ∈ ℝ ∧ 0 ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))) β†’ 0 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))))))
10545, 51, 102, 103, 104syl22anc 837 . . . . . . . . . . 11 (πœ‘ β†’ 0 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))))))
10641, 105eqbrtrd 5125 . . . . . . . . . 10 (πœ‘ β†’ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))))))
10721, 106jca 512 . . . . . . . . 9 (πœ‘ β†’ ((π΄β€˜π‘) ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))))
108 oveq1 7358 . . . . . . . . . . . 12 (𝑧 = (π΄β€˜π‘) β†’ (𝑧 βˆ’ (π΄β€˜π‘)) = ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘)))
109108oveq2d 7367 . . . . . . . . . . 11 (𝑧 = (π΄β€˜π‘) β†’ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) = (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))))
110 fveq2 6839 . . . . . . . . . . . . . . . 16 (𝑧 = (π΄β€˜π‘) β†’ (π»β€˜π‘§) = (π»β€˜(π΄β€˜π‘)))
111110fveq1d 6841 . . . . . . . . . . . . . . 15 (𝑧 = (π΄β€˜π‘) β†’ ((π»β€˜π‘§)β€˜(π·β€˜π‘—)) = ((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))
112111oveq2d 7367 . . . . . . . . . . . . . 14 (𝑧 = (π΄β€˜π‘) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))
113112mpteq2dv 5205 . . . . . . . . . . . . 13 (𝑧 = (π΄β€˜π‘) β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))) = (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))))
114113fveq2d 6843 . . . . . . . . . . . 12 (𝑧 = (π΄β€˜π‘) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))
115114oveq2d 7367 . . . . . . . . . . 11 (𝑧 = (π΄β€˜π‘) β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) = ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—)))))))
116109, 115breq12d 5116 . . . . . . . . . 10 (𝑧 = (π΄β€˜π‘) β†’ ((𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) ↔ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))))
117116elrab 3643 . . . . . . . . 9 ((π΄β€˜π‘) ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))} ↔ ((π΄β€˜π‘) ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜(π΄β€˜π‘))β€˜(π·β€˜π‘—))))))))
118107, 117sylibr 233 . . . . . . . 8 (πœ‘ β†’ (π΄β€˜π‘) ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))})
119118, 14eleqtrrdi 2849 . . . . . . 7 (πœ‘ β†’ (π΄β€˜π‘) ∈ π‘ˆ)
120 ne0i 4292 . . . . . . 7 ((π΄β€˜π‘) ∈ π‘ˆ β†’ π‘ˆ β‰  βˆ…)
121119, 120syl 17 . . . . . 6 (πœ‘ β†’ π‘ˆ β‰  βˆ…)
12211, 13, 17, 121supicc 13372 . . . . 5 (πœ‘ β†’ sup(π‘ˆ, ℝ, < ) ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
1232, 122eqeltrd 2838 . . . 4 (πœ‘ β†’ 𝑆 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
1242oveq1d 7366 . . . . . . 7 (πœ‘ β†’ (𝑆 βˆ’ (π΄β€˜π‘)) = (sup(π‘ˆ, ℝ, < ) βˆ’ (π΄β€˜π‘)))
125124oveq2d 7367 . . . . . 6 (πœ‘ β†’ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) = (𝐺 Β· (sup(π‘ˆ, ℝ, < ) βˆ’ (π΄β€˜π‘))))
12611, 13iccssred 13305 . . . . . . . . 9 (πœ‘ β†’ ((π΄β€˜π‘)[,](π΅β€˜π‘)) βŠ† ℝ)
12717, 126sstrd 3952 . . . . . . . 8 (πœ‘ β†’ π‘ˆ βŠ† ℝ)
12811, 13jca 512 . . . . . . . . . 10 (πœ‘ β†’ ((π΄β€˜π‘) ∈ ℝ ∧ (π΅β€˜π‘) ∈ ℝ))
129 iccsupr 13313 . . . . . . . . . 10 ((((π΄β€˜π‘) ∈ ℝ ∧ (π΅β€˜π‘) ∈ ℝ) ∧ π‘ˆ βŠ† ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (π΄β€˜π‘) ∈ π‘ˆ) β†’ (π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ π‘ˆ 𝑧 ≀ 𝑦))
130128, 17, 119, 129syl3anc 1371 . . . . . . . . 9 (πœ‘ β†’ (π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ π‘ˆ 𝑧 ≀ 𝑦))
131130simp3d 1144 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ π‘ˆ 𝑧 ≀ 𝑦)
132 eqid 2737 . . . . . . . 8 {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} = {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}
133127, 121, 131, 11, 132supsubc 43492 . . . . . . 7 (πœ‘ β†’ (sup(π‘ˆ, ℝ, < ) βˆ’ (π΄β€˜π‘)) = sup({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}, ℝ, < ))
134133oveq2d 7367 . . . . . 6 (πœ‘ β†’ (𝐺 Β· (sup(π‘ˆ, ℝ, < ) βˆ’ (π΄β€˜π‘))) = (𝐺 Β· sup({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}, ℝ, < )))
13546rexrd 11163 . . . . . . . 8 (πœ‘ β†’ 0 ∈ ℝ*)
136 icogelb 13269 . . . . . . . 8 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐺 ∈ (0[,)+∞)) β†’ 0 ≀ 𝐺)
137135, 87, 37, 136syl3anc 1371 . . . . . . 7 (πœ‘ β†’ 0 ≀ 𝐺)
138 vex 3447 . . . . . . . . . . . 12 π‘Ÿ ∈ V
139 eqeq1 2741 . . . . . . . . . . . . 13 (𝑀 = π‘Ÿ β†’ (𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘))))
140139rexbidv 3173 . . . . . . . . . . . 12 (𝑀 = π‘Ÿ β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ βˆƒπ‘’ ∈ π‘ˆ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘))))
141138, 140elab 3628 . . . . . . . . . . 11 (π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ↔ βˆƒπ‘’ ∈ π‘ˆ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)))
142141biimpi 215 . . . . . . . . . 10 (π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ βˆƒπ‘’ ∈ π‘ˆ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)))
143142adantl 482 . . . . . . . . 9 ((πœ‘ ∧ π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ βˆƒπ‘’ ∈ π‘ˆ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)))
144 nfv 1917 . . . . . . . . . . 11 β„²π‘’πœ‘
145 nfcv 2905 . . . . . . . . . . . 12 β„²π‘’π‘Ÿ
146 nfre1 3266 . . . . . . . . . . . . 13 β„²π‘’βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))
147146nfab 2911 . . . . . . . . . . . 12 Ⅎ𝑒{𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}
148145, 147nfel 2919 . . . . . . . . . . 11 Ⅎ𝑒 π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}
149144, 148nfan 1902 . . . . . . . . . 10 Ⅎ𝑒(πœ‘ ∧ π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))})
150 nfv 1917 . . . . . . . . . 10 Ⅎ𝑒0 ≀ π‘Ÿ
15111rexrd 11163 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π΄β€˜π‘) ∈ ℝ*)
152151adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π΄β€˜π‘) ∈ ℝ*)
15313rexrd 11163 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π΅β€˜π‘) ∈ ℝ*)
154153adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π΅β€˜π‘) ∈ ℝ*)
15517sselda 3942 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
156 iccgelb 13274 . . . . . . . . . . . . . . . 16 (((π΄β€˜π‘) ∈ ℝ* ∧ (π΅β€˜π‘) ∈ ℝ* ∧ 𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘))) β†’ (π΄β€˜π‘) ≀ 𝑒)
157152, 154, 155, 156syl3anc 1371 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π΄β€˜π‘) ≀ 𝑒)
158127sselda 3942 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ ℝ)
15911adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π΄β€˜π‘) ∈ ℝ)
160158, 159subge0d 11703 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (0 ≀ (𝑒 βˆ’ (π΄β€˜π‘)) ↔ (π΄β€˜π‘) ≀ 𝑒))
161157, 160mpbird 256 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 0 ≀ (𝑒 βˆ’ (π΄β€˜π‘)))
1621613adant3 1132 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 0 ≀ (𝑒 βˆ’ (π΄β€˜π‘)))
163 id 22 . . . . . . . . . . . . . . 15 (π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)))
164163eqcomd 2743 . . . . . . . . . . . . . 14 (π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) = π‘Ÿ)
1651643ad2ant3 1135 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) = π‘Ÿ)
166162, 165breqtrd 5129 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 0 ≀ π‘Ÿ)
1671663exp 1119 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 0 ≀ π‘Ÿ)))
168167adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (𝑒 ∈ π‘ˆ β†’ (π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 0 ≀ π‘Ÿ)))
169149, 150, 168rexlimd 3247 . . . . . . . . 9 ((πœ‘ ∧ π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (βˆƒπ‘’ ∈ π‘ˆ π‘Ÿ = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 0 ≀ π‘Ÿ))
170143, 169mpd 15 . . . . . . . 8 ((πœ‘ ∧ π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ 0 ≀ π‘Ÿ)
171170ralrimiva 3141 . . . . . . 7 (πœ‘ β†’ βˆ€π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 ≀ π‘Ÿ)
172 simp3 1138 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)))
173158, 159resubcld 11541 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) ∈ ℝ)
1741733adant3 1132 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) ∈ ℝ)
175172, 174eqeltrd 2838 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑀 ∈ ℝ)
1761753exp 1119 . . . . . . . . . 10 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑀 ∈ ℝ)))
177176rexlimdv 3148 . . . . . . . . 9 (πœ‘ β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑀 ∈ ℝ))
178177alrimiv 1930 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘€(βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑀 ∈ ℝ))
179 abss 4015 . . . . . . . 8 ({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} βŠ† ℝ ↔ βˆ€π‘€(βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑀 ∈ ℝ))
180178, 179sylibr 233 . . . . . . 7 (πœ‘ β†’ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} βŠ† ℝ)
18123eqcomd 2743 . . . . . . . . . 10 (πœ‘ β†’ 0 = ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘)))
182 oveq1 7358 . . . . . . . . . . 11 (𝑒 = (π΄β€˜π‘) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) = ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘)))
183182rspceeqv 3593 . . . . . . . . . 10 (((π΄β€˜π‘) ∈ π‘ˆ ∧ 0 = ((π΄β€˜π‘) βˆ’ (π΄β€˜π‘))) β†’ βˆƒπ‘’ ∈ π‘ˆ 0 = (𝑒 βˆ’ (π΄β€˜π‘)))
184119, 181, 183syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘’ ∈ π‘ˆ 0 = (𝑒 βˆ’ (π΄β€˜π‘)))
185 eqeq1 2741 . . . . . . . . . 10 (𝑀 = 0 β†’ (𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ 0 = (𝑒 βˆ’ (π΄β€˜π‘))))
186185rexbidv 3173 . . . . . . . . 9 (𝑀 = 0 β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ βˆƒπ‘’ ∈ π‘ˆ 0 = (𝑒 βˆ’ (π΄β€˜π‘))))
18746, 184, 186elabd 3631 . . . . . . . 8 (πœ‘ β†’ 0 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))})
188 ne0i 4292 . . . . . . . 8 (0 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β‰  βˆ…)
189187, 188syl 17 . . . . . . 7 (πœ‘ β†’ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β‰  βˆ…)
19013, 11resubcld 11541 . . . . . . . 8 (πœ‘ β†’ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)) ∈ ℝ)
191 vex 3447 . . . . . . . . . . . . 13 𝑠 ∈ V
192 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑀 = 𝑠 β†’ (𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))))
193192rexbidv 3173 . . . . . . . . . . . . 13 (𝑀 = 𝑠 β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))))
194191, 193elab 3628 . . . . . . . . . . . 12 (𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)))
195194biimpi 215 . . . . . . . . . . 11 (𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)))
196195adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)))
197 nfcv 2905 . . . . . . . . . . . . 13 Ⅎ𝑒𝑠
198197, 147nfel 2919 . . . . . . . . . . . 12 Ⅎ𝑒 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}
199144, 198nfan 1902 . . . . . . . . . . 11 Ⅎ𝑒(πœ‘ ∧ 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))})
200 nfv 1917 . . . . . . . . . . 11 Ⅎ𝑒 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))
201 simp3 1138 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)))
2021593adant3 1132 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (π΄β€˜π‘) ∈ ℝ)
203133ad2ant1 1133 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (π΅β€˜π‘) ∈ ℝ)
2041553adant3 1132 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
205213ad2ant1 1133 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (π΄β€˜π‘) ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)))
206202, 203, 204, 205iccsuble 43658 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))
207201, 206eqbrtrd 5125 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))
2082073exp 1119 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))))
209208adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (𝑒 ∈ π‘ˆ β†’ (𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))))
210199, 200, 209rexlimd 3247 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑠 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
211196, 210mpd 15 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ 𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))
212211ralrimiva 3141 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))
213 brralrspcev 5163 . . . . . . . 8 ((((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)) ∈ ℝ ∧ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))) β†’ βˆƒπ‘Ÿ ∈ ℝ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ π‘Ÿ)
214190, 212, 213syl2anc 584 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘Ÿ ∈ ℝ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ π‘Ÿ)
215 eqid 2737 . . . . . . . 8 {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} = {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}
216 biid 260 . . . . . . . 8 (((𝐺 ∈ ℝ ∧ 0 ≀ 𝐺 ∧ βˆ€π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 ≀ π‘Ÿ) ∧ ({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} βŠ† ℝ ∧ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β‰  βˆ… ∧ βˆƒπ‘Ÿ ∈ ℝ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ π‘Ÿ)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≀ 𝐺 ∧ βˆ€π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 ≀ π‘Ÿ) ∧ ({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} βŠ† ℝ ∧ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β‰  βˆ… ∧ βˆƒπ‘Ÿ ∈ ℝ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ π‘Ÿ)))
217215, 216supmul1 12082 . . . . . . 7 (((𝐺 ∈ ℝ ∧ 0 ≀ 𝐺 ∧ βˆ€π‘Ÿ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 ≀ π‘Ÿ) ∧ ({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} βŠ† ℝ ∧ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β‰  βˆ… ∧ βˆƒπ‘Ÿ ∈ ℝ βˆ€π‘  ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑠 ≀ π‘Ÿ)) β†’ (𝐺 Β· sup({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}, ℝ, < )) = sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ))
21838, 137, 171, 180, 189, 214, 217syl33anc 1385 . . . . . 6 (πœ‘ β†’ (𝐺 Β· sup({𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}, ℝ, < )) = sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ))
219125, 134, 2183eqtrd 2781 . . . . 5 (πœ‘ β†’ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) = sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ))
220 vex 3447 . . . . . . . . . . . 12 𝑐 ∈ V
221 eqeq1 2741 . . . . . . . . . . . . 13 (𝑣 = 𝑐 β†’ (𝑣 = (𝐺 Β· 𝑑) ↔ 𝑐 = (𝐺 Β· 𝑑)))
222221rexbidv 3173 . . . . . . . . . . . 12 (𝑣 = 𝑐 β†’ (βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑) ↔ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑)))
223220, 222elab 3628 . . . . . . . . . . 11 (𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} ↔ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑))
224223biimpi 215 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β†’ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑))
225 nfv 1917 . . . . . . . . . . . 12 β„²π‘‘βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))
226 vex 3447 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
227 eqeq1 2741 . . . . . . . . . . . . . . . . . 18 (𝑀 = 𝑑 β†’ (𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))))
228227rexbidv 3173 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑑 β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘)) ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))))
229226, 228elab 3628 . . . . . . . . . . . . . . . 16 (𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)))
230229biimpi 215 . . . . . . . . . . . . . . 15 (𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)))
231230adantr 481 . . . . . . . . . . . . . 14 ((𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)))
232 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 Β· 𝑑) ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 = (𝐺 Β· 𝑑))
233 oveq2 7359 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ (𝐺 Β· 𝑑) = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
234233adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝐺 Β· 𝑑) ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝐺 Β· 𝑑) = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
235232, 234eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝐺 Β· 𝑑) ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
236235ex 413 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐺 Β· 𝑑) β†’ (𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))))
237236reximdv 3165 . . . . . . . . . . . . . . 15 (𝑐 = (𝐺 Β· 𝑑) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))))
238237adantl 482 . . . . . . . . . . . . . 14 ((𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))))
239231, 238mpd 15 . . . . . . . . . . . . 13 ((𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
240239ex 413 . . . . . . . . . . . 12 (𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))))
241225, 240rexlimi 3240 . . . . . . . . . . 11 (βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
242241a1i 11 . . . . . . . . . 10 (𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β†’ (βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))))
243224, 242mpd 15 . . . . . . . . 9 (𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
244243adantl 482 . . . . . . . 8 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
245 simp3 1138 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))) β†’ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
24638adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝐺 ∈ ℝ)
247246, 173remulcld 11143 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ∈ ℝ)
24845adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (1 + 𝐸) ∈ ℝ)
24952a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ β„• ∈ V)
25060adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ π‘Š ∈ Fin)
25164adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ (πΆβ€˜π‘—):π‘ŠβŸΆβ„)
252158adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ 𝑒 ∈ ℝ)
25379adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ (π·β€˜π‘—):π‘ŠβŸΆβ„)
25474, 252, 250, 253hsphoif 44718 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((π»β€˜π‘’)β€˜(π·β€˜π‘—)):π‘ŠβŸΆβ„)
25527, 250, 251, 254hoidmvcl 44724 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))) ∈ (0[,)+∞))
25654, 255sselid 3940 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
257256fmpttd 7059 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))):β„•βŸΆ(0[,]+∞))
258249, 257sge0cl 44523 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞))
259249, 257sge0xrcl 44527 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ∈ ℝ*)
26086a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ +∞ ∈ ℝ*)
26189adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))) ∈ ℝ*)
262 nfv 1917 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗(πœ‘ ∧ 𝑒 ∈ π‘ˆ)
26392adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)) ∈ (0[,]+∞))
26495adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ 𝑍 ∈ (π‘Š βˆ– π‘Œ))
26527, 250, 264, 9, 252, 74, 251, 253hsphoidmvle 44728 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))
266262, 249, 256, 263, 265sge0lempt 44552 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))))
26798adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)(π·β€˜π‘—)))) < +∞)
268259, 261, 260, 266, 267xrlelttrd 13033 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) < +∞)
269259, 260, 268xrltned 43496 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) β‰  +∞)
270 ge0xrre 43670 . . . . . . . . . . . . . . . 16 (((Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ∈ (0[,]+∞) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) β‰  +∞) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ∈ ℝ)
271258, 269, 270syl2anc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ∈ ℝ)
272248, 271remulcld 11143 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))) ∈ ℝ)
273126, 123sseldd 3943 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑆 ∈ ℝ)
27427, 30, 94, 9, 61, 76, 88, 65, 273sge0hsphoire 44731 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))) ∈ ℝ)
27545, 274remulcld 11143 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))) ∈ ℝ)
276275adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))) ∈ ℝ)
27714eleq2i 2829 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ π‘ˆ ↔ 𝑒 ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))})
278277biimpi 215 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ π‘ˆ β†’ 𝑒 ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))})
279 oveq1 7358 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑒 β†’ (𝑧 βˆ’ (π΄β€˜π‘)) = (𝑒 βˆ’ (π΄β€˜π‘)))
280279oveq2d 7367 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑒 β†’ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))))
281 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑒 β†’ (π»β€˜π‘§) = (π»β€˜π‘’))
282281fveq1d 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑒 β†’ ((π»β€˜π‘§)β€˜(π·β€˜π‘—)) = ((π»β€˜π‘’)β€˜(π·β€˜π‘—)))
283282oveq2d 7367 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑒 β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))
284283mpteq2dv 5205 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑒 β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))) = (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))
285284fveq2d 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑒 β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))))
286285oveq2d 7367 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑒 β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) = ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))))
287280, 286breq12d 5116 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑒 β†’ ((𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) ↔ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))))))
288287elrab 3643 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))} ↔ (𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))))))
289278, 288sylib 217 . . . . . . . . . . . . . . . 16 (𝑒 ∈ π‘ˆ β†’ (𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))))))
290289simprd 496 . . . . . . . . . . . . . . 15 (𝑒 ∈ π‘ˆ β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))))
291290adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))))
292274adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))) ∈ ℝ)
29351adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 0 ≀ (1 + 𝐸))
294273adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑆 ∈ ℝ)
29574, 294, 60, 79hsphoif 44718 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((π»β€˜π‘†)β€˜(π·β€˜π‘—)):π‘ŠβŸΆβ„)
29627, 60, 64, 295hoidmvcl 44724 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))) ∈ (0[,)+∞))
29754, 296sselid 3940 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
298297adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))) ∈ (0[,]+∞))
299294adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ 𝑆 ∈ ℝ)
300127adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ π‘ˆ βŠ† ℝ)
301121adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ π‘ˆ β‰  βˆ…)
302131adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ π‘ˆ 𝑧 ≀ 𝑦)
303 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ∈ π‘ˆ)
304 suprub 12074 . . . . . . . . . . . . . . . . . . . 20 (((π‘ˆ βŠ† ℝ ∧ π‘ˆ β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ π‘ˆ 𝑧 ≀ 𝑦) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ sup(π‘ˆ, ℝ, < ))
305300, 301, 302, 303, 304syl31anc 1373 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ sup(π‘ˆ, ℝ, < ))
306305, 1breqtrrdi 5145 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ 𝑆)
307306adantr 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ 𝑒 ≀ 𝑆)
30827, 250, 264, 9, 252, 299, 307, 74, 251, 253hsphoidmvle2 44727 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑗 ∈ β„•) β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))) ≀ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))
309262, 249, 256, 298, 308sge0lempt 44552 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—))))) ≀ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))
310271, 292, 248, 293, 309lemul2ad 12053 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘’)β€˜(π·β€˜π‘—)))))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
311247, 272, 276, 291, 310letrd 11270 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
3123113adant3 1132 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
313245, 312eqbrtrd 5125 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))) β†’ 𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
3143133exp 1119 . . . . . . . . . 10 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))))
315314rexlimdv 3148 . . . . . . . . 9 (πœ‘ β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
316315adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
317244, 316mpd 15 . . . . . . 7 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ 𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
318317ralrimiva 3141 . . . . . 6 (πœ‘ β†’ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
319224adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑))
320 nfv 1917 . . . . . . . . . . . 12 β„²π‘‘πœ‘
321 nfcv 2905 . . . . . . . . . . . . 13 Ⅎ𝑑𝑐
322 nfre1 3266 . . . . . . . . . . . . . 14 β„²π‘‘βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)
323322nfab 2911 . . . . . . . . . . . . 13 Ⅎ𝑑{𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}
324321, 323nfel 2919 . . . . . . . . . . . 12 Ⅎ𝑑 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}
325320, 324nfan 1902 . . . . . . . . . . 11 Ⅎ𝑑(πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)})
326 nfv 1917 . . . . . . . . . . 11 Ⅎ𝑑 𝑐 ∈ ℝ
327230adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)))
328 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ 𝑐 = (𝐺 Β· 𝑑))
3292463adant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝐺 ∈ ℝ)
330 simp3 1138 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)))
3311733adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) ∈ ℝ)
332330, 331eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑑 ∈ ℝ)
333329, 332remulcld 11143 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝐺 Β· 𝑑) ∈ ℝ)
334333adantr 481 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ (𝐺 Β· 𝑑) ∈ ℝ)
335328, 334eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) ∧ 𝑐 = (𝐺 Β· 𝑑)) β†’ 𝑐 ∈ ℝ)
336335ex 413 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘))) β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ))
3373363exp 1119 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ))))
338337rexlimdv 3148 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ)))
339338adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑑 = (𝑒 βˆ’ (π΄β€˜π‘)) β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ)))
340327, 339mpd 15 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}) β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ))
341340ex 413 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ)))
342341adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ (𝑑 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} β†’ (𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ)))
343325, 326, 342rexlimd 3247 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ (βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑐 = (𝐺 Β· 𝑑) β†’ 𝑐 ∈ ℝ))
344319, 343mpd 15 . . . . . . . . 9 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ 𝑐 ∈ ℝ)
345344ralrimiva 3141 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ∈ ℝ)
346 dfss3 3930 . . . . . . . 8 ({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} βŠ† ℝ ↔ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ∈ ℝ)
347345, 346sylibr 233 . . . . . . 7 (πœ‘ β†’ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} βŠ† ℝ)
34840eqcomd 2743 . . . . . . . . . 10 (πœ‘ β†’ 0 = (𝐺 Β· 0))
349 oveq2 7359 . . . . . . . . . . 11 (𝑑 = 0 β†’ (𝐺 Β· 𝑑) = (𝐺 Β· 0))
350349rspceeqv 3593 . . . . . . . . . 10 ((0 ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))} ∧ 0 = (𝐺 Β· 0)) β†’ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 = (𝐺 Β· 𝑑))
351187, 348, 350syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 = (𝐺 Β· 𝑑))
352 eqeq1 2741 . . . . . . . . . 10 (𝑣 = 0 β†’ (𝑣 = (𝐺 Β· 𝑑) ↔ 0 = (𝐺 Β· 𝑑)))
353352rexbidv 3173 . . . . . . . . 9 (𝑣 = 0 β†’ (βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑) ↔ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}0 = (𝐺 Β· 𝑑)))
35446, 351, 353elabd 3631 . . . . . . . 8 (πœ‘ β†’ 0 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)})
355 ne0i 4292 . . . . . . . 8 (0 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β†’ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β‰  βˆ…)
356354, 355syl 17 . . . . . . 7 (πœ‘ β†’ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β‰  βˆ…)
35738, 190remulcld 11143 . . . . . . . 8 (πœ‘ β†’ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))) ∈ ℝ)
358190adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)) ∈ ℝ)
359137adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 0 ≀ 𝐺)
36013adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (π΅β€˜π‘) ∈ ℝ)
361 iccleub 13273 . . . . . . . . . . . . . . . . . 18 (((π΄β€˜π‘) ∈ ℝ* ∧ (π΅β€˜π‘) ∈ ℝ* ∧ 𝑒 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘))) β†’ 𝑒 ≀ (π΅β€˜π‘))
362152, 154, 155, 361syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 ≀ (π΅β€˜π‘))
363158, 360, 159, 362lesub1dd 11729 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 βˆ’ (π΄β€˜π‘)) ≀ ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))
364173, 358, 246, 359, 363lemul2ad 12053 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
3653643adant3 1132 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))) β†’ (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
366245, 365eqbrtrd 5125 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑒 ∈ π‘ˆ ∧ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘)))) β†’ 𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
3673663exp 1119 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑒 ∈ π‘ˆ β†’ (𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))))
368367rexlimdv 3148 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))))
369368adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ (βˆƒπ‘’ ∈ π‘ˆ 𝑐 = (𝐺 Β· (𝑒 βˆ’ (π΄β€˜π‘))) β†’ 𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))))
370244, 369mpd 15 . . . . . . . . 9 ((πœ‘ ∧ 𝑐 ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}) β†’ 𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
371370ralrimiva 3141 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))))
372 brralrspcev 5163 . . . . . . . 8 (((𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘))) ∈ ℝ ∧ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ (𝐺 Β· ((π΅β€˜π‘) βˆ’ (π΄β€˜π‘)))) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ 𝑦)
373357, 371, 372syl2anc 584 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ 𝑦)
374 suprleub 12079 . . . . . . 7 ((({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} βŠ† ℝ ∧ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)} β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ 𝑦) ∧ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))) ∈ ℝ) β†’ (sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))) ↔ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
375347, 356, 373, 275, 374syl31anc 1373 . . . . . 6 (πœ‘ β†’ (sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))) ↔ βˆ€π‘ ∈ {𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}𝑐 ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
376318, 375mpbird 256 . . . . 5 (πœ‘ β†’ sup({𝑣 ∣ βˆƒπ‘‘ ∈ {𝑀 ∣ βˆƒπ‘’ ∈ π‘ˆ 𝑀 = (𝑒 βˆ’ (π΄β€˜π‘))}𝑣 = (𝐺 Β· 𝑑)}, ℝ, < ) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
377219, 376eqbrtrd 5125 . . . 4 (πœ‘ β†’ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
378123, 377jca 512 . . 3 (πœ‘ β†’ (𝑆 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
379 oveq1 7358 . . . . . 6 (𝑧 = 𝑆 β†’ (𝑧 βˆ’ (π΄β€˜π‘)) = (𝑆 βˆ’ (π΄β€˜π‘)))
380379oveq2d 7367 . . . . 5 (𝑧 = 𝑆 β†’ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) = (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))))
381 fveq2 6839 . . . . . . . . . 10 (𝑧 = 𝑆 β†’ (π»β€˜π‘§) = (π»β€˜π‘†))
382381fveq1d 6841 . . . . . . . . 9 (𝑧 = 𝑆 β†’ ((π»β€˜π‘§)β€˜(π·β€˜π‘—)) = ((π»β€˜π‘†)β€˜(π·β€˜π‘—)))
383382oveq2d 7367 . . . . . . . 8 (𝑧 = 𝑆 β†’ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))) = ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))
384383mpteq2dv 5205 . . . . . . 7 (𝑧 = 𝑆 β†’ (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))) = (𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))
385384fveq2d 6843 . . . . . 6 (𝑧 = 𝑆 β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))
386385oveq2d 7367 . . . . 5 (𝑧 = 𝑆 β†’ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) = ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—)))))))
387380, 386breq12d 5116 . . . 4 (𝑧 = 𝑆 β†’ ((𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—)))))) ↔ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
388387elrab 3643 . . 3 (𝑆 ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))} ↔ (𝑆 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∧ (𝐺 Β· (𝑆 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘†)β€˜(π·β€˜π‘—))))))))
389378, 388sylibr 233 . 2 (πœ‘ β†’ 𝑆 ∈ {𝑧 ∈ ((π΄β€˜π‘)[,](π΅β€˜π‘)) ∣ (𝐺 Β· (𝑧 βˆ’ (π΄β€˜π‘))) ≀ ((1 + 𝐸) Β· (Ξ£^β€˜(𝑗 ∈ β„• ↦ ((πΆβ€˜π‘—)(πΏβ€˜π‘Š)((π»β€˜π‘§)β€˜(π·β€˜π‘—))))))})
390389, 14eleqtrrdi 2849 1 (πœ‘ β†’ 𝑆 ∈ π‘ˆ)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106  {cab 2714   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3405  Vcvv 3443   βˆ– cdif 3905   βˆͺ cun 3906   βŠ† wss 3908  βˆ…c0 4280  ifcif 4484  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   β†Ύ cres 5633  βŸΆwf 6489  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353   ↑m cmap 8723  Fincfn 8841  supcsup 9334  β„cr 11008  0cc0 11009  1c1 11010   + caddc 11012   Β· cmul 11014  +∞cpnf 11144  β„*cxr 11146   < clt 11147   ≀ cle 11148   βˆ’ cmin 11343  β„•cn 12111  β„+crp 12869  [,)cico 13220  [,]cicc 13221  βˆcprod 15748  volcvol 24779  Ξ£^csumge0 44504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-2o 8405  df-er 8606  df-map 8725  df-pm 8726  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fi 9305  df-sup 9336  df-inf 9337  df-oi 9404  df-dju 9795  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-n0 12372  df-z 12458  df-uz 12722  df-q 12828  df-rp 12870  df-xneg 12987  df-xadd 12988  df-xmul 12989  df-ioo 13222  df-ico 13224  df-icc 13225  df-fz 13379  df-fzo 13522  df-fl 13651  df-seq 13861  df-exp 13922  df-hash 14185  df-cj 14944  df-re 14945  df-im 14946  df-sqrt 15080  df-abs 15081  df-clim 15330  df-rlim 15331  df-sum 15531  df-prod 15749  df-rest 17264  df-topgen 17285  df-psmet 20741  df-xmet 20742  df-met 20743  df-bl 20744  df-mopn 20745  df-top 22195  df-topon 22212  df-bases 22248  df-cmp 22690  df-ovol 24780  df-vol 24781  df-sumge0 44505
This theorem is referenced by:  hoidmvlelem4  44740
  Copyright terms: Public domain W3C validator