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	$⊢ φ \to F : D ⟶ ℂ$
	dvlem.2	$⊢ φ \to D \subseteq ℂ$
	dvlem.3	$⊢ φ \to B \in D$
Assertion	dvlem	$⊢ (φ \land A \in (D ∖ \{B\})) \to \frac{F (A) - F (B)}{A - B} \in ℂ$

Step	Hyp	Ref	Expression
1		dvlem.1	$⊢ φ \to F : D ⟶ ℂ$
2		dvlem.2	$⊢ φ \to D \subseteq ℂ$
3		dvlem.3	$⊢ φ \to B \in D$
4		eldifsn	$⊢ A \in (D ∖ \{B\}) \leftrightarrow (A \in D \land A \neq B)$
5	1	adantr	$⊢ (φ \land (A \in D \land A \neq B)) \to F : D ⟶ ℂ$
6		simprl	$⊢ (φ \land (A \in D \land A \neq B)) \to A \in D$
7	5 6	ffvelcdmd	$⊢ (φ \land (A \in D \land A \neq B)) \to F (A) \in ℂ$
8	3	adantr	$⊢ (φ \land (A \in D \land A \neq B)) \to B \in D$
9	5 8	ffvelcdmd	$⊢ (φ \land (A \in D \land A \neq B)) \to F (B) \in ℂ$
10	7 9	subcld	$⊢ (φ \land (A \in D \land A \neq B)) \to F (A) - F (B) \in ℂ$
11	2	adantr	$⊢ (φ \land (A \in D \land A \neq B)) \to D \subseteq ℂ$
12	11 6	sseldd	$⊢ (φ \land (A \in D \land A \neq B)) \to A \in ℂ$
13	11 8	sseldd	$⊢ (φ \land (A \in D \land A \neq B)) \to B \in ℂ$
14	12 13	subcld	$⊢ (φ \land (A \in D \land A \neq B)) \to A - B \in ℂ$
15		simprr	$⊢ (φ \land (A \in D \land A \neq B)) \to A \neq B$
16	12 13 15	subne0d	$⊢ (φ \land (A \in D \land A \neq B)) \to A - B \neq 0$
17	10 14 16	divcld	$⊢ (φ \land (A \in D \land A \neq B)) \to \frac{F (A) - F (B)}{A - B} \in ℂ$
18	4 17	sylan2b	$⊢ (φ \land A \in (D ∖ \{B\})) \to \frac{F (A) - F (B)}{A - B} \in ℂ$

Metamath Proof Explorer