# 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 ℂ\mathrm{D}\left(ℂ×\left\{{A}\right\}\right)=ℂ×\left\{0\right\}$

### Proof

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