Theorem lcmineqlem7

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

	Ref	Expression
Assertion	lcmineqlem7	⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 )

Proof

Step	Hyp	Ref	Expression
1		cnelprrecn	⊢ ℂ ∈ { ℝ , ℂ }
2	1	a1i	⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
3		1cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
4		0cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℂ )
5		1cnd	⊢ ( ⊤ → 1 ∈ ℂ )
6	2 5	dvmptc	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
7		simpr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
8	2	dvmptid	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
9	2 3 4 6 7 3 8	dvmptsub	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 0 − 1 ) ) )
10		df-neg	⊢ - 1 = ( 0 − 1 )
11	10	a1i	⊢ ( ⊤ → - 1 = ( 0 − 1 ) )
12	11	eqcomd	⊢ ( ⊤ → ( 0 − 1 ) = - 1 )
13	12	mpteq2dv	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 0 − 1 ) ) = ( 𝑥 ∈ ℂ ↦ - 1 ) )
14	9 13	eqtrd	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 ) )
15	14	mptru	⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - 1 )