lcmineqlem8

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

	Ref	Expression
Hypotheses	lcmineqlem8.1	$⊢ φ \to M \in ℕ$
	lcmineqlem8.2	$⊢ φ \to N \in ℕ$
	lcmineqlem8.3	$⊢ φ \to M < N$
Assertion	lcmineqlem8	$⊢ φ \to \frac{d (x \in ℂ⟼ {(1 - x)}^{N - M})}{d_{ℂ} x} = (x \in ℂ ⟼ (- (N - M)) {(1 - x)}^{N - M - 1})$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem8.1	$⊢ φ \to M \in ℕ$
2		lcmineqlem8.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem8.3	$⊢ φ \to M < N$
4		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
5	4	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
6		1cnd	$⊢ (φ \land x \in ℂ) \to 1 \in ℂ$
7		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
8	6 7	subcld	$⊢ (φ \land x \in ℂ) \to 1 - x \in ℂ$
9		neg1cn	$⊢ - 1 \in ℂ$
10	9	a1i	$⊢ (φ \land x \in ℂ) \to - 1 \in ℂ$
11		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
12	1	nnzd	$⊢ φ \to M \in ℤ$
13	2	nnzd	$⊢ φ \to N \in ℤ$
14		znnsub	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow N - M \in ℕ)$
15	12 13 14	syl2anc	$⊢ φ \to (M < N \leftrightarrow N - M \in ℕ)$
16	3 15	mpbid	$⊢ φ \to N - M \in ℕ$
17	16	nnnn0d	$⊢ φ \to N - M \in ℕ_{0}$
18	17	adantr	$⊢ (φ \land y \in ℂ) \to N - M \in ℕ_{0}$
19	11 18	expcld	$⊢ (φ \land y \in ℂ) \to y^{N - M} \in ℂ$
20	2	nncnd	$⊢ φ \to N \in ℂ$
21	20	adantr	$⊢ (φ \land y \in ℂ) \to N \in ℂ$
22	1	nncnd	$⊢ φ \to M \in ℂ$
23	22	adantr	$⊢ (φ \land y \in ℂ) \to M \in ℂ$
24	21 23	subcld	$⊢ (φ \land y \in ℂ) \to N - M \in ℂ$
25		nnm1nn0	$⊢ N - M \in ℕ \to N - M - 1 \in ℕ_{0}$
26	16 25	syl	$⊢ φ \to N - M - 1 \in ℕ_{0}$
27	26	adantr	$⊢ (φ \land y \in ℂ) \to N - M - 1 \in ℕ_{0}$
28		expcl	$⊢ (y \in ℂ \land N - M - 1 \in ℕ_{0}) \to y^{N - M - 1} \in ℂ$
29	11 27 28	syl2anc	$⊢ (φ \land y \in ℂ) \to y^{N - M - 1} \in ℂ$
30	24 29	mulcld	$⊢ (φ \land y \in ℂ) \to (N - M) y^{N - M - 1} \in ℂ$
31		lcmineqlem7	$⊢ \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ - 1)$
32	31	a1i	$⊢ φ \to \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ - 1)$
33		dvexp	$⊢ N - M \in ℕ \to \frac{d (y \in ℂ⟼ y^{N - M})}{d_{ℂ} y} = (y \in ℂ ⟼ (N - M) y^{N - M - 1})$
34	16 33	syl	$⊢ φ \to \frac{d (y \in ℂ⟼ y^{N - M})}{d_{ℂ} y} = (y \in ℂ ⟼ (N - M) y^{N - M - 1})$
35		oveq1	$⊢ y = 1 - x \to y^{N - M} = {(1 - x)}^{N - M}$
36		oveq1	$⊢ y = 1 - x \to y^{N - M - 1} = {(1 - x)}^{N - M - 1}$
37	36	oveq2d	$⊢ y = 1 - x \to (N - M) y^{N - M - 1} = (N - M) {(1 - x)}^{N - M - 1}$
38	5 5 8 10 19 30 32 34 35 37	dvmptco	$⊢ φ \to \frac{d (x \in ℂ⟼ {(1 - x)}^{N - M})}{d_{ℂ} x} = (x \in ℂ ⟼ (N - M) {(1 - x)}^{N - M - 1} -1)$
39	20	adantr	$⊢ (φ \land x \in ℂ) \to N \in ℂ$
40	22	adantr	$⊢ (φ \land x \in ℂ) \to M \in ℂ$
41	39 40	subcld	$⊢ (φ \land x \in ℂ) \to N - M \in ℂ$
42		ax-1cn	$⊢ 1 \in ℂ$
43		subcl	$⊢ (1 \in ℂ \land x \in ℂ) \to 1 - x \in ℂ$
44	42 43	mpan	$⊢ x \in ℂ \to 1 - x \in ℂ$
45		expcl	$⊢ (1 - x \in ℂ \land N - M - 1 \in ℕ_{0}) \to {(1 - x)}^{N - M - 1} \in ℂ$
46	44 26 45	syl2anr	$⊢ (φ \land x \in ℂ) \to {(1 - x)}^{N - M - 1} \in ℂ$
47	41 46 10	mul32d	$⊢ (φ \land x \in ℂ) \to (N - M) {(1 - x)}^{N - M - 1} -1 = (N - M) -1 {(1 - x)}^{N - M - 1}$
48	20 22	subcld	$⊢ φ \to N - M \in ℂ$
49	9	a1i	$⊢ φ \to - 1 \in ℂ$
50	48 49	mulcomd	$⊢ φ \to (N - M) -1 = -1 (N - M)$
51	50	oveq1d	$⊢ φ \to (N - M) -1 {(1 - x)}^{N - M - 1} = -1 (N - M) {(1 - x)}^{N - M - 1}$
52	51	adantr	$⊢ (φ \land x \in ℂ) \to (N - M) -1 {(1 - x)}^{N - M - 1} = -1 (N - M) {(1 - x)}^{N - M - 1}$
53	47 52	eqtrd	$⊢ (φ \land x \in ℂ) \to (N - M) {(1 - x)}^{N - M - 1} -1 = -1 (N - M) {(1 - x)}^{N - M - 1}$
54	48	mulm1d	$⊢ φ \to -1 (N - M) = - (N - M)$
55	54	adantr	$⊢ (φ \land x \in ℂ) \to -1 (N - M) = - (N - M)$
56	55	oveq1d	$⊢ (φ \land x \in ℂ) \to -1 (N - M) {(1 - x)}^{N - M - 1} = (- (N - M)) {(1 - x)}^{N - M - 1}$
57	53 56	eqtrd	$⊢ (φ \land x \in ℂ) \to (N - M) {(1 - x)}^{N - M - 1} -1 = (- (N - M)) {(1 - x)}^{N - M - 1}$
58	57	mpteq2dva	$⊢ φ \to (x \in ℂ ⟼ (N - M) {(1 - x)}^{N - M - 1} -1) = (x \in ℂ ⟼ (- (N - M)) {(1 - x)}^{N - M - 1})$
59	38 58	eqtrd	$⊢ φ \to \frac{d (x \in ℂ⟼ {(1 - x)}^{N - M})}{d_{ℂ} x} = (x \in ℂ ⟼ (- (N - M)) {(1 - x)}^{N - M - 1})$

Metamath Proof Explorer

Theorem lcmineqlem8

Proof