Metamath Proof Explorer

Theorem lcmineqlem8

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

Ref Expression
Hypotheses lcmineqlem8.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem8.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem8.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
Assertion lcmineqlem8 ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem8.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lcmineqlem8.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem8.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
4 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
5 4 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
6 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
8 6 7 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 1 − 𝑥 ) ∈ ℂ )
9 neg1cn ⊢ - 1 ∈ ℂ
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → - 1 ∈ ℂ )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
12 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
14 znnsub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
15 12 13 14 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
16 3 15 mpbid ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ )
17 16 nnnn0d ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
19 11 18 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) ∈ ℂ )
20 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℂ )
22 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑀 ∈ ℂ )
24 21 23 subcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℂ )
25 nnm1nn0 ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
26 16 25 syl ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
28 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 ) → ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
29 11 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
30 24 29 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 − 𝑀 ) · ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ℂ )
31 lcmineqlem7 ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 )
32 31 a1i ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 ) )
33 dvexp ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 − 𝑀 ) · ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
34 16 33 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑁 − 𝑀 ) · ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
35 oveq1 ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) )
36 oveq1 ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) = ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) )
37 36 oveq2d ⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( ( 𝑁 − 𝑀 ) · ( 𝑦 ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
38 5 5 8 10 19 30 32 34 35 37 dvmptco ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) · - 1 ) ) )
39 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℂ )
40 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑀 ∈ ℂ )
41 39 40 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℂ )
42 ax-1cn ⊢ 1 ∈ ℂ
43 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 − 𝑥 ) ∈ ℂ )
44 42 43 mpan ⊢ ( 𝑥 ∈ ℂ → ( 1 − 𝑥 ) ∈ ℂ )
45 expcl ⊢ ( ( ( 1 − 𝑥 ) ∈ ℂ ∧ ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 ) → ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
46 44 26 45 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
47 41 46 10 mul32d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) · - 1 ) = ( ( ( 𝑁 − 𝑀 ) · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
48 20 22 subcld ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℂ )
49 9 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
50 48 49 mulcomd ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · - 1 ) = ( - 1 · ( 𝑁 − 𝑀 ) ) )
51 50 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑀 ) · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( ( - 1 · ( 𝑁 − 𝑀 ) ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑁 − 𝑀 ) · - 1 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( ( - 1 · ( 𝑁 − 𝑀 ) ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
53 47 52 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) · - 1 ) = ( ( - 1 · ( 𝑁 − 𝑀 ) ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
54 48 mulm1d ⊢ ( 𝜑 → ( - 1 · ( 𝑁 − 𝑀 ) ) = - ( 𝑁 − 𝑀 ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( - 1 · ( 𝑁 − 𝑀 ) ) = - ( 𝑁 − 𝑀 ) )
56 55 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( - 1 · ( 𝑁 − 𝑀 ) ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
57 53 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) · - 1 ) = ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) )
58 57 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) · - 1 ) ) = ( 𝑥 ∈ ℂ ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
59 38 58 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )