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

Metamath Proof Explorer

Theorem dvlem

Description: Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses dvlem.1 
|- ( ph -> F : D --> CC )
dvlem.2 
|- ( ph -> D C_ CC )
dvlem.3 
|- ( ph -> B e. D )
Assertion dvlem 
|- ( ( ph /\ A e. ( D \ { B } ) ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )

Proof

Step Hyp Ref Expression
1 dvlem.1 
 |-  ( ph -> F : D --> CC )
2 dvlem.2 
 |-  ( ph -> D C_ CC )
3 dvlem.3 
 |-  ( ph -> B e. D )
4 eldifsn 
 |-  ( A e. ( D \ { B } ) <-> ( A e. D /\ A =/= B ) )
5 1 adantr 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> F : D --> CC )
6 simprl 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> A e. D )
7 5 6 ffvelcdmd 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( F ` A ) e. CC )
8 3 adantr 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> B e. D )
9 5 8 ffvelcdmd 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( F ` B ) e. CC )
10 7 9 subcld 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( ( F ` A ) - ( F ` B ) ) e. CC )
11 2 adantr 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> D C_ CC )
12 11 6 sseldd 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> A e. CC )
13 11 8 sseldd 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> B e. CC )
14 12 13 subcld 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( A - B ) e. CC )
15 simprr 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> A =/= B )
16 12 13 15 subne0d 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( A - B ) =/= 0 )
17 10 14 16 divcld 
 |-  ( ( ph /\ ( A e. D /\ A =/= B ) ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )
18 4 17 sylan2b 
 |-  ( ( ph /\ A e. ( D \ { B } ) ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )