# Metamath Proof Explorer

## Theorem divsubdir

Description: Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005)

Ref Expression
Assertion divsubdir ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}-{B}}{{C}}=\left(\frac{{A}}{{C}}\right)-\left(\frac{{B}}{{C}}\right)$

### Proof

Step Hyp Ref Expression
1 negcl ${⊢}{B}\in ℂ\to -{B}\in ℂ$
2 divdir ${⊢}\left({A}\in ℂ\wedge -{B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}+\left(-{B}\right)}{{C}}=\left(\frac{{A}}{{C}}\right)+\left(\frac{-{B}}{{C}}\right)$
3 1 2 syl3an2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}+\left(-{B}\right)}{{C}}=\left(\frac{{A}}{{C}}\right)+\left(\frac{-{B}}{{C}}\right)$
4 negsub ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+\left(-{B}\right)={A}-{B}$
5 4 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \frac{{A}+\left(-{B}\right)}{{C}}=\frac{{A}-{B}}{{C}}$
6 5 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}+\left(-{B}\right)}{{C}}=\frac{{A}-{B}}{{C}}$
7 3 6 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{A}}{{C}}\right)+\left(\frac{-{B}}{{C}}\right)=\frac{{A}-{B}}{{C}}$
8 divneg ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to -\frac{{B}}{{C}}=\frac{-{B}}{{C}}$
9 8 3expb ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to -\frac{{B}}{{C}}=\frac{-{B}}{{C}}$
10 9 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to -\frac{{B}}{{C}}=\frac{-{B}}{{C}}$
11 10 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{A}}{{C}}\right)+\left(-\frac{{B}}{{C}}\right)=\left(\frac{{A}}{{C}}\right)+\left(\frac{-{B}}{{C}}\right)$
12 divcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{A}}{{C}}\in ℂ$
13 12 3expb ${⊢}\left({A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}}{{C}}\in ℂ$
14 13 3adant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}}{{C}}\in ℂ$
15 divcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{B}}{{C}}\in ℂ$
16 15 3expb ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}}{{C}}\in ℂ$
17 16 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}}{{C}}\in ℂ$
18 14 17 negsubd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{A}}{{C}}\right)+\left(-\frac{{B}}{{C}}\right)=\left(\frac{{A}}{{C}}\right)-\left(\frac{{B}}{{C}}\right)$
19 11 18 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{A}}{{C}}\right)+\left(\frac{-{B}}{{C}}\right)=\left(\frac{{A}}{{C}}\right)-\left(\frac{{B}}{{C}}\right)$
20 7 19 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}-{B}}{{C}}=\left(\frac{{A}}{{C}}\right)-\left(\frac{{B}}{{C}}\right)$