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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
24 7 22 ffvelcdmd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
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 sselid ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
79 elmapi ⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
81 76 77 64 80 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
82 1 64 67 81 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
83 58 82 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐴 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 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 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 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 bilani ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
143 nfv ⊢ Ⅎ 𝑢 𝜑
144 nfcv ⊢ Ⅎ 𝑢 𝑟
145 nfre1 ⊢ Ⅎ 𝑢 ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) )
146 145 nfab ⊢ Ⅎ 𝑢 { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
147 144 146 nfel ⊢ Ⅎ 𝑢 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
148 143 147 nfan ⊢ Ⅎ 𝑢 ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
149 nfv ⊢ Ⅎ 𝑢 0 ≤ 𝑟
150 23 rexrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
151 150 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* )
152 24 rexrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* )
154 27 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
155 iccgelb ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 )
156 151 153 154 155 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 )
157 127 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ℝ )
158 23 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
159 157 158 subge0d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ( 𝐴 ‘ 𝑍 ) ≤ 𝑢 ) )
160 156 159 mpbird ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
161 160 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 0 ≤ ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
162 id ⊢ ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
163 162 eqcomd ⊢ ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = 𝑟 )
164 163 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = 𝑟 )
165 161 164 breqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 0 ≤ 𝑟 )
166 165 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑢 ∈ 𝑈 → ( 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) ) )
168 148 149 167 rexlimd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑟 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 0 ≤ 𝑟 ) )
169 142 168 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → 0 ≤ 𝑟 )
170 169 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 )
171 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
172 157 158 resubcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
173 172 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
174 171 173 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑤 ∈ ℝ )
175 174 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) ) )
176 175 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑤 ∈ ℝ ) )
177 176 abssdv ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ )
178 32 eqcomd ⊢ ( 𝜑 → 0 = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
179 oveq1 ⊢ ( 𝑢 = ( 𝐴 ‘ 𝑍 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
180 179 rspceeqv ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ 𝑈 ∧ 0 = ( ( 𝐴 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) → ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
181 119 178 180 syl2anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
182 eqeq1 ⊢ ( 𝑤 = 0 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
183 182 rexbidv ⊢ ( 𝑤 = 0 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 0 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
184 50 181 183 elabd ⊢ ( 𝜑 → 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
185 ne0i ⊢ ( 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ )
186 184 185 syl ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ )
187 24 23 resubcld ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
188 vex ⊢ 𝑠 ∈ V
189 eqeq1 ⊢ ( 𝑤 = 𝑠 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
190 189 rexbidv ⊢ ( 𝑤 = 𝑠 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
191 188 190 elab ⊢ ( 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ↔ ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
192 191 bilani ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
193 nfcv ⊢ Ⅎ 𝑢 𝑠
194 193 146 nfel ⊢ Ⅎ 𝑢 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) }
195 143 194 nfan ⊢ Ⅎ 𝑢 ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } )
196 nfv ⊢ Ⅎ 𝑢 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) )
197 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
198 158 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ )
199 24 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
200 154 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
201 30 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐴 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) )
202 198 199 200 201 iccsuble ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
203 197 202 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
204 203 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
205 204 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑢 ∈ 𝑈 → ( 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
206 195 196 205 rexlimd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑠 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
207 192 206 mpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
208 207 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
209 brralrspcev ⊢ ( ( ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ ∧ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 )
210 187 208 209 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 )
211 eqid ⊢ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } = { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
212 biid ⊢ ( ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) ↔ ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) )
213 211 212 supmul1 ⊢ ( ( ( 𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀ 𝑟 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 ≤ 𝑟 ) ∧ ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ⊆ ℝ ∧ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑠 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑠 ≤ 𝑟 ) ) → ( 𝐺 · sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
214 43 137 170 177 186 210 213 syl33anc ⊢ ( 𝜑 → ( 𝐺 · sup ( { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } , ℝ , < ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
215 125 134 214 3eqtrd ⊢ ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) = sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) )
216 vex ⊢ 𝑐 ∈ V
217 eqeq1 ⊢ ( 𝑣 = 𝑐 → ( 𝑣 = ( 𝐺 · 𝑡 ) ↔ 𝑐 = ( 𝐺 · 𝑡 ) ) )
218 217 rexbidv ⊢ ( 𝑣 = 𝑐 → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) ) )
219 216 218 elab ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
220 219 biimpi ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
221 nfv ⊢ Ⅎ 𝑡 ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
222 vex ⊢ 𝑡 ∈ V
223 eqeq1 ⊢ ( 𝑤 = 𝑡 → ( 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
224 223 rexbidv ⊢ ( 𝑤 = 𝑡 → ( ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ↔ ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
225 222 224 elab ⊢ ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ↔ ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
226 225 birani ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
227 simpl ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 = ( 𝐺 · 𝑡 ) )
228 oveq2 ⊢ ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝐺 · 𝑡 ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
229 228 adantl ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐺 · 𝑡 ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
230 227 229 eqtrd ⊢ ( ( 𝑐 = ( 𝐺 · 𝑡 ) ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
231 230 ex ⊢ ( 𝑐 = ( 𝐺 · 𝑡 ) → ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
232 231 reximdv ⊢ ( 𝑐 = ( 𝐺 · 𝑡 ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
233 232 adantl ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
234 226 233 mpd ⊢ ( ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
235 234 ex ⊢ ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) )
236 221 235 rexlimi ⊢ ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
237 220 236 syl ⊢ ( 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
238 237 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
239 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
240 43 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝐺 ∈ ℝ )
241 240 172 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ )
242 49 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 1 + 𝐸 ) ∈ ℝ )
243 56 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ℕ ∈ V )
244 64 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin )
245 67 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
246 157 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑢 ∈ ℝ )
247 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ )
248 76 246 244 247 hsphoif ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
249 1 244 245 248 hoidmvcl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
250 58 249 sselid ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
251 250 fmpttd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
252 243 251 sge0cl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
253 243 251 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* )
254 87 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → +∞ ∈ ℝ* )
255 89 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* )
256 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑢 ∈ 𝑈 )
257 92 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) )
258 95 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) )
259 1 244 258 5 246 76 245 247 hsphoidmvle ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) )
260 256 243 250 257 259 sge0lempt ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) )
261 98 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ )
262 253 255 254 260 261 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ )
263 253 254 262 xrltned ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ )
264 ge0xrre ⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
265 252 263 264 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
266 242 265 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
267 126 123 sseldd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
268 1 35 94 5 8 9 10 11 267 sge0hsphoire ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
269 49 268 remulcld ⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
270 269 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ )
271 14 eleq2i ⊢ ( 𝑢 ∈ 𝑈 ↔ 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
272 271 biimpi ⊢ ( 𝑢 ∈ 𝑈 → 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
273 oveq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
274 273 oveq2d ⊢ ( 𝑧 = 𝑢 → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) )
275 fveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑢 ) )
276 275 fveq1d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
277 276 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
278 277 mpteq2dv ⊢ ( 𝑧 = 𝑢 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
279 278 fveq2d ⊢ ( 𝑧 = 𝑢 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
280 279 oveq2d ⊢ ( 𝑧 = 𝑢 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
281 274 280 breq12d ⊢ ( 𝑧 = 𝑢 → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
282 281 elrab ⊢ ( 𝑢 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
283 272 282 sylib ⊢ ( 𝑢 ∈ 𝑈 → ( 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
284 283 simprd ⊢ ( 𝑢 ∈ 𝑈 → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
285 284 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
286 268 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
287 55 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ ( 1 + 𝐸 ) )
288 267 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
289 76 288 64 80 hsphoif ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ )
290 1 64 67 289 hoidmvcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) )
291 58 290 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
292 291 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) )
293 288 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑆 ∈ ℝ )
294 127 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ℝ )
295 121 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ≠ ∅ )
296 131 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 )
297 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 )
298 suprub ⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑈 𝑧 ≤ 𝑦 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
299 294 295 296 297 298 syl31anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) )
300 299 15 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ 𝑆 )
301 300 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → 𝑢 ≤ 𝑆 )
302 1 244 258 5 246 293 301 76 245 247 hsphoidmvle2 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
303 256 243 250 292 302 sge0lempt ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
304 265 286 242 287 303 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑢 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
305 241 266 270 285 304 letrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
306 305 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
307 239 306 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
308 307 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) )
309 308 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
310 309 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
311 238 310 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
312 311 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
313 219 bilani ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) )
314 nfv ⊢ Ⅎ 𝑡 𝜑
315 nfcv ⊢ Ⅎ 𝑡 𝑐
316 nfre1 ⊢ Ⅎ 𝑡 ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 )
317 316 nfab ⊢ Ⅎ 𝑡 { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
318 315 317 nfel ⊢ Ⅎ 𝑡 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) }
319 314 318 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } )
320 nfv ⊢ Ⅎ 𝑡 𝑐 ∈ ℝ
321 225 bilani ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
322 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → 𝑐 = ( 𝐺 · 𝑡 ) )
323 240 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝐺 ∈ ℝ )
324 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) )
325 172 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
326 324 325 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑡 ∈ ℝ )
327 323 326 remulcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝐺 · 𝑡 ) ∈ ℝ )
328 327 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → ( 𝐺 · 𝑡 ) ∈ ℝ )
329 322 328 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ∧ 𝑐 = ( 𝐺 · 𝑡 ) ) → 𝑐 ∈ ℝ )
330 329 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
331 330 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) ) )
332 331 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
333 332 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑡 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
334 321 333 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ) → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
335 334 ex ⊢ ( 𝜑 → ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
336 335 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } → ( 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) ) )
337 319 320 336 rexlimd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑐 = ( 𝐺 · 𝑡 ) → 𝑐 ∈ ℝ ) )
338 313 337 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ∈ ℝ )
339 338 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ∈ ℝ )
340 dfss3 ⊢ ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ∈ ℝ )
341 339 340 sylibr ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ )
342 45 eqcomd ⊢ ( 𝜑 → 0 = ( 𝐺 · 0 ) )
343 oveq2 ⊢ ( 𝑡 = 0 → ( 𝐺 · 𝑡 ) = ( 𝐺 · 0 ) )
344 343 rspceeqv ⊢ ( ( 0 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } ∧ 0 = ( 𝐺 · 0 ) ) → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) )
345 184 342 344 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) )
346 eqeq1 ⊢ ( 𝑣 = 0 → ( 𝑣 = ( 𝐺 · 𝑡 ) ↔ 0 = ( 𝐺 · 𝑡 ) ) )
347 346 rexbidv ⊢ ( 𝑣 = 0 → ( ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) ↔ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 0 = ( 𝐺 · 𝑡 ) ) )
348 50 345 347 elabd ⊢ ( 𝜑 → 0 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } )
349 ne0i ⊢ ( 0 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ )
350 348 349 syl ⊢ ( 𝜑 → { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ )
351 43 187 remulcld ⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ )
352 187 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ∈ ℝ )
353 137 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 0 ≤ 𝐺 )
354 24 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ )
355 iccleub ⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
356 151 153 154 355 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) )
357 157 354 158 356 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ≤ ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) )
358 172 352 240 353 357 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
359 358 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
360 239 359 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
361 360 3exp ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 → ( 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) ) )
362 361 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
363 362 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → ( ∃ 𝑢 ∈ 𝑈 𝑐 = ( 𝐺 · ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) )
364 238 363 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ) → 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
365 364 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) )
366 brralrspcev ⊢ ( ( ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ∈ ℝ ∧ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 )
367 351 365 366 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 )
368 suprleub ⊢ ( ( ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ⊆ ℝ ∧ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ 𝑦 ) ∧ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ ) → ( sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
369 341 350 367 269 368 syl31anc ⊢ ( 𝜑 → ( sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ∀ 𝑐 ∈ { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } 𝑐 ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
370 312 369 mpbird ⊢ ( 𝜑 → sup ( { 𝑣 ∣ ∃ 𝑡 ∈ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑈 𝑤 = ( 𝑢 − ( 𝐴 ‘ 𝑍 ) ) } 𝑣 = ( 𝐺 · 𝑡 ) } , ℝ , < ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
371 215 370 eqbrtrd ⊢ ( 𝜑 → ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
372 123 371 jca ⊢ ( 𝜑 → ( 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
373 oveq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) )
374 373 oveq2d ⊢ ( 𝑧 = 𝑆 → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) )
375 fveq2 ⊢ ( 𝑧 = 𝑆 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑆 ) )
376 375 fveq1d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) )
377 376 oveq2d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
378 377 mpteq2dv ⊢ ( 𝑧 = 𝑆 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) )
379 378 fveq2d ⊢ ( 𝑧 = 𝑆 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
380 379 oveq2d ⊢ ( 𝑧 = 𝑆 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
381 374 380 breq12d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
382 381 elrab ⊢ ( 𝑆 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( 𝑆 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑆 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
383 372 382 sylibr ⊢ ( 𝜑 → 𝑆 ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } )
384 383 14 eleqtrrdi ⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )