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	ffvelrnd	|- ( ( 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	ffvelrnd	|- ( ( 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 )