This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvconst

Description: Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion dvconst ( 𝐴 ∈ ℂ → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )

Proof

Step Hyp Ref Expression
1 fconst6g ⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ )
2 simpr2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → 𝑧 ∈ ℂ )
3 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) = 𝐴 )
4 2 3 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) = 𝐴 )
5 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
6 5 3ad2antr1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
7 4 6 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) − ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) ) = ( 𝐴 − 𝐴 ) )
8 subid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
9 8 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( 𝐴 − 𝐴 ) = 0 )
10 7 9 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) − ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) ) = 0 )
11 10 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) − ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( 0 / ( 𝑧 − 𝑥 ) ) )
12 simpr1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → 𝑥 ∈ ℂ )
13 2 12 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( 𝑧 − 𝑥 ) ∈ ℂ )
14 simpr3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → 𝑧 ≠ 𝑥 )
15 2 12 14 subne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( 𝑧 − 𝑥 ) ≠ 0 )
16 13 15 div0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( 0 / ( 𝑧 − 𝑥 ) ) = 0 )
17 11 16 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( ( ℂ × { 𝐴 } ) ‘ 𝑧 ) − ( ( ℂ × { 𝐴 } ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 0 )
18 0cn ⊢ 0 ∈ ℂ
19 1 17 18 dvidlem ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )