Metamath Proof Explorer

Theorem lcmineqlem7

Description: Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024)

Ref Expression
Assertion lcmineqlem7 
|- ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 )

Proof

Step Hyp Ref Expression
1 cnelprrecn 
 |-  CC e. { RR , CC }
2 1 a1i 
 |-  ( T. -> CC e. { RR , CC } )
3 1cnd 
 |-  ( ( T. /\ x e. CC ) -> 1 e. CC )
4 0cnd 
 |-  ( ( T. /\ x e. CC ) -> 0 e. CC )
5 1cnd 
 |-  ( T. -> 1 e. CC )
6 2 5 dvmptc 
 |-  ( T. -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
7 simpr 
 |-  ( ( T. /\ x e. CC ) -> x e. CC )
8 2 dvmptid 
 |-  ( T. -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
9 2 3 4 6 7 3 8 dvmptsub 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> ( 0 - 1 ) ) )
10 df-neg 
 |-  -u 1 = ( 0 - 1 )
11 10 a1i 
 |-  ( T. -> -u 1 = ( 0 - 1 ) )
12 11 eqcomd 
 |-  ( T. -> ( 0 - 1 ) = -u 1 )
13 12 mpteq2dv 
 |-  ( T. -> ( x e. CC |-> ( 0 - 1 ) ) = ( x e. CC |-> -u 1 ) )
14 9 13 eqtrd 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 ) )
15 14 mptru 
 |-  ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 )