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

Metamath Proof Explorer

Theorem dvferm2

Description: One-sided version of dvferm . A point U which is the local maximum of its left neighborhood has derivative at least 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 𝐹 ) )
dvferm2.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
Assertion dvferm2 ( 𝜑 → 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )

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 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 ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) )
35 2 27 sstrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
36 4 3 sseldd ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
37 30 35 36 dvlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ∈ ℂ )
38 37 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) : ( 𝑋 ∖ { 𝑈 } ) ⟶ ℂ )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) : ( 𝑋 ∖ { 𝑈 } ) ⟶ ℂ )
40 35 adantr ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → 𝑋 ⊆ ℂ )
41 40 ssdifssd ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( 𝑋 ∖ { 𝑈 } ) ⊆ ℂ )
42 35 36 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → 𝑈 ∈ ℂ )
44 39 41 43 ellimc3 ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) limℂ 𝑈 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ) ) )
45 34 44 mpbid ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) ) )
46 45 simprd ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑋 ∖ { 𝑈 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑥 − 𝑈 ) ) ) ‘ 𝑧 ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < 𝑦 ) )
47 dvfre ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
48 1 2 47 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
49 48 5 ffvelcdmd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
51 50 renegcld ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
52 49 lt0neg1d ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ↔ 0 < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
53 52 biimpa ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → 0 < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
54 51 53 elrpd ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ+ )
55 19 46 54 rspcdva ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
56 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝐹 : 𝑋 ⟶ ℝ )
57 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑋 ⊆ ℝ )
58 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
59 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
60 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
61 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
62 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 )
63 simplr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → 𝑢 ∈ ℝ+ )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) → ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
65 eqid ⊢ ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑢 ) , ( 𝑈 − 𝑢 ) , 𝐴 ) + 𝑈 ) / 2 ) = ( ( if ( 𝐴 ≤ ( 𝑈 − 𝑢 ) , ( 𝑈 − 𝑢 ) , 𝐴 ) + 𝑈 ) / 2 )
66 56 57 58 59 60 61 62 63 64 65 dvferm2lem ⊢ ¬ ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
67 66 imnani ⊢ ( ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) ∧ 𝑢 ∈ ℝ+ ) → ¬ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
68 67 nrexdv ⊢ ( ( 𝜑 ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) → ¬ ∃ 𝑢 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝑋 ∖ { 𝑈 } ) ( ( 𝑧 ≠ 𝑈 ∧ ( abs ‘ ( 𝑧 − 𝑈 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑈 ) ) / ( 𝑧 − 𝑈 ) ) − ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) < - ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) )
69 55 68 pm2.65da ⊢ ( 𝜑 → ¬ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 )
70 0re ⊢ 0 ∈ ℝ
71 lenlt ⊢ ( ( 0 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ ) → ( 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ↔ ¬ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) )
72 70 49 71 sylancr ⊢ ( 𝜑 → ( 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ↔ ¬ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) < 0 ) )
73 69 72 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )