Metamath Proof Explorer

Theorem dvivthlem2

Description: Lemma for dvivth . (Contributed by Mario Carneiro, 20-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 ) )
dvivth.5 
|- ( ph -> M < N )
dvivth.6 
|- ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )
dvivth.7 
|- G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )
Assertion dvivthlem2 
|- ( ph -> C e. 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 dvivth.5 
 |-  ( ph -> M < N )
6 dvivth.6 
 |-  ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )
7 dvivth.7 
 |-  G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )
8 1 2 3 4 5 6 7 dvivthlem1 
 |-  ( ph -> E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C )
9 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
10 4 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
11 9 10 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
12 11 ffnd 
 |-  ( ph -> ( RR _D F ) Fn ( A (,) B ) )
13 iccssioo2 
 |-  ( ( M e. ( A (,) B ) /\ N e. ( A (,) B ) ) -> ( M [,] N ) C_ ( A (,) B ) )
14 1 2 13 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ ( A (,) B ) )
15 14 sselda 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> x e. ( A (,) B ) )
16 fnfvelrn 
 |-  ( ( ( RR _D F ) Fn ( A (,) B ) /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. ran ( RR _D F ) )
17 12 15 16 syl2an2r 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( RR _D F ) ` x ) e. ran ( RR _D F ) )
18 eleq1 
 |-  ( ( ( RR _D F ) ` x ) = C -> ( ( ( RR _D F ) ` x ) e. ran ( RR _D F ) <-> C e. ran ( RR _D F ) ) )
19 17 18 syl5ibcom 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( ( RR _D F ) ` x ) = C -> C e. ran ( RR _D F ) ) )
20 19 rexlimdva 
 |-  ( ph -> ( E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C -> C e. ran ( RR _D F ) ) )
21 8 20 mpd 
 |-  ( ph -> C e. ran ( RR _D F ) )