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 
|- ( ph -> A e. RR )
dvne0.b 
|- ( ph -> B e. RR )
dvne0.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
dvne0.d 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvne0.z 
|- ( ph -> -. 0 e. ran ( RR _D F ) )
Assertion dvne0 
|- ( ph -> ( F Isom < , < ( ( A [,] B ) , ran F ) \/ F Isom < , `' < ( ( A [,] B ) , ran F ) ) )

Proof

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