Metamath Proof Explorer

Theorem lcmineqlem8

Description: Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem8.1 
|- ( ph -> M e. NN )
lcmineqlem8.2 
|- ( ph -> N e. NN )
lcmineqlem8.3 
|- ( ph -> M < N )
Assertion lcmineqlem8 
|- ( ph -> ( CC _D ( x e. CC |-> ( ( 1 - x ) ^ ( N - M ) ) ) ) = ( x e. CC |-> ( -u ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem8.1 
 |-  ( ph -> M e. NN )
2 lcmineqlem8.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem8.3 
 |-  ( ph -> M < N )
4 cnelprrecn 
 |-  CC e. { RR , CC }
5 4 a1i 
 |-  ( ph -> CC e. { RR , CC } )
6 1cnd 
 |-  ( ( ph /\ x e. CC ) -> 1 e. CC )
7 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
8 6 7 subcld 
 |-  ( ( ph /\ x e. CC ) -> ( 1 - x ) e. CC )
9 neg1cn 
 |-  -u 1 e. CC
10 9 a1i 
 |-  ( ( ph /\ x e. CC ) -> -u 1 e. CC )
11 simpr 
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
12 1 nnzd 
 |-  ( ph -> M e. ZZ )
13 2 nnzd 
 |-  ( ph -> N e. ZZ )
14 znnsub 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )
15 12 13 14 syl2anc 
 |-  ( ph -> ( M < N <-> ( N - M ) e. NN ) )
16 3 15 mpbid 
 |-  ( ph -> ( N - M ) e. NN )
17 16 nnnn0d 
 |-  ( ph -> ( N - M ) e. NN0 )
18 17 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( N - M ) e. NN0 )
19 11 18 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ ( N - M ) ) e. CC )
20 2 nncnd 
 |-  ( ph -> N e. CC )
21 20 adantr 
 |-  ( ( ph /\ y e. CC ) -> N e. CC )
22 1 nncnd 
 |-  ( ph -> M e. CC )
23 22 adantr 
 |-  ( ( ph /\ y e. CC ) -> M e. CC )
24 21 23 subcld 
 |-  ( ( ph /\ y e. CC ) -> ( N - M ) e. CC )
25 nnm1nn0 
 |-  ( ( N - M ) e. NN -> ( ( N - M ) - 1 ) e. NN0 )
26 16 25 syl 
 |-  ( ph -> ( ( N - M ) - 1 ) e. NN0 )
27 26 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( ( N - M ) - 1 ) e. NN0 )
28 expcl 
 |-  ( ( y e. CC /\ ( ( N - M ) - 1 ) e. NN0 ) -> ( y ^ ( ( N - M ) - 1 ) ) e. CC )
29 11 27 28 syl2anc 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ ( ( N - M ) - 1 ) ) e. CC )
30 24 29 mulcld 
 |-  ( ( ph /\ y e. CC ) -> ( ( N - M ) x. ( y ^ ( ( N - M ) - 1 ) ) ) e. CC )
31 lcmineqlem7 
 |-  ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 )
32 31 a1i 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 ) )
33 dvexp 
 |-  ( ( N - M ) e. NN -> ( CC _D ( y e. CC |-> ( y ^ ( N - M ) ) ) ) = ( y e. CC |-> ( ( N - M ) x. ( y ^ ( ( N - M ) - 1 ) ) ) ) )
34 16 33 syl 
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y ^ ( N - M ) ) ) ) = ( y e. CC |-> ( ( N - M ) x. ( y ^ ( ( N - M ) - 1 ) ) ) ) )
35 oveq1 
 |-  ( y = ( 1 - x ) -> ( y ^ ( N - M ) ) = ( ( 1 - x ) ^ ( N - M ) ) )
36 oveq1 
 |-  ( y = ( 1 - x ) -> ( y ^ ( ( N - M ) - 1 ) ) = ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) )
37 36 oveq2d 
 |-  ( y = ( 1 - x ) -> ( ( N - M ) x. ( y ^ ( ( N - M ) - 1 ) ) ) = ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
38 5 5 8 10 19 30 32 34 35 37 dvmptco 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( 1 - x ) ^ ( N - M ) ) ) ) = ( x e. CC |-> ( ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) x. -u 1 ) ) )
39 20 adantr 
 |-  ( ( ph /\ x e. CC ) -> N e. CC )
40 22 adantr 
 |-  ( ( ph /\ x e. CC ) -> M e. CC )
41 39 40 subcld 
 |-  ( ( ph /\ x e. CC ) -> ( N - M ) e. CC )
42 ax-1cn 
 |-  1 e. CC
43 subcl 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 - x ) e. CC )
44 42 43 mpan 
 |-  ( x e. CC -> ( 1 - x ) e. CC )
45 expcl 
 |-  ( ( ( 1 - x ) e. CC /\ ( ( N - M ) - 1 ) e. NN0 ) -> ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) e. CC )
46 44 26 45 syl2anr 
 |-  ( ( ph /\ x e. CC ) -> ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) e. CC )
47 41 46 10 mul32d 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) x. -u 1 ) = ( ( ( N - M ) x. -u 1 ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
48 20 22 subcld 
 |-  ( ph -> ( N - M ) e. CC )
49 9 a1i 
 |-  ( ph -> -u 1 e. CC )
50 48 49 mulcomd 
 |-  ( ph -> ( ( N - M ) x. -u 1 ) = ( -u 1 x. ( N - M ) ) )
51 50 oveq1d 
 |-  ( ph -> ( ( ( N - M ) x. -u 1 ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) = ( ( -u 1 x. ( N - M ) ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
52 51 adantr 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( N - M ) x. -u 1 ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) = ( ( -u 1 x. ( N - M ) ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
53 47 52 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) x. -u 1 ) = ( ( -u 1 x. ( N - M ) ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
54 48 mulm1d 
 |-  ( ph -> ( -u 1 x. ( N - M ) ) = -u ( N - M ) )
55 54 adantr 
 |-  ( ( ph /\ x e. CC ) -> ( -u 1 x. ( N - M ) ) = -u ( N - M ) )
56 55 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 x. ( N - M ) ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) = ( -u ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
57 53 56 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) x. -u 1 ) = ( -u ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) )
58 57 mpteq2dva 
 |-  ( ph -> ( x e. CC |-> ( ( ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) x. -u 1 ) ) = ( x e. CC |-> ( -u ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) ) )
59 38 58 eqtrd 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( 1 - x ) ^ ( N - M ) ) ) ) = ( x e. CC |-> ( -u ( N - M ) x. ( ( 1 - x ) ^ ( ( N - M ) - 1 ) ) ) ) )