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 } ) )