lcmineqlem7

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

		Ref	Expression
	Assertion	lcmineqlem7	$⊢ \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ - 1)$

Step	Hyp	Ref	Expression
1		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
2	1	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
3		1cnd	$⊢ (⊤ \land x \in ℂ) \to 1 \in ℂ$
4		0cnd	$⊢ (⊤ \land x \in ℂ) \to 0 \in ℂ$
5		1cnd	$⊢ ⊤ \to 1 \in ℂ$
6	2 5	dvmptc	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
7		simpr	$⊢ (⊤ \land x \in ℂ) \to x \in ℂ$
8	2	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
9	2 3 4 6 7 3 8	dvmptsub	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ 0 - 1)$
10		df-neg	$⊢ - 1 = 0 - 1$
11	10	a1i	$⊢ ⊤ \to - 1 = 0 - 1$
12	11	eqcomd	$⊢ ⊤ \to 0 - 1 = - 1$
13	12	mpteq2dv	$⊢ ⊤ \to (x \in ℂ ⟼ 0 - 1) = (x \in ℂ ⟼ - 1)$
14	9 13	eqtrd	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ - 1)$
15	14	mptru	$⊢ \frac{d (x \in ℂ⟼ 1 - x)}{d_{ℂ} x} = (x \in ℂ ⟼ - 1)$

Metamath Proof Explorer