Metamath Proof Explorer

Theorem dvivth

Description: Darboux' theorem, or the intermediate value theorem for derivatives. A differentiable function's derivative satisfies the intermediate value property, even though it may not be continuous (so that ivthicc does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvivth.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
dvivth.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
dvivth.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
dvivth.4 ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
Assertion dvivth ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ran ( ℝ D 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dvivth.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
2 dvivth.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
3 dvivth.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
4 dvivth.4 ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
7 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
8 3 7 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
9 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
10 9 renegcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
11 10 fmpttd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
12 ax-resscn ⊢ ℝ ⊆ ℂ
13 ssid ⊢ ℂ ⊆ ℂ
14 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
15 12 13 14 mp2an ⊢ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ )
16 15 3 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
17 eqid ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) )
18 17 negfcncf ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
19 16 18 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
20 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
21 12 19 20 sylancr ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
22 11 21 mpbird ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
24 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
25 24 a1i ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ℝ ∈ { ℝ , ℂ } )
26 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
27 26 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
28 27 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℂ )
29 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ V )
30 26 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝐹 = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑤 ) ) )
31 30 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑤 ) ) ) )
32 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
33 dvfre ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
34 8 32 33 sylancl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
35 4 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
36 34 35 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
38 37 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D 𝐹 ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
39 31 38 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
40 25 28 29 39 dvmptneg ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
41 40 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → dom ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) = dom ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
42 dmmptg ⊢ ( ∀ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ V → dom ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) = ( 𝐴 (,) 𝐵 ) )
43 negex ⊢ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ V
44 43 a1i ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ V )
45 42 44 mprg ⊢ dom ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) = ( 𝐴 (,) 𝐵 )
46 41 45 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → dom ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) = ( 𝐴 (,) 𝐵 ) )
47 simprl ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑀 < 𝑁 )
48 simprr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) )
49 36 1 ffvelrnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
51 2 4 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom ( ℝ D 𝐹 ) )
52 34 51 ffvelrnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
53 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
54 iccssre ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ℝ )
55 49 52 54 syl2anc ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ℝ )
57 56 48 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ℝ )
58 iccneg ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ↔ - 𝑥 ∈ ( - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
59 50 53 57 58 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ↔ - 𝑥 ∈ ( - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
60 48 59 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → - 𝑥 ∈ ( - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
61 40 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑁 ) = ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑁 ) )
62 fveq2 ⊢ ( 𝑤 = 𝑁 → ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
63 62 negeqd ⊢ ( 𝑤 = 𝑁 → - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
64 eqid ⊢ ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
65 negex ⊢ - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ V
66 63 64 65 fvmpt ⊢ ( 𝑁 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑁 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
67 6 66 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑁 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
68 61 67 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑁 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
69 40 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑀 ) = ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑀 ) )
70 fveq2 ⊢ ( 𝑤 = 𝑀 → ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
71 70 negeqd ⊢ ( 𝑤 = 𝑀 → - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
72 negex ⊢ - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ V
73 71 64 72 fvmpt ⊢ ( 𝑀 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑀 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
74 5 73 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ‘ 𝑀 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
75 69 74 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑀 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
76 68 75 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑁 ) [,] ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑀 ) ) = ( - ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] - ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
77 60 76 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → - 𝑥 ∈ ( ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑁 ) [,] ( ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) ‘ 𝑀 ) ) )
78 eqid ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑦 ) − ( - 𝑥 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑦 ) − ( - 𝑥 · 𝑦 ) ) )
79 5 6 23 46 47 77 78 dvivthlem2 ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → - 𝑥 ∈ ran ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) )
80 40 rneqd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ran ( ℝ D ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑤 ) ) ) = ran ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
81 79 80 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → - 𝑥 ∈ ran ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
82 negex ⊢ - 𝑥 ∈ V
83 64 elrnmpt ⊢ ( - 𝑥 ∈ V → ( - 𝑥 ∈ ran ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
84 82 83 ax-mp ⊢ ( - 𝑥 ∈ ran ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
85 81 84 sylib ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) )
86 57 recnd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ℂ )
87 86 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℂ )
88 25 28 29 39 dvmptcl ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ∈ ℂ )
89 87 88 neg11ad ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ↔ 𝑥 = ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) )
90 eqcom ⊢ ( 𝑥 = ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ↔ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 )
91 89 90 bitrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) ∧ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ↔ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 ) )
92 91 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) - 𝑥 = - ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 ) )
93 85 92 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 )
94 37 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) )
95 fvelrnb ⊢ ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 ) )
96 94 95 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ ∃ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑤 ) = 𝑥 ) )
97 93 96 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑀 < 𝑁 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ran ( ℝ D 𝐹 ) )
98 97 expr ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑁 ) → ( 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) → 𝑥 ∈ ran ( ℝ D 𝐹 ) ) )
99 98 ssrdv ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑁 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ran ( ℝ D 𝐹 ) )
100 fveq2 ⊢ ( 𝑀 = 𝑁 → ( ( ℝ D 𝐹 ) ‘ 𝑀 ) = ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
101 100 oveq1d ⊢ ( 𝑀 = 𝑁 → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) )
102 52 rexrd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ* )
103 iccid ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ* → ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) = { ( ( ℝ D 𝐹 ) ‘ 𝑁 ) } )
104 102 103 syl ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) = { ( ( ℝ D 𝐹 ) ‘ 𝑁 ) } )
105 101 104 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑁 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) = { ( ( ℝ D 𝐹 ) ‘ 𝑁 ) } )
106 34 ffnd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) Fn dom ( ℝ D 𝐹 ) )
107 fnfvelrn ⊢ ( ( ( ℝ D 𝐹 ) Fn dom ( ℝ D 𝐹 ) ∧ 𝑁 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ran ( ℝ D 𝐹 ) )
108 106 51 107 syl2anc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ran ( ℝ D 𝐹 ) )
109 108 snssd ⊢ ( 𝜑 → { ( ( ℝ D 𝐹 ) ‘ 𝑁 ) } ⊆ ran ( ℝ D 𝐹 ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑁 ) → { ( ( ℝ D 𝐹 ) ‘ 𝑁 ) } ⊆ ran ( ℝ D 𝐹 ) )
111 105 110 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑁 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ran ( ℝ D 𝐹 ) )
112 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
113 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
114 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
115 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
116 simprl ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑁 < 𝑀 )
117 simprr ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) )
118 eqid ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝑥 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝑥 · 𝑦 ) ) )
119 112 113 114 115 116 117 118 dvivthlem2 ⊢ ( ( 𝜑 ∧ ( 𝑁 < 𝑀 ∧ 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ran ( ℝ D 𝐹 ) )
120 119 expr ⊢ ( ( 𝜑 ∧ 𝑁 < 𝑀 ) → ( 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) → 𝑥 ∈ ran ( ℝ D 𝐹 ) ) )
121 120 ssrdv ⊢ ( ( 𝜑 ∧ 𝑁 < 𝑀 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ran ( ℝ D 𝐹 ) )
122 32 1 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
123 32 2 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
124 122 123 lttri4d ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) )
125 99 111 121 124 mpjao3dan ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑀 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ) ⊆ ran ( ℝ D 𝐹 ) )