Metamath Proof Explorer

Theorem unbdqndv2lem2

Description: Lemma for unbdqndv2 . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2lem2.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) )
unbdqndv2lem2.w ⊢ 𝑊 = if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 )
unbdqndv2lem2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
unbdqndv2lem2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
unbdqndv2lem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
unbdqndv2lem2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
unbdqndv2lem2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
unbdqndv2lem2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
unbdqndv2lem2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑋 )
unbdqndv2lem2.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
unbdqndv2lem2.2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
unbdqndv2lem2.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝑉 )
unbdqndv2lem2.4 ⊢ ( 𝜑 → ( 𝑉 − 𝑈 ) < 𝐷 )
unbdqndv2lem2.5 ⊢ ( 𝜑 → ( 2 · 𝐵 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( 𝑉 − 𝑈 ) ) )
Assertion unbdqndv2lem2 ( 𝜑 → ( 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) ∧ ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2lem2.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) )
2 unbdqndv2lem2.w ⊢ 𝑊 = if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 )
3 unbdqndv2lem2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
4 unbdqndv2lem2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 unbdqndv2lem2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
6 unbdqndv2lem2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
7 unbdqndv2lem2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
8 unbdqndv2lem2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
9 unbdqndv2lem2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑋 )
10 unbdqndv2lem2.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
11 unbdqndv2lem2.2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
12 unbdqndv2lem2.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝑉 )
13 unbdqndv2lem2.4 ⊢ ( 𝜑 → ( 𝑉 − 𝑈 ) < 𝐷 )
14 unbdqndv2lem2.5 ⊢ ( 𝜑 → ( 2 · 𝐵 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( 𝑉 − 𝑈 ) ) )
15 2 a1i ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 = if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 ) )
16 iftrue ⊢ ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) → if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 ) = 𝑈 )
17 16 adantl ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 ) = 𝑈 )
18 15 17 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 = 𝑈 )
19 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 ∈ 𝑋 )
20 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑈 = 𝐴 ) → ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
21 fveq2 ⊢ ( 𝑈 = 𝐴 → ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝐴 ) )
22 21 eqcomd ⊢ ( 𝑈 = 𝐴 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝑈 ) )
23 22 oveq2d ⊢ ( 𝑈 = 𝐴 → ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) )
24 23 fveq2d ⊢ ( 𝑈 = 𝐴 → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑈 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) ) )
26 4 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) ∈ ℂ )
27 26 subidd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) = 0 )
28 27 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) ) = ( abs ‘ 0 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) ) = ( abs ‘ 0 ) )
30 abs0 ⊢ ( abs ‘ 0 ) = 0
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑈 = 𝐴 ) → ( abs ‘ 0 ) = 0 )
32 29 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝑈 ) ) ) = 0 )
33 25 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) = 0 )
34 33 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑈 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) = 0 )
35 20 34 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑈 = 𝐴 ) → ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 )
36 6 rpred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
37 3 9 sseldd ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
38 3 8 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
39 37 38 resubcld ⊢ ( 𝜑 → ( 𝑉 − 𝑈 ) ∈ ℝ )
40 6 rpgt0d ⊢ ( 𝜑 → 0 < 𝐵 )
41 3 5 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
42 38 41 37 11 12 letrd ⊢ ( 𝜑 → 𝑈 ≤ 𝑉 )
43 10 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
44 38 37 42 43 leneltd ⊢ ( 𝜑 → 𝑈 < 𝑉 )
45 38 37 posdifd ⊢ ( 𝜑 → ( 𝑈 < 𝑉 ↔ 0 < ( 𝑉 − 𝑈 ) ) )
46 44 45 mpbid ⊢ ( 𝜑 → 0 < ( 𝑉 − 𝑈 ) )
47 36 39 40 46 mulgt0d ⊢ ( 𝜑 → 0 < ( 𝐵 · ( 𝑉 − 𝑈 ) ) )
48 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
49 36 39 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝑉 − 𝑈 ) ) ∈ ℝ )
50 48 49 ltnled ⊢ ( 𝜑 → ( 0 < ( 𝐵 · ( 𝑉 − 𝑈 ) ) ↔ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 ) )
51 47 50 mpbid ⊢ ( 𝜑 → ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑈 = 𝐴 ) → ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 )
54 35 53 pm2.65da ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ 𝑈 = 𝐴 )
55 54 neqned ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 ≠ 𝐴 )
56 19 55 jca ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴 ) )
57 eldifsn ⊢ ( 𝑈 ∈ ( 𝑋 ∖ { 𝐴 } ) ↔ ( 𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴 ) )
58 56 57 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 ∈ ( 𝑋 ∖ { 𝐴 } ) )
59 18 58 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) )
60 18 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑊 − 𝐴 ) = ( 𝑈 − 𝐴 ) )
61 60 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) = ( abs ‘ ( 𝑈 − 𝐴 ) ) )
62 38 41 11 abssuble0d ⊢ ( 𝜑 → ( abs ‘ ( 𝑈 − 𝐴 ) ) = ( 𝐴 − 𝑈 ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑈 − 𝐴 ) ) = ( 𝐴 − 𝑈 ) )
64 61 63 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) = ( 𝐴 − 𝑈 ) )
65 41 38 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑈 ) ∈ ℝ )
66 7 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
67 41 37 38 12 lesub1dd ⊢ ( 𝜑 → ( 𝐴 − 𝑈 ) ≤ ( 𝑉 − 𝑈 ) )
68 65 39 66 67 13 lelttrd ⊢ ( 𝜑 → ( 𝐴 − 𝑈 ) < 𝐷 )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐴 − 𝑈 ) < 𝐷 )
70 64 69 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 )
71 36 65 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 − 𝑈 ) ) ∈ ℝ )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( 𝐴 − 𝑈 ) ) ∈ ℝ )
73 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( 𝑉 − 𝑈 ) ) ∈ ℝ )
74 4 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
75 26 74 subcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
76 75 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
77 76 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
78 48 36 40 ltled ⊢ ( 𝜑 → 0 ≤ 𝐵 )
79 65 39 36 78 67 lemul2ad ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 − 𝑈 ) ) ≤ ( 𝐵 · ( 𝑉 − 𝑈 ) ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( 𝐴 − 𝑈 ) ) ≤ ( 𝐵 · ( 𝑉 − 𝑈 ) ) )
81 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
82 72 73 77 80 81 letrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( 𝐴 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
83 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ∈ ℝ )
84 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐴 − 𝑈 ) ∈ ℝ )
85 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 ≤ 𝐴 )
86 55 necomd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐴 ≠ 𝑈 )
87 85 86 jca ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈 ) )
88 38 41 ltlend ⊢ ( 𝜑 → ( 𝑈 < 𝐴 ↔ ( 𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈 ) ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 < 𝐴 ↔ ( 𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈 ) ) )
90 87 89 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 < 𝐴 )
91 38 41 posdifd ⊢ ( 𝜑 → ( 𝑈 < 𝐴 ↔ 0 < ( 𝐴 − 𝑈 ) ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 < 𝐴 ↔ 0 < ( 𝐴 − 𝑈 ) ) )
93 90 92 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 0 < ( 𝐴 − 𝑈 ) )
94 84 93 jca ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 − 𝑈 ) ∈ ℝ ∧ 0 < ( 𝐴 − 𝑈 ) ) )
95 elrp ⊢ ( ( 𝐴 − 𝑈 ) ∈ ℝ+ ↔ ( ( 𝐴 − 𝑈 ) ∈ ℝ ∧ 0 < ( 𝐴 − 𝑈 ) ) )
96 94 95 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐴 − 𝑈 ) ∈ ℝ+ )
97 83 77 96 lemuldivd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐵 · ( 𝐴 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ↔ 𝐵 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) ) )
98 82 97 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) )
99 18 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑊 ) = ( 𝐺 ‘ 𝑈 ) )
100 fveq2 ⊢ ( 𝑧 = 𝑈 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑈 ) )
101 100 oveq1d ⊢ ( 𝑧 = 𝑈 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) )
102 oveq1 ⊢ ( 𝑧 = 𝑈 → ( 𝑧 − 𝐴 ) = ( 𝑈 − 𝐴 ) )
103 101 102 oveq12d ⊢ ( 𝑧 = 𝑈 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) = ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) )
104 ovexd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) ∈ V )
105 1 103 58 104 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑈 ) = ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) )
106 99 105 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑊 ) = ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) )
107 106 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) ) )
108 75 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
109 38 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
110 41 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
111 109 110 subcld ⊢ ( 𝜑 → ( 𝑈 − 𝐴 ) ∈ ℂ )
112 111 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 − 𝐴 ) ∈ ℂ )
113 109 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑈 ∈ ℂ )
114 110 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐴 ∈ ℂ )
115 113 114 55 subne0d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑈 − 𝐴 ) ≠ 0 )
116 108 112 115 absdivd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑈 − 𝐴 ) ) ) )
117 63 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑈 − 𝐴 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) )
118 116 117 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑈 − 𝐴 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) )
119 107 118 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) )
120 119 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( 𝐴 − 𝑈 ) ) = ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) )
121 98 120 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) )
122 70 121 jca ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) )
123 59 122 jca ⊢ ( ( 𝜑 ∧ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) ∧ ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) ) )
124 2 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 = if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 ) )
125 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
126 125 iffalsed ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → if ( ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑈 , 𝑉 ) = 𝑉 )
127 124 126 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 = 𝑉 )
128 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑉 ∈ 𝑋 )
129 38 37 42 abssubge0d ⊢ ( 𝜑 → ( abs ‘ ( 𝑉 − 𝑈 ) ) = ( 𝑉 − 𝑈 ) )
130 129 oveq2d ⊢ ( 𝜑 → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) = ( 𝐵 · ( 𝑉 − 𝑈 ) ) )
131 130 breq1d ⊢ ( 𝜑 → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ↔ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) )
132 131 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ↔ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) )
133 125 132 mtbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
134 4 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) ∈ ℂ )
135 39 recnd ⊢ ( 𝜑 → ( 𝑉 − 𝑈 ) ∈ ℂ )
136 48 46 gtned ⊢ ( 𝜑 → ( 𝑉 − 𝑈 ) ≠ 0 )
137 134 26 subcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ∈ ℂ )
138 137 135 136 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑉 − 𝑈 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( abs ‘ ( 𝑉 − 𝑈 ) ) ) )
139 129 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( abs ‘ ( 𝑉 − 𝑈 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( 𝑉 − 𝑈 ) ) )
140 138 139 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑉 − 𝑈 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( 𝑉 − 𝑈 ) ) )
141 140 eqcomd ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) ) / ( 𝑉 − 𝑈 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑉 − 𝑈 ) ) ) )
142 14 141 breqtrd ⊢ ( 𝜑 → ( 2 · 𝐵 ) ≤ ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑉 − 𝑈 ) ) ) )
143 134 26 74 135 6 136 142 unbdqndv2lem1 ⊢ ( 𝜑 → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∨ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) )
144 143 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∨ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) )
145 orel2 ⊢ ( ¬ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) → ( ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∨ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) )
146 133 144 145 sylc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑉 = 𝐴 ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
148 fveq2 ⊢ ( 𝑉 = 𝐴 → ( 𝐹 ‘ 𝑉 ) = ( 𝐹 ‘ 𝐴 ) )
149 148 oveq1d ⊢ ( 𝑉 = 𝐴 → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐴 ) ) )
150 149 adantl ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐴 ) ) )
151 74 subidd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐴 ) ) = 0 )
152 151 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐴 ) ) = 0 )
153 150 152 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) = 0 )
154 153 fveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) = ( abs ‘ 0 ) )
155 30 a1i ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( abs ‘ 0 ) = 0 )
156 154 155 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) = 0 )
157 156 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑉 = 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) = 0 )
158 147 157 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑉 = 𝐴 ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ 0 )
159 130 breq1d ⊢ ( 𝜑 → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ 0 ↔ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ 0 ) )
160 51 159 mtbird ⊢ ( 𝜑 → ¬ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ 0 )
161 160 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ 0 )
162 161 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) ∧ 𝑉 = 𝐴 ) → ¬ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ≤ 0 )
163 158 162 pm2.65da ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ¬ 𝑉 = 𝐴 )
164 163 neqned ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑉 ≠ 𝐴 )
165 128 164 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴 ) )
166 eldifsn ⊢ ( 𝑉 ∈ ( 𝑋 ∖ { 𝐴 } ) ↔ ( 𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴 ) )
167 165 166 sylibr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑉 ∈ ( 𝑋 ∖ { 𝐴 } ) )
168 127 167 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) )
169 127 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑊 − 𝐴 ) = ( 𝑉 − 𝐴 ) )
170 169 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) = ( abs ‘ ( 𝑉 − 𝐴 ) ) )
171 41 37 12 abssubge0d ⊢ ( 𝜑 → ( abs ‘ ( 𝑉 − 𝐴 ) ) = ( 𝑉 − 𝐴 ) )
172 171 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑉 − 𝐴 ) ) = ( 𝑉 − 𝐴 ) )
173 170 172 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) = ( 𝑉 − 𝐴 ) )
174 37 41 resubcld ⊢ ( 𝜑 → ( 𝑉 − 𝐴 ) ∈ ℝ )
175 38 41 37 11 lesub2dd ⊢ ( 𝜑 → ( 𝑉 − 𝐴 ) ≤ ( 𝑉 − 𝑈 ) )
176 174 39 66 175 13 lelttrd ⊢ ( 𝜑 → ( 𝑉 − 𝐴 ) < 𝐷 )
177 176 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑉 − 𝐴 ) < 𝐷 )
178 173 177 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 )
179 171 174 eqeltrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑉 − 𝐴 ) ) ∈ ℝ )
180 36 179 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ∈ ℝ )
181 180 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ∈ ℝ )
182 130 49 eqeltrd ⊢ ( 𝜑 → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ∈ ℝ )
183 182 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) ∈ ℝ )
184 134 74 subcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
185 184 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
186 185 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ )
187 129 39 eqeltrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑉 − 𝑈 ) ) ∈ ℝ )
188 175 171 129 3brtr4d ⊢ ( 𝜑 → ( abs ‘ ( 𝑉 − 𝐴 ) ) ≤ ( abs ‘ ( 𝑉 − 𝑈 ) ) )
189 179 187 36 78 188 lemul2ad ⊢ ( 𝜑 → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ≤ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) )
190 189 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ≤ ( 𝐵 · ( abs ‘ ( 𝑉 − 𝑈 ) ) ) )
191 181 183 186 190 146 letrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
192 36 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ∈ ℝ )
193 174 recnd ⊢ ( 𝜑 → ( 𝑉 − 𝐴 ) ∈ ℂ )
194 193 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑉 − 𝐴 ) ∈ ℂ )
195 37 recnd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
196 195 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝑉 ∈ ℂ )
197 110 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐴 ∈ ℂ )
198 196 197 164 subne0d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑉 − 𝐴 ) ≠ 0 )
199 194 198 absrpcld ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝑉 − 𝐴 ) ) ∈ ℝ+ )
200 192 186 199 lemuldivd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐵 · ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) ↔ 𝐵 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑉 − 𝐴 ) ) ) ) )
201 191 200 mpbid ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑉 − 𝐴 ) ) ) )
202 127 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑊 ) = ( 𝐺 ‘ 𝑉 ) )
203 fveq2 ⊢ ( 𝑧 = 𝑉 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑉 ) )
204 203 oveq1d ⊢ ( 𝑧 = 𝑉 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) )
205 oveq1 ⊢ ( 𝑧 = 𝑉 → ( 𝑧 − 𝐴 ) = ( 𝑉 − 𝐴 ) )
206 204 205 oveq12d ⊢ ( 𝑧 = 𝑉 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) = ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) )
207 ovexd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) ∈ V )
208 1 206 167 207 fvmptd3 ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑉 ) = ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) )
209 202 208 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝐺 ‘ 𝑊 ) = ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) )
210 209 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) ) )
211 184 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
212 211 194 198 absdivd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑉 − 𝐴 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑉 − 𝐴 ) ) ) )
213 210 212 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑉 − 𝐴 ) ) ) )
214 213 eqcomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑉 ) − ( 𝐹 ‘ 𝐴 ) ) ) / ( abs ‘ ( 𝑉 − 𝐴 ) ) ) = ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) )
215 201 214 breqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) )
216 178 215 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) )
217 168 216 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 · ( 𝑉 − 𝑈 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑈 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) → ( 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) ∧ ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) ) )
218 123 217 pm2.61dan ⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝑋 ∖ { 𝐴 } ) ∧ ( ( abs ‘ ( 𝑊 − 𝐴 ) ) < 𝐷 ∧ 𝐵 ≤ ( abs ‘ ( 𝐺 ‘ 𝑊 ) ) ) ) )