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