Metamath Proof Explorer

Theorem dvferm1

Description: One-sided version of dvferm . A point U which is the local maximum of its right neighborhood has derivative at most zero. (Contributed by Mario Carneiro, 24-Feb-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvferm.a ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
dvferm.b ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
dvferm.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
dvferm.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
dvferm.d ⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
dvferm1.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑈 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
Assertion dvferm1 ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 )

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 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
8 7 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 − 𝑈 ) = ( 𝑧 − 𝑈 ) )
10 8 9 oveq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) )
11 eqid ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) = ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) )
12 ovex ⊢ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) ∈ V
13 10 11 12 fvmpt ⊢ ( 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) → ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) )
14 13 fvoveq1d ⊢ ( 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
15 id ⊢ ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) → 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
16 14 15 breqan12rd ⊢ ( ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∧ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ) → ( ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
17 16 imbi2d ⊢ ( ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∧ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ) → ( ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ↔ ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
18 17 ralbidva ⊢ ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) → ( ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ↔ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
19 18 rexbidv ⊢ ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑈 ) → ( ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ↔ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
20 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
21 ffun ⊢ ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ → Fun ( ℝ D 𝐹 ) )
22 funfvbrb ⊢ ( Fun ( ℝ D 𝐹 ) → ( 𝑈 ∈ dom ( ℝ D 𝐹 ) ↔ 𝑈 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
23 20 21 22 mp2b ⊢ ( 𝑈 ∈ dom ( ℝ D 𝐹 ) ↔ 𝑈 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
24 5 23 sylib ⊢ ( 𝜑 → 𝑈 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
25 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
26 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 27 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
29 fss ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
30 1 27 29 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
31 25 26 11 28 30 2 eldv ⊢ ( 𝜑 → ( 𝑈 ( ℝ D 𝐹 ) ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ↔ ( 𝑈 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) ) ) )
32 24 31 mpbid ⊢ ( 𝜑 → ( 𝑈 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) ) )
33 32 simprd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) )
35 2 27 sstrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
36 4 3 sseldd ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
37 30 35 36 dvlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ∈ ℂ )
38 37 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) : ( 𝑋 ∖ { 𝑈 } ) ⟶ ℂ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) : ( 𝑋 ∖ { 𝑈 } ) ⟶ ℂ )
40 35 adantr ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → 𝑋 ⊆ ℂ )
41 40 ssdifssd ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( 𝑋 ∖ { 𝑈 } ) ⊆ ℂ )
42 35 36 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
43 42 adantr ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → 𝑈 ∈ ℂ )
44 39 41 43 ellimc3 ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ) ) )
45 34 44 mpbid ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ) )
46 45 simprd ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) )
47 dvfre ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
48 1 2 47 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
49 48 5 ffvelrnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
50 49 anim1i ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
51 elrp ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ+ ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
52 50 51 sylibr ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ+ )
53 19 46 52 rspcdva ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
54 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝐹 : 𝑋 ⟶ ℝ )
55 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑋 ⊆ ℝ )
56 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
57 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
58 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
59 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ∀ 𝑦 ∈ ( 𝑈 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
60 simpllr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
61 simplr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑢 ∈ ℝ+ )
62 simpr ⊢ ( ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
63 eqid ⊢ ( ( 𝑈 + if ( 𝐵 ≤ ( 𝑈 + 𝑢 ) , 𝐵 , ( 𝑈 + 𝑢 ) ) ) / 2 ) = ( ( 𝑈 + if ( 𝐵 ≤ ( 𝑈 + 𝑢 ) , 𝐵 , ( 𝑈 + 𝑢 ) ) ) / 2 )
64 54 55 56 57 58 59 60 61 62 63 dvferm1lem ⊢ ¬ ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
65 64 imnani ⊢ ( ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ∧ 𝑢 ∈ ℝ+ ) → ¬ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
66 65 nrexdv ⊢ ( ( 𝜑 ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) → ¬ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
67 53 66 pm2.65da ⊢ ( 𝜑 → ¬ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
68 0re ⊢ 0 ∈ ℝ
69 lenlt ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 ↔ ¬ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
70 49 68 69 sylancl ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 ↔ ¬ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
71 67 70 mpbird ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 )