This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvferm1lem

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 𝐹 ) )
dvferm1.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑈 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
dvferm1.z ⊢ ( 𝜑 → 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
dvferm1.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
dvferm1.l ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑇 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
dvferm1.x ⊢ 𝑆 = ( ( 𝑈 + if ( 𝐵 ≤ ( 𝑈 + 𝑇 ) , 𝐵 , ( 𝑈 + 𝑇 ) ) ) / 2 )
Assertion dvferm1lem ¬ 𝜑

Proof

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