Metamath Proof Explorer

Theorem dvid

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

Ref Expression
Assertion dvid 
|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` CC ) : CC -1-1-onto-> CC
2 f1of 
 |-  ( ( _I |` CC ) : CC -1-1-onto-> CC -> ( _I |` CC ) : CC --> CC )
3 1 2 mp1i 
 |-  ( T. -> ( _I |` CC ) : CC --> CC )
4 simp2 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> z e. CC )
5 simp1 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> x e. CC )
6 4 5 subcld 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> ( z - x ) e. CC )
7 simp3 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> z =/= x )
8 4 5 7 subne0d 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> ( z - x ) =/= 0 )
9 fvresi 
 |-  ( z e. CC -> ( ( _I |` CC ) ` z ) = z )
10 fvresi 
 |-  ( x e. CC -> ( ( _I |` CC ) ` x ) = x )
11 9 10 oveqan12rd 
 |-  ( ( x e. CC /\ z e. CC ) -> ( ( ( _I |` CC ) ` z ) - ( ( _I |` CC ) ` x ) ) = ( z - x ) )
12 11 3adant3 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> ( ( ( _I |` CC ) ` z ) - ( ( _I |` CC ) ` x ) ) = ( z - x ) )
13 6 8 12 diveq1bd 
 |-  ( ( x e. CC /\ z e. CC /\ z =/= x ) -> ( ( ( ( _I |` CC ) ` z ) - ( ( _I |` CC ) ` x ) ) / ( z - x ) ) = 1 )
14 13 adantl 
 |-  ( ( T. /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( ( _I |` CC ) ` z ) - ( ( _I |` CC ) ` x ) ) / ( z - x ) ) = 1 )
15 ax-1cn 
 |-  1 e. CC
16 3 14 15 dvidlem 
 |-  ( T. -> ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } ) )
17 16 mptru 
 |-  ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )