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 
|- ( ph -> M e. ( A (,) B ) )
dvivth.2 
|- ( ph -> N e. ( A (,) B ) )
dvivth.3 
|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
dvivth.4 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
Assertion dvivth 
|- ( ph -> ( ( ( RR _D F ) ` M ) [,] ( ( RR _D F ) ` N ) ) C_ ran ( RR _D F ) )

Proof

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