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 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐵 ∈ 𝐷 )
9 5 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
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 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )