Metamath Proof Explorer

Theorem dvconst

Description: Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

		Ref	Expression
	Assertion	dvconst	$⊢ A \in ℂ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$

Proof

Step	Hyp	Ref	Expression
1		fconst6g	$⊢ A \in ℂ \to (ℂ \times \{A\}) : ℂ ⟶ ℂ$
2		simpr2	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to z \in ℂ$
3		fvconst2g	$⊢ (A \in ℂ \land z \in ℂ) \to (ℂ \times \{A\}) (z) = A$
4	2 3	syldan	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to (ℂ \times \{A\}) (z) = A$
5		fvconst2g	$⊢ (A \in ℂ \land x \in ℂ) \to (ℂ \times \{A\}) (x) = A$
6	5	3ad2antr1	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to (ℂ \times \{A\}) (x) = A$
7	4 6	oveq12d	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to (ℂ \times \{A\}) (z) - (ℂ \times \{A\}) (x) = A - A$
8		subid	$⊢ A \in ℂ \to A - A = 0$
9	8	adantr	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to A - A = 0$
10	7 9	eqtrd	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to (ℂ \times \{A\}) (z) - (ℂ \times \{A\}) (x) = 0$
11	10	oveq1d	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to \frac{(ℂ \times \{A\}) (z) - (ℂ \times \{A\}) (x)}{z - x} = \frac{0}{z - x}$
12		simpr1	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to x \in ℂ$
13	2 12	subcld	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to z - x \in ℂ$
14		simpr3	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to z \neq x$
15	2 12 14	subne0d	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to z - x \neq 0$
16	13 15	div0d	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to \frac{0}{z - x} = 0$
17	11 16	eqtrd	$⊢ (A \in ℂ \land (x \in ℂ \land z \in ℂ \land z \neq x)) \to \frac{(ℂ \times \{A\}) (z) - (ℂ \times \{A\}) (x)}{z - x} = 0$
18		0cn	$⊢ 0 \in ℂ$
19	1 17 18	dvidlem	$⊢ A \in ℂ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$