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	|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		fconst6g	|- ( A e. CC -> ( CC X. { A } ) : CC --> CC )
2		simpr2	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> z e. CC )
3		fvconst2g	|- ( ( A e. CC /\ z e. CC ) -> ( ( CC X. { A } ) ` z ) = A )
4	2 3	syldan	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( CC X. { A } ) ` z ) = A )
5		fvconst2g	|- ( ( A e. CC /\ x e. CC ) -> ( ( CC X. { A } ) ` x ) = A )
6	5	3ad2antr1	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( CC X. { A } ) ` x ) = A )
7	4 6	oveq12d	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( CC X. { A } ) ` z ) - ( ( CC X. { A } ) ` x ) ) = ( A - A ) )
8		subid	|- ( A e. CC -> ( A - A ) = 0 )
9	8	adantr	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( A - A ) = 0 )
10	7 9	eqtrd	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( CC X. { A } ) ` z ) - ( ( CC X. { A } ) ` x ) ) = 0 )
11	10	oveq1d	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( ( CC X. { A } ) ` z ) - ( ( CC X. { A } ) ` x ) ) / ( z - x ) ) = ( 0 / ( z - x ) ) )
12		simpr1	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> x e. CC )
13	2 12	subcld	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( z - x ) e. CC )
14		simpr3	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> z =/= x )
15	2 12 14	subne0d	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( z - x ) =/= 0 )
16	13 15	div0d	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( 0 / ( z - x ) ) = 0 )
17	11 16	eqtrd	|- ( ( A e. CC /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( ( CC X. { A } ) ` z ) - ( ( CC X. { A } ) ` x ) ) / ( z - x ) ) = 0 )
18		0cn	|- 0 e. CC
19	1 17 18	dvidlem	|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )