Metamath Proof Explorer

Theorem lcmineqlem7

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

Ref Expression
Assertion lcmineqlem7 ⊢ dx ∈ ℂ 1 − x d ℂ x = x ∈ ℂ ⟼ − 1

Proof

Step Hyp Ref Expression
1 cnelprrecn ⊢ ℂ ∈ ℝ ℂ
2 1 a1i ⊢ ⊤ → ℂ ∈ ℝ ℂ
3 1cnd ⊢ ⊤ ∧ x ∈ ℂ → 1 ∈ ℂ
4 0cnd ⊢ ⊤ ∧ x ∈ ℂ → 0 ∈ ℂ
5 1cnd ⊢ ⊤ → 1 ∈ ℂ
6 2 5 dvmptc ⊢ ⊤ → dx ∈ ℂ 1 d ℂ x = x ∈ ℂ ⟼ 0
7 simpr ⊢ ⊤ ∧ x ∈ ℂ → x ∈ ℂ
8 2 dvmptid ⊢ ⊤ → dx ∈ ℂ x d ℂ x = x ∈ ℂ ⟼ 1
9 2 3 4 6 7 3 8 dvmptsub ⊢ ⊤ → dx ∈ ℂ 1 − x d ℂ x = x ∈ ℂ ⟼ 0 − 1
10 df-neg ⊢ − 1 = 0 − 1
11 10 a1i ⊢ ⊤ → − 1 = 0 − 1
12 11 eqcomd ⊢ ⊤ → 0 − 1 = − 1
13 12 mpteq2dv ⊢ ⊤ → x ∈ ℂ ⟼ 0 − 1 = x ∈ ℂ ⟼ − 1
14 9 13 eqtrd ⊢ ⊤ → dx ∈ ℂ 1 − x d ℂ x = x ∈ ℂ ⟼ − 1
15 14 mptru ⊢ dx ∈ ℂ 1 − x d ℂ x = x ∈ ℂ ⟼ − 1