Metamath Proof Explorer

Theorem hoidmvlelem1

Description: The supremum of U belongs to U . Step (c) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses 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 hoidmvlelem1 ( 𝜑 → 𝑆 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 hoidmvlelem1.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoidmvlelem1.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoidmvlelem1.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4 hoidmvlelem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) )
5 hoidmvlelem1.w ⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } )
6 hoidmvlelem1.a ⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ )
7 hoidmvlelem1.b ⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ )
8 hoidmvlelem1.c ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
9 hoidmvlelem1.d ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
10 hoidmvlelem1.r ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ )
11 hoidmvlelem1.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) )
12 hoidmvlelem1.g ⊢ 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) )
13 hoidmvlelem1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
14 hoidmvlelem1.u ⊢ 𝑈 = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) }
15 hoidmvlelem1.s ⊢ 𝑆 = sup ( 𝑈 , ℝ , < )
16 hoidmvlelem1.ab ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) )
17 15 a1i ⊢ ( 𝜑 → 𝑆 = sup ( 𝑈 , ℝ , < ) )
18 snidg ⊢ ( 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑍 ∈ { 𝑍 } )
19 4 18 syl ⊢ ( 𝜑 → 𝑍 ∈ { 𝑍 } )
20 elun2 ⊢ ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
21 19 20 syl ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
22 21 5 eleqtrrdi ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
23 6 22 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
24 7 22 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
25 ssrab2 ⊢ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) )
26 14 25 eqsstri ⊢ 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) )
27 26 a1i ⊢ ( 𝜑 → 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
28 23 leidd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐴 ‘ 𝑍 ) )
29 23 24 16 ltled ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ≤ ( 𝐵 ‘ 𝑍 ) )
30 23 24 23 28 29 eliccd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
31 23 recnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℂ )
32 31 subidd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) = 0 )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · 0 ) )
34 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
35 2 3 ssfid ⊢ ( 𝜑 → 𝑌 ∈ Fin )
36 ssun1 ⊢ 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } )
37 36 5 sseqtrri ⊢ 𝑌 ⊆ 𝑊
38 37 a1i ⊢ ( 𝜑 → 𝑌 ⊆ 𝑊 )
39 6 38 fssresd ⊢ ( 𝜑 → ( 𝐴 ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
40 7 38 fssresd ⊢ ( 𝜑 → ( 𝐵 ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
41 1 35 39 40 hoidmvcl ⊢ ( 𝜑 → ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) ∈ ( 0 [,) +∞ ) )
42 12 41 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ( 0 [,) +∞ ) )
43 34 42 sseldi ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
44 43 recnd ⊢ ( 𝜑 → 𝐺 ∈ ℂ )
45 44 mul01d ⊢ ( 𝜑 → ( 𝐺 · 0 ) = 0 )
46 33 45 eqtrd ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) = 0 )
47 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
48 13 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
49 47 48 readdcld ⊢ ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ )
50 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
51 0lt1 ⊢ 0 < 1
52 51 a1i ⊢ ( 𝜑 → 0 < 1 )
53 47 13 ltaddrpd ⊢ ( 𝜑 → 1 < ( 1 + 𝐸 ) )
54 50 47 49 52 53 lttrd ⊢ ( 𝜑 → 0 < ( 1 + 𝐸 ) )
55 50 49 54 ltled ⊢ ( 𝜑 → 0 ≤ ( 1 + 𝐸 ) )
56 nnex ⊢ ℕ ∈ V
57 56 a1i ⊢ ( 𝜑 → ℕ ∈ V )
58 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
59 snfi ⊢ { 𝑍 } ∈ Fin
60 59 a1i ⊢ ( 𝜑 → { 𝑍 } ∈ Fin )
61 unfi ⊢ ( ( 𝑌 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
62 35 60 61 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ∈ Fin )
63 5 62 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ Fin )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
65 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
66 elmapi ⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
67 65 66 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
68 eleq1w ⊢ ( 𝑗 = ℎ → ( 𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
69 fveq2 ⊢ ( 𝑗 = ℎ → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ ℎ ) )
70 69 breq1d ⊢ ( 𝑗 = ℎ → ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝑐 ‘ ℎ ) ≤ 𝑥 ) )
71 70 69 ifbieq1d ⊢ ( 𝑗 = ℎ → if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) = if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) )
72 68 69 71 ifbieq12d ⊢ ( 𝑗 = ℎ → if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) = if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
73 72 cbvmptv ⊢ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) = ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) )
74 73 mpteq2i ⊢ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) )
75 74 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
76 11 75 eqtri ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) )
77 23 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
78 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
79 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
81 76 77 64 80 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
82 1 64 67 81 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
83 58 82 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
84 83 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
85 57 84 sge0cl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
86 57 84 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
87 pnfxr ⊢ +∞ ∈ ℝ*
88 87 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
89 10 rexrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
90 nfv ⊢ Ⅎ 𝑗 𝜑
91 1 64 67 80 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) )
92 58 91 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
93 4 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 )
94 22 93 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
96 1 64 95 5 77 76 67 80 hsphoidmvle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) )
97 90 57 83 92 96 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
98 10 ltpnfd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
99 86 89 88 97 98 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
100 86 88 99 xrltned ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ )
101 ge0xrre ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
102 85 100 101 syl2anc ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
103 57 84 sge0ge0 ⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
104 mulge0 ⊢ ( ( ( ( 1 + 𝐸 ) ∈ ℝ ∧ 0 ≤ ( 1 + 𝐸 ) ) ∧ ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ ∧ 0 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) → 0 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
105 49 55 102 103 104 syl22anc ⊢ ( 𝜑 → 0 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
106 46 105 eqbrtrd ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
107 30 106 jca ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
108 oveq1 ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
109 108 oveq2d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
110 fveq2 ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) )
111 110 fveq1d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
112 111 oveq2d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
113 112 mpteq2dv ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
114 113 fveq2d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
115 114 oveq2d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
116 109 115 breq12d ⊢ ( 𝑧 = ( 𝐴 ‘ 𝑍 ) → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
117 116 elrab ⊢ ( ( 𝐴 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( ( 𝐴 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
118 107 117 sylibr ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
119 118 14 eleqtrrdi ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ 𝑈 )
120 ne0i ⊢ ( ( 𝐴 ‘ 𝑍 ) ∈ 𝑈 → 𝑈 ≠ ∅ )
121 119 120 syl ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
122 23 24 27 121 supicc ⊢ ( 𝜑 → sup ( 𝑈 , ℝ , < ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
123 17 122 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
124 17 oveq1d ⊢ ( 𝜑 → ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) = ( sup ( 𝑈 , ℝ , < ) − ( 𝐴 ‘ 𝑍 ) ) )
125 124 oveq2d ⊢ ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( sup ( 𝑈 , ℝ , < ) − ( 𝐴 ‘ 𝑍 ) ) ) )
126 23 24 iccssred ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ⊆ ℝ )
127 27 126 sstrd ⊢ ( 𝜑 → 𝑈 ⊆ ℝ )
128 23 24 jca ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) )
129 iccsupr ⊢ ( ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) ∧ 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐴 ‘ 𝑍 ) ∈ 𝑈 ) → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 ) )
130 128 27 119 129 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 ) )
131 130 simp3d ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 )
132 eqid ⊢ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } = { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
133 127 121 131 23 132 supsubc ⊢ ( 𝜑 → ( sup ( 𝑈 , ℝ , < ) − ( 𝐴 ‘ 𝑍 ) ) = sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) )
134 133 oveq2d ⊢ ( 𝜑 → ( 𝐺 · ( sup ( 𝑈 , ℝ , < ) − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) ) )
135 50 rexrd ⊢ ( 𝜑 → 0 ∈ ℝ* )
136 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐺 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐺 )
137 135 88 42 136 syl3anc ⊢ ( 𝜑 → 0 ≤ 𝐺 )
138 vex ⊢ 𝑟 ∈ V
139 eqeq1 ⊢ ( 𝑤 = 𝑟 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
140 139 rexbidv ⊢ ( 𝑤 = 𝑟 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
141 138 140 elab ⊢ ( 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ↔ ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
142 141 biimpi ⊢ ( 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
143 142 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
144 nfv ⊢ Ⅎ 𝑢 𝜑
145 nfcv ⊢ Ⅎ 𝑢 𝑟
146 nfre1 ⊢ Ⅎ 𝑢 ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) )
147 146 nfab ⊢ Ⅎ 𝑢 { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
148 145 147 nfel ⊢ Ⅎ 𝑢 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
149 144 148 nfan ⊢ Ⅎ 𝑢 ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
150 nfv ⊢ Ⅎ 𝑢 0 ≤ 𝑟
151 23 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
152 151 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
153 24 rexrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
154 153 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
155 27 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
156 iccgelb ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 )
157 152 154 155 156 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 )
158 127 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ℝ )
159 23 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
160 158 159 subge0d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 ) )
161 157 160 mpbird ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
162 161 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
163 id ⊢ ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
164 163 eqcomd ⊢ ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = 𝑟 )
165 164 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = 𝑟 )
166 162 165 breqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 0 ≤ 𝑟 )
167 166 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) ) )
168 167 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑢 ∈ 𝑈 → ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) ) )
169 149 150 168 rexlimd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) )
170 143 169 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → 0 ≤ 𝑟 )
171 170 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 )
172 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
173 158 159 resubcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
174 173 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
175 172 174 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑤 ∈ ℝ )
176 175 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) ) )
177 176 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) )
178 177 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) )
179 abss ⊢ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ↔ ∀ 𝑤 ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) )
180 178 179 sylibr ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ )
181 32 eqcomd ⊢ ( 𝜑 → 0 = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
182 oveq1 ⊢ ( 𝑢 = ( 𝐴 ‘ 𝑍 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
183 182 rspceeqv ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ 𝑈 ∧ 0 = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) → ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
184 119 181 183 syl2anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
185 eqeq1 ⊢ ( 𝑤 = 0 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
186 185 rexbidv ⊢ ( 𝑤 = 0 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
187 50 184 186 elabd ⊢ ( 𝜑 → 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
188 ne0i ⊢ ( 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ )
189 187 188 syl ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ )
190 24 23 resubcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
191 vex ⊢ 𝑠 ∈ V
192 eqeq1 ⊢ ( 𝑤 = 𝑠 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
193 192 rexbidv ⊢ ( 𝑤 = 𝑠 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
194 191 193 elab ⊢ ( 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ↔ ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
195 194 biimpi ⊢ ( 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
196 195 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
197 nfcv ⊢ Ⅎ 𝑢 𝑠
198 197 147 nfel ⊢ Ⅎ 𝑢 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
199 144 198 nfan ⊢ Ⅎ 𝑢 ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
200 nfv ⊢ Ⅎ 𝑢 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) )
201 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
202 159 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
203 24 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
204 155 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
205 30 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
206 202 203 204 205 iccsuble ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
207 201 206 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
208 207 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
209 208 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑢 ∈ 𝑈 → ( 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
210 199 200 209 rexlimd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
211 196 210 mpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
212 211 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
213 brralrspcev ⊢ ( ( ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ ∧ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 )
214 190 212 213 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 )
215 eqid ⊢ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } = { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
216 biid ⊢ ( ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) ↔ ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) )
217 215 216 supmul1 ⊢ ( ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) → ( 𝐺 · sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
218 43 137 171 180 189 214 217 syl33anc ⊢ ( 𝜑 → ( 𝐺 · sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
219 125 134 218 3eqtrd ⊢ ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
220 vex ⊢ 𝑐 ∈ V
221 eqeq1 ⊢ ( 𝑣 = 𝑐 → ( 𝑣 = ( 𝐺 · 𝑡 ) ↔ 𝑐 = ( 𝐺 · 𝑡 ) ) )
222 221 rexbidv ⊢ ( 𝑣 = 𝑐 → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) ) )
223 220 222 elab ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
224 223 biimpi ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
225 nfv ⊢ Ⅎ 𝑡 ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
226 vex ⊢ 𝑡 ∈ V
227 eqeq1 ⊢ ( 𝑤 = 𝑡 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
228 227 rexbidv ⊢ ( 𝑤 = 𝑡 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
229 226 228 elab ⊢ ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ↔ ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
230 229 biimpi ⊢ ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
231 230 adantr ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
232 simpl ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 = ( 𝐺 · 𝑡 ) )
233 oveq2 ⊢ ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝐺 · 𝑡 ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
234 233 adantl ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐺 · 𝑡 ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
235 232 234 eqtrd ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
236 235 ex ⊢ ( 𝑐 = ( 𝐺 · 𝑡 ) → ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
237 236 reximdv ⊢ ( 𝑐 = ( 𝐺 · 𝑡 ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
238 237 adantl ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
239 231 238 mpd ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
240 239 ex ⊢ ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
241 225 240 rexlimi ⊢ ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
242 241 a1i ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
243 224 242 mpd ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
244 243 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
245 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
246 43 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝐺 ∈ ℝ )
247 246 173 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ )
248 49 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 1 + 𝐸 ) ∈ ℝ )
249 56 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ℕ ∈ V )
250 64 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
251 67 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
252 158 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑢 ∈ ℝ )
253 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
254 76 252 250 253 hsphoif ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
255 1 250 251 254 hoidmvcl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
256 58 255 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
257 256 fmpttd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
258 249 257 sge0cl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
259 249 257 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
260 87 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → +∞ ∈ ℝ* )
261 89 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
262 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑢 ∈ 𝑈 )
263 92 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
264 95 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
265 1 250 264 5 252 76 251 253 hsphoidmvle ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) )
266 262 249 256 263 265 sge0lempt ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
267 98 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
268 259 261 260 266 267 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
269 259 260 268 xrltned ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ )
270 ge0xrre ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
271 258 269 270 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
272 248 271 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
273 126 123 sseldd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
274 1 35 94 5 8 9 10 11 273 sge0hsphoire ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
275 49 274 remulcld ⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
276 275 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
277 14 eleq2i ⊢ ( 𝑢 ∈ 𝑈 ↔ 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
278 277 biimpi ⊢ ( 𝑢 ∈ 𝑈 → 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
279 oveq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
280 279 oveq2d ⊢ ( 𝑧 = 𝑢 → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
281 fveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑢 ) )
282 281 fveq1d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
283 282 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
284 283 mpteq2dv ⊢ ( 𝑧 = 𝑢 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
285 284 fveq2d ⊢ ( 𝑧 = 𝑢 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
286 285 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
287 280 286 breq12d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
288 287 elrab ⊢ ( 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
289 278 288 sylib ⊢ ( 𝑢 ∈ 𝑈 → ( 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
290 289 simprd ⊢ ( 𝑢 ∈ 𝑈 → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
291 290 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
292 274 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
293 55 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ ( 1 + 𝐸 ) )
294 273 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
295 76 294 64 80 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
296 1 64 67 295 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
297 58 296 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
298 297 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
299 294 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
300 127 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ℝ )
301 121 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ≠ ∅ )
302 131 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 )
303 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
304 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
305 300 301 302 303 304 syl31anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
306 305 15 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ 𝑆 )
307 306 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑢 ≤ 𝑆 )
308 1 250 264 5 252 299 307 76 251 253 hsphoidmvle2 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
309 262 249 256 298 308 sge0lempt ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
310 271 292 248 293 309 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
311 247 272 276 291 310 letrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
312 311 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
313 245 312 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
314 313 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) )
315 314 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
316 315 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
317 244 316 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
318 317 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
319 224 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
320 nfv ⊢ Ⅎ 𝑡 𝜑
321 nfcv ⊢ Ⅎ 𝑡 𝑐
322 nfre1 ⊢ Ⅎ 𝑡 ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 )
323 322 nfab ⊢ Ⅎ 𝑡 { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
324 321 323 nfel ⊢ Ⅎ 𝑡 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
325 320 324 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } )
326 nfv ⊢ Ⅎ 𝑡 𝑐 ∈ ℝ
327 230 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
328 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → 𝑐 = ( 𝐺 · 𝑡 ) )
329 246 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝐺 ∈ ℝ )
330 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
331 173 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
332 330 331 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑡 ∈ ℝ )
333 329 332 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐺 · 𝑡 ) ∈ ℝ )
334 333 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ( 𝐺 · 𝑡 ) ∈ ℝ )
335 328 334 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → 𝑐 ∈ ℝ )
336 335 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
337 336 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) ) )
338 337 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
339 338 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
340 327 339 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
341 340 ex ⊢ ( 𝜑 → ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
342 341 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
343 325 326 342 rexlimd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
344 319 343 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ∈ ℝ )
345 344 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ∈ ℝ )
346 dfss3 ⊢ ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ∈ ℝ )
347 345 346 sylibr ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ )
348 45 eqcomd ⊢ ( 𝜑 → 0 = ( 𝐺 · 0 ) )
349 oveq2 ⊢ ( 𝑡 = 0 → ( 𝐺 · 𝑡 ) = ( 𝐺 · 0 ) )
350 349 rspceeqv ⊢ ( ( 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 0 = ( 𝐺 · 0 ) ) → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) )
351 187 348 350 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) )
352 eqeq1 ⊢ ( 𝑣 = 0 → ( 𝑣 = ( 𝐺 · 𝑡 ) ↔ 0 = ( 𝐺 · 𝑡 ) ) )
353 352 rexbidv ⊢ ( 𝑣 = 0 → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) ) )
354 50 351 353 elabd ⊢ ( 𝜑 → 0 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } )
355 ne0i ⊢ ( 0 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ )
356 354 355 syl ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ )
357 43 190 remulcld ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ )
358 190 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
359 137 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ 𝐺 )
360 24 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
361 iccleub ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
362 152 154 155 361 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
363 158 360 159 362 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
364 173 358 246 359 363 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
365 364 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
366 245 365 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
367 366 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) ) )
368 367 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
369 368 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
370 244 369 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
371 370 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
372 brralrspcev ⊢ ( ( ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ ∧ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 )
373 357 371 372 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 )
374 suprleub ⊢ ( ( ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ ∧ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 ) ∧ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ ) → ( sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
375 347 356 373 275 374 syl31anc ⊢ ( 𝜑 → ( sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
376 318 375 mpbird ⊢ ( 𝜑 → sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
377 219 376 eqbrtrd ⊢ ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
378 123 377 jca ⊢ ( 𝜑 → ( 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
379 oveq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) )
380 379 oveq2d ⊢ ( 𝑧 = 𝑆 → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) )
381 fveq2 ⊢ ( 𝑧 = 𝑆 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑆 ) )
382 381 fveq1d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
383 382 oveq2d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
384 383 mpteq2dv ⊢ ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
385 384 fveq2d ⊢ ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
386 385 oveq2d ⊢ ( 𝑧 = 𝑆 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
387 380 386 breq12d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
388 387 elrab ⊢ ( 𝑆 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
389 378 388 sylibr ⊢ ( 𝜑 → 𝑆 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
390 389 14 eleqtrrdi ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )