Metamath Proof Explorer

Theorem dvferm2lem

Description: Lemma for dvferm . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvferm.a ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
dvferm.b ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
dvferm.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
dvferm.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
dvferm.d ⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
dvferm2.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
dvferm2.z ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 )
dvferm2.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
dvferm2.l ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
dvferm2.x ⊢ 𝑆 = ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 )
Assertion dvferm2lem ¬ 𝜑

Proof

Step Hyp Ref Expression
1 dvferm.a ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
2 dvferm.b ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
3 dvferm.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
4 dvferm.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
5 dvferm.d ⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
6 dvferm2.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
7 dvferm2.z ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 )
8 dvferm2.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
9 dvferm2.l ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
10 dvferm2.x ⊢ 𝑆 = ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 )
11 mnfxr ⊢ -∞ ∈ ℝ*
12 11 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
13 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
14 13 3 sseldi ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
15 8 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
16 14 15 resubcld ⊢ ( 𝜑 → ( 𝑈 − 𝑇 ) ∈ ℝ )
17 16 rexrd ⊢ ( 𝜑 → ( 𝑈 − 𝑇 ) ∈ ℝ* )
18 ne0i ⊢ ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
19 ndmioo ⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )
20 19 necon1ai ⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
21 3 18 20 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
22 21 simpld ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
23 17 22 ifcld ⊢ ( 𝜑 → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ* )
24 14 rexrd ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
25 16 mnfltd ⊢ ( 𝜑 → -∞ < ( 𝑈 − 𝑇 ) )
26 xrmax2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝑈 − 𝑇 ) ∈ ℝ* ) → ( 𝑈 − 𝑇 ) ≤ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) )
27 22 17 26 syl2anc ⊢ ( 𝜑 → ( 𝑈 − 𝑇 ) ≤ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) )
28 12 17 23 25 27 xrltletrd ⊢ ( 𝜑 → -∞ < if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) )
29 14 8 ltsubrpd ⊢ ( 𝜑 → ( 𝑈 − 𝑇 ) < 𝑈 )
30 eliooord ⊢ ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑈 ∧ 𝑈 < 𝐵 ) )
31 3 30 syl ⊢ ( 𝜑 → ( 𝐴 < 𝑈 ∧ 𝑈 < 𝐵 ) )
32 31 simpld ⊢ ( 𝜑 → 𝐴 < 𝑈 )
33 breq1 ⊢ ( ( 𝑈 − 𝑇 ) = if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) → ( ( 𝑈 − 𝑇 ) < 𝑈 ↔ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ) )
34 breq1 ⊢ ( 𝐴 = if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) → ( 𝐴 < 𝑈 ↔ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ) )
35 33 34 ifboth ⊢ ( ( ( 𝑈 − 𝑇 ) < 𝑈 ∧ 𝐴 < 𝑈 ) → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 )
36 29 32 35 syl2anc ⊢ ( 𝜑 → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 )
37 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ* ∧ 𝑈 ∈ ℝ* ) ∧ ( -∞ < if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∧ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ) ) → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ )
38 12 23 24 28 36 37 syl32anc ⊢ ( 𝜑 → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ )
39 38 14 readdcld ⊢ ( 𝜑 → ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) ∈ ℝ )
40 39 rehalfcld ⊢ ( 𝜑 → ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) ∈ ℝ )
41 10 40 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
42 avglt2 ⊢ ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ↔ ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) < 𝑈 ) )
43 38 14 42 syl2anc ⊢ ( 𝜑 → ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ↔ ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) < 𝑈 ) )
44 36 43 mpbid ⊢ ( 𝜑 → ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) < 𝑈 )
45 10 44 eqbrtrid ⊢ ( 𝜑 → 𝑆 < 𝑈 )
46 41 45 ltned ⊢ ( 𝜑 → 𝑆 ≠ 𝑈 )
47 41 14 45 ltled ⊢ ( 𝜑 → 𝑆 ≤ 𝑈 )
48 41 14 47 abssuble0d ⊢ ( 𝜑 → ( abs ‘ ( 𝑆 − 𝑈 ) ) = ( 𝑈 − 𝑆 ) )
49 avglt1 ⊢ ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ↔ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) ) )
50 38 14 49 syl2anc ⊢ ( 𝜑 → ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑈 ↔ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) ) )
51 36 50 mpbid ⊢ ( 𝜑 → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) + 𝑈 ) / 2 ) )
52 51 10 breqtrrdi ⊢ ( 𝜑 → if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) < 𝑆 )
53 16 38 41 27 52 lelttrd ⊢ ( 𝜑 → ( 𝑈 − 𝑇 ) < 𝑆 )
54 14 15 41 53 ltsub23d ⊢ ( 𝜑 → ( 𝑈 − 𝑆 ) < 𝑇 )
55 48 54 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑆 − 𝑈 ) ) < 𝑇 )
56 neeq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈 ) )
57 fvoveq1 ⊢ ( 𝑧 = 𝑆 → ( abs ‘ ( 𝑧 − 𝑈 ) ) = ( abs ‘ ( 𝑆 − 𝑈 ) ) )
58 57 breq1d ⊢ ( 𝑧 = 𝑆 → ( ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ↔ ( abs ‘ ( 𝑆 − 𝑈 ) ) < 𝑇 ) )
59 56 58 anbi12d ⊢ ( 𝑧 = 𝑆 → ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ) ↔ ( 𝑆 ≠ 𝑈 ∧ ( abs ‘ ( 𝑆 − 𝑈 ) ) < 𝑇 ) ) )
60 fveq2 ⊢ ( 𝑧 = 𝑆 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑆 ) )
61 60 oveq1d ⊢ ( 𝑧 = 𝑆 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) = ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) )
62 oveq1 ⊢ ( 𝑧 = 𝑆 → ( 𝑧 − 𝑈 ) = ( 𝑆 − 𝑈 ) )
63 61 62 oveq12d ⊢ ( 𝑧 = 𝑆 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) = ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) )
64 63 fvoveq1d ⊢ ( 𝑧 = 𝑆 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
65 64 breq1d ⊢ ( 𝑧 = 𝑆 → ( ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ↔ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
66 59 65 imbi12d ⊢ ( 𝑧 = 𝑆 → ( ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ↔ ( ( 𝑆 ≠ 𝑈 ∧ ( abs ‘ ( 𝑆 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
67 21 simprd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
68 31 simprd ⊢ ( 𝜑 → 𝑈 < 𝐵 )
69 24 67 68 xrltled ⊢ ( 𝜑 → 𝑈 ≤ 𝐵 )
70 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑈 ≤ 𝐵 ) → ( 𝐴 (,) 𝑈 ) ⊆ ( 𝐴 (,) 𝐵 ) )
71 67 69 70 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑈 ) ⊆ ( 𝐴 (,) 𝐵 ) )
72 71 4 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝑈 ) ⊆ 𝑋 )
73 41 rexrd ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
74 xrmax1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝑈 − 𝑇 ) ∈ ℝ* ) → 𝐴 ≤ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) )
75 22 17 74 syl2anc ⊢ ( 𝜑 → 𝐴 ≤ if ( 𝐴 ≤ ( 𝑈 − 𝑇 ) , ( 𝑈 − 𝑇 ) , 𝐴 ) )
76 22 23 73 75 52 xrlelttrd ⊢ ( 𝜑 → 𝐴 < 𝑆 )
77 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑈 ∈ ℝ* ) → ( 𝑆 ∈ ( 𝐴 (,) 𝑈 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈 ) ) )
78 22 24 77 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐴 (,) 𝑈 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈 ) ) )
79 41 76 45 78 mpbir3and ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐴 (,) 𝑈 ) )
80 72 79 sseldd ⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
81 eldifsn ⊢ ( 𝑆 ∈ ( 𝑋 ∖ { 𝑈 } ) ↔ ( 𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈 ) )
82 80 46 81 sylanbrc ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑋 ∖ { 𝑈 } ) )
83 66 9 82 rspcdva ⊢ ( 𝜑 → ( ( 𝑆 ≠ 𝑈 ∧ ( abs ‘ ( 𝑆 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
84 46 55 83 mp2and ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
85 1 80 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ∈ ℝ )
86 4 3 sseldd ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
87 1 86 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) ∈ ℝ )
88 85 87 resubcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ∈ ℝ )
89 41 14 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑈 ) ∈ ℝ )
90 41 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
91 14 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
92 90 91 46 subne0d ⊢ ( 𝜑 → ( 𝑆 − 𝑈 ) ≠ 0 )
93 88 89 92 redivcld ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) ∈ ℝ )
94 dvfre ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
95 1 2 94 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
96 95 5 ffvelrnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
97 96 renegcld ⊢ ( 𝜑 → - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
98 93 96 97 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ↔ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) − - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) < ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) ∧ ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) < ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) + - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) ) )
99 84 98 mpbid ⊢ ( 𝜑 → ( ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) − - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) < ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) ∧ ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) < ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) + - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
100 99 simprd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) < ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) + - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
101 96 recnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℂ )
102 101 negidd ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) + - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) = 0 )
103 100 102 breqtrd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) < 0 )
104 93 lt0neg1d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) < 0 ↔ 0 < - ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) ) )
105 103 104 mpbid ⊢ ( 𝜑 → 0 < - ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) )
106 88 recnd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ∈ ℂ )
107 89 recnd ⊢ ( 𝜑 → ( 𝑆 − 𝑈 ) ∈ ℂ )
108 106 107 92 divneg2d ⊢ ( 𝜑 → - ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑆 − 𝑈 ) ) = ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / - ( 𝑆 − 𝑈 ) ) )
109 105 108 breqtrd ⊢ ( 𝜑 → 0 < ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / - ( 𝑆 − 𝑈 ) ) )
110 89 renegcld ⊢ ( 𝜑 → - ( 𝑆 − 𝑈 ) ∈ ℝ )
111 41 14 posdifd ⊢ ( 𝜑 → ( 𝑆 < 𝑈 ↔ 0 < ( 𝑈 − 𝑆 ) ) )
112 45 111 mpbid ⊢ ( 𝜑 → 0 < ( 𝑈 − 𝑆 ) )
113 90 91 negsubdi2d ⊢ ( 𝜑 → - ( 𝑆 − 𝑈 ) = ( 𝑈 − 𝑆 ) )
114 112 113 breqtrrd ⊢ ( 𝜑 → 0 < - ( 𝑆 − 𝑈 ) )
115 gt0div ⊢ ( ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ∈ ℝ ∧ - ( 𝑆 − 𝑈 ) ∈ ℝ ∧ 0 < - ( 𝑆 − 𝑈 ) ) → ( 0 < ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ↔ 0 < ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / - ( 𝑆 − 𝑈 ) ) ) )
116 88 110 114 115 syl3anc ⊢ ( 𝜑 → ( 0 < ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ↔ 0 < ( ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) / - ( 𝑆 − 𝑈 ) ) ) )
117 109 116 mpbird ⊢ ( 𝜑 → 0 < ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) )
118 87 85 posdifd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑆 ) ↔ 0 < ( ( 𝐹 ‘ 𝑆 ) − ( 𝐹 ‘ 𝑈 ) ) ) )
119 117 118 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑆 ) )
120 fveq2 ⊢ ( 𝑦 = 𝑆 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑆 ) )
121 120 breq1d ⊢ ( 𝑦 = 𝑆 → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) ↔ ( 𝐹 ‘ 𝑆 ) ≤ ( 𝐹 ‘ 𝑈 ) ) )
122 121 6 79 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ≤ ( 𝐹 ‘ 𝑈 ) )
123 85 87 122 lensymd ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑆 ) )
124 119 123 pm2.65i ⊢ ¬ 𝜑