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

Metamath Proof Explorer

Theorem dvne0

Description: A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvne0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvne0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvne0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvne0.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
dvne0.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
Assertion dvne0 ( 𝜑 → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 dvne0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvne0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvne0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvne0.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5 dvne0.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
6 eleq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ 0 ∈ ran ( ℝ D 𝐹 ) ) )
7 6 notbid ⊢ ( 𝑥 = 0 → ( ¬ 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ ¬ 0 ∈ ran ( ℝ D 𝐹 ) ) )
8 5 7 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = 0 → ¬ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) )
9 8 necon2ad ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) → 𝑥 ≠ 0 ) )
10 9 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → 𝑥 ≠ 0 )
11 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
12 3 11 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
13 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
15 dvfre ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
16 12 14 15 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
17 16 frnd ⊢ ( 𝜑 → ran ( ℝ D 𝐹 ) ⊆ ℝ )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → 𝑥 ∈ ℝ )
19 0re ⊢ 0 ∈ ℝ
20 lttri2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 < 0 ∨ 0 < 𝑥 ) ) )
21 18 19 20 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 < 0 ∨ 0 < 𝑥 ) ) )
22 0xr ⊢ 0 ∈ ℝ*
23 elioomnf ⊢ ( 0 ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) )
24 22 23 ax-mp ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) )
25 24 baib ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ 𝑥 < 0 ) )
26 elrp ⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
27 26 baib ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ℝ+ ↔ 0 < 𝑥 ) )
28 25 27 orbi12d ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ∈ ( -∞ (,) 0 ) ∨ 𝑥 ∈ ℝ+ ) ↔ ( 𝑥 < 0 ∨ 0 < 𝑥 ) ) )
29 18 28 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → ( ( 𝑥 ∈ ( -∞ (,) 0 ) ∨ 𝑥 ∈ ℝ+ ) ↔ ( 𝑥 < 0 ∨ 0 < 𝑥 ) ) )
30 21 29 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 ∈ ( -∞ (,) 0 ) ∨ 𝑥 ∈ ℝ+ ) ) )
31 10 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → ( 𝑥 ∈ ( -∞ (,) 0 ) ∨ 𝑥 ∈ ℝ+ ) )
32 elun ⊢ ( 𝑥 ∈ ( ( -∞ (,) 0 ) ∪ ℝ+ ) ↔ ( 𝑥 ∈ ( -∞ (,) 0 ) ∨ 𝑥 ∈ ℝ+ ) )
33 31 32 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ℝ D 𝐹 ) ) → 𝑥 ∈ ( ( -∞ (,) 0 ) ∪ ℝ+ ) )
34 33 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) → 𝑥 ∈ ( ( -∞ (,) 0 ) ∪ ℝ+ ) ) )
35 34 ssrdv ⊢ ( 𝜑 → ran ( ℝ D 𝐹 ) ⊆ ( ( -∞ (,) 0 ) ∪ ℝ+ ) )
36 disjssun ⊢ ( ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) = ∅ → ( ran ( ℝ D 𝐹 ) ⊆ ( ( -∞ (,) 0 ) ∪ ℝ+ ) ↔ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) )
37 35 36 syl5ibcom ⊢ ( 𝜑 → ( ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) = ∅ → ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) )
38 37 imp ⊢ ( ( 𝜑 ∧ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) = ∅ ) → ran ( ℝ D 𝐹 ) ⊆ ℝ+ )
39 1 adantr ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → 𝐴 ∈ ℝ )
40 2 adantr ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → 𝐵 ∈ ℝ )
41 3 adantr ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
42 4 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
43 16 42 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
44 43 ffnd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) )
45 44 anim1i ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) )
46 df-f ⊢ ( ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ+ ↔ ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) )
47 45 46 sylibr ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ+ )
48 39 40 41 47 dvgt0 ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )
49 48 orcd ⊢ ( ( 𝜑 ∧ ran ( ℝ D 𝐹 ) ⊆ ℝ+ ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
50 38 49 syldan ⊢ ( ( 𝜑 ∧ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) = ∅ ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
51 n0 ⊢ ( ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) )
52 elin ⊢ ( 𝑥 ∈ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) ↔ ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ∧ 𝑥 ∈ ( -∞ (,) 0 ) ) )
53 fvelrnb ⊢ ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 ) )
54 44 53 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ↔ ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 ) )
55 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → 𝐴 ∈ ℝ )
56 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → 𝐵 ∈ ℝ )
57 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
58 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) )
59 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
60 59 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
61 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
62 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
63 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
64 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
65 rescncf ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ) )
66 64 3 65 mpsyl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
68 ax-resscn ⊢ ℝ ⊆ ℂ
69 68 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
70 fss ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
71 12 68 70 sylancl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
72 64 14 sstrid ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
73 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
74 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
75 73 74 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) )
76 69 71 14 72 75 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) )
77 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
78 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
79 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
80 77 78 79 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )
81 80 reseq2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) )
82 fnresdm ⊢ ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ℝ D 𝐹 ) )
83 44 82 syl ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ℝ D 𝐹 ) )
84 81 83 eqtrid ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) = ( ℝ D 𝐹 ) )
85 76 84 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ℝ D 𝐹 ) )
86 85 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = dom ( ℝ D 𝐹 ) )
87 86 4 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( 𝐴 (,) 𝐵 ) )
88 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → dom ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( 𝐴 (,) 𝐵 ) )
89 62 63 67 88 dvivth ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑦 ) [,] ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ⊆ ran ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) )
90 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( ℝ D 𝐹 ) )
91 90 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
92 90 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
93 91 92 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑦 ) [,] ( ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) ‘ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
94 90 rneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ran ( ℝ D ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ) = ran ( ℝ D 𝐹 ) )
95 89 93 94 3sstr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ⊆ ran ( ℝ D 𝐹 ) )
96 19 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 0 ∈ ℝ )
97 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) )
98 elioomnf ⊢ ( 0 ∈ ℝ* → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 ) ) )
99 22 98 ax-mp ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 ) )
100 97 99 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 ) )
101 100 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 )
102 100 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ )
103 ltle ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ≤ 0 ) )
104 102 19 103 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) < 0 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ≤ 0 ) )
105 101 104 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ≤ 0 )
106 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
107 63 60 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
108 elicc2 ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ ) → ( 0 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ↔ ( 0 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ≤ 0 ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) )
109 102 107 108 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → ( 0 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ↔ ( 0 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ≤ 0 ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) )
110 96 105 106 109 mpbir3and ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 0 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
111 95 110 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) → 0 ∈ ran ( ℝ D 𝐹 ) )
112 111 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) → 0 ∈ ran ( ℝ D 𝐹 ) ) )
113 61 112 mtod ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
114 ltnle ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) < 0 ↔ ¬ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
115 60 19 114 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) < 0 ↔ ¬ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
116 113 115 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) < 0 )
117 elioomnf ⊢ ( 0 ∈ ℝ* → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) < 0 ) ) )
118 22 117 ax-mp ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) < 0 ) )
119 60 116 118 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 0 ) )
120 119 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 0 ) )
121 ffnfv ⊢ ( ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( -∞ (,) 0 ) ↔ ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 0 ) ) )
122 58 120 121 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( -∞ (,) 0 ) )
123 55 56 57 122 dvlt0 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )
124 123 olcd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ) ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
125 124 expr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) )
126 eleq1 ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) ↔ 𝑥 ∈ ( -∞ (,) 0 ) ) )
127 126 imbi1d ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 → ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) ↔ ( 𝑥 ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) ) )
128 125 127 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 → ( 𝑥 ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) ) )
129 128 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 𝑥 → ( 𝑥 ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) ) )
130 54 129 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ℝ D 𝐹 ) → ( 𝑥 ∈ ( -∞ (,) 0 ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) ) )
131 130 impd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ran ( ℝ D 𝐹 ) ∧ 𝑥 ∈ ( -∞ (,) 0 ) ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) )
132 52 131 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) )
133 132 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) )
134 51 133 biimtrid ⊢ ( 𝜑 → ( ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) ≠ ∅ → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) ) )
135 134 imp ⊢ ( ( 𝜑 ∧ ( ran ( ℝ D 𝐹 ) ∩ ( -∞ (,) 0 ) ) ≠ ∅ ) → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
136 50 135 pm2.61dane ⊢ ( 𝜑 → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )