# 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 ${⊢}{\phi }\to {F}:{D}⟶ℂ$
dvlem.2 ${⊢}{\phi }\to {D}\subseteq ℂ$
dvlem.3 ${⊢}{\phi }\to {B}\in {D}$
Assertion dvlem ${⊢}\left({\phi }\wedge {A}\in \left({D}\setminus \left\{{B}\right\}\right)\right)\to \frac{{F}\left({A}\right)-{F}\left({B}\right)}{{A}-{B}}\in ℂ$

### Proof

Step Hyp Ref Expression
1 dvlem.1 ${⊢}{\phi }\to {F}:{D}⟶ℂ$
2 dvlem.2 ${⊢}{\phi }\to {D}\subseteq ℂ$
3 dvlem.3 ${⊢}{\phi }\to {B}\in {D}$
4 eldifsn ${⊢}{A}\in \left({D}\setminus \left\{{B}\right\}\right)↔\left({A}\in {D}\wedge {A}\ne {B}\right)$
5 1 adantr ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {F}:{D}⟶ℂ$
6 simprl ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {A}\in {D}$
7 5 6 ffvelrnd ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {F}\left({A}\right)\in ℂ$
8 3 adantr ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {B}\in {D}$
9 5 8 ffvelrnd ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {F}\left({B}\right)\in ℂ$
10 7 9 subcld ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {F}\left({A}\right)-{F}\left({B}\right)\in ℂ$
11 2 adantr ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {D}\subseteq ℂ$
12 11 6 sseldd ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {A}\in ℂ$
13 11 8 sseldd ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {B}\in ℂ$
14 12 13 subcld ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {A}-{B}\in ℂ$
15 simprr ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {A}\ne {B}$
16 12 13 15 subne0d ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to {A}-{B}\ne 0$
17 10 14 16 divcld ${⊢}\left({\phi }\wedge \left({A}\in {D}\wedge {A}\ne {B}\right)\right)\to \frac{{F}\left({A}\right)-{F}\left({B}\right)}{{A}-{B}}\in ℂ$
18 4 17 sylan2b ${⊢}\left({\phi }\wedge {A}\in \left({D}\setminus \left\{{B}\right\}\right)\right)\to \frac{{F}\left({A}\right)-{F}\left({B}\right)}{{A}-{B}}\in ℂ$