Metamath Proof Explorer

Theorem divsubdir

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

Ref Expression
Assertion divsubdir ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A−BC=AC−BC

Proof

Step Hyp Ref Expression
1 negcl ⊢B∈ℂ→−B∈ℂ
2 divdir ⊢A∈ℂ∧−B∈ℂ∧C∈ℂ∧C≠0→A+−BC=AC+−BC
3 1 2 syl3an2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A+−BC=AC+−BC
4 negsub ⊢A∈ℂ∧B∈ℂ→A+−B=A−B
5 4 oveq1d ⊢A∈ℂ∧B∈ℂ→A+−BC=A−BC
6 5 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A+−BC=A−BC
7 3 6 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC+−BC=A−BC
8 divneg ⊢B∈ℂ∧C∈ℂ∧C≠0→−BC=−BC
9 8 3expb ⊢B∈ℂ∧C∈ℂ∧C≠0→−BC=−BC
10 9 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→−BC=−BC
11 10 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC+−BC=AC+−BC
12 divcl ⊢A∈ℂ∧C∈ℂ∧C≠0→AC∈ℂ
13 12 3expb ⊢A∈ℂ∧C∈ℂ∧C≠0→AC∈ℂ
14 13 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC∈ℂ
15 divcl ⊢B∈ℂ∧C∈ℂ∧C≠0→BC∈ℂ
16 15 3expb ⊢B∈ℂ∧C∈ℂ∧C≠0→BC∈ℂ
17 16 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→BC∈ℂ
18 14 17 negsubd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC+−BC=AC−BC
19 11 18 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→AC+−BC=AC−BC
20 7 19 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0→A−BC=AC−BC