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	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
	dvlem.2	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
	dvlem.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	dvlem	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		dvlem.1	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
2		dvlem.2	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
3		dvlem.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
4		eldifsn	⊢ ( 𝐴 ∈ ( 𝐷 ∖ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) )
5	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐹 : 𝐷 ⟶ ℂ )
6		simprl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ∈ 𝐷 )
7	5 6	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
8	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐵 ∈ 𝐷 )
9	5 8	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
10	7 9	subcld	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
11	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐷 ⊆ ℂ )
12	11 6	sseldd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ∈ ℂ )
13	11 8	sseldd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐵 ∈ ℂ )
14	12 13	subcld	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
15		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ≠ 𝐵 )
16	12 13 15	subne0d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 − 𝐵 ) ≠ 0 )
17	10 14 16	divcld	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )
18	4 17	sylan2b	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )