# Metamath Proof Explorer

## Theorem bj-bary1lem

Description: Lemma for bj-bary1 : expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses bj-bary1.a ${⊢}{\phi }\to {A}\in ℂ$
bj-bary1.b ${⊢}{\phi }\to {B}\in ℂ$
bj-bary1.x ${⊢}{\phi }\to {X}\in ℂ$
bj-bary1.neq ${⊢}{\phi }\to {A}\ne {B}$
Assertion bj-bary1lem ${⊢}{\phi }\to {X}=\left(\frac{{B}-{X}}{{B}-{A}}\right){A}+\left(\frac{{X}-{A}}{{B}-{A}}\right){B}$

### Proof

Step Hyp Ref Expression
1 bj-bary1.a ${⊢}{\phi }\to {A}\in ℂ$
2 bj-bary1.b ${⊢}{\phi }\to {B}\in ℂ$
3 bj-bary1.x ${⊢}{\phi }\to {X}\in ℂ$
4 bj-bary1.neq ${⊢}{\phi }\to {A}\ne {B}$
5 2 1 mulcld ${⊢}{\phi }\to {B}{A}\in ℂ$
6 3 1 mulcld ${⊢}{\phi }\to {X}{A}\in ℂ$
7 5 6 subcld ${⊢}{\phi }\to {B}{A}-{X}{A}\in ℂ$
8 3 2 mulcld ${⊢}{\phi }\to {X}{B}\in ℂ$
9 1 2 mulcld ${⊢}{\phi }\to {A}{B}\in ℂ$
10 7 8 9 addsub12d ${⊢}{\phi }\to \left({B}{A}-{X}{A}\right)+{X}{B}-{A}{B}={X}{B}+\left({B}{A}-{X}{A}\right)-{A}{B}$
11 5 6 9 sub32d ${⊢}{\phi }\to {B}{A}-{X}{A}-{A}{B}={B}{A}-{A}{B}-{X}{A}$
12 2 1 bj-subcom ${⊢}{\phi }\to {B}{A}-{A}{B}=0$
13 12 oveq1d ${⊢}{\phi }\to {B}{A}-{A}{B}-{X}{A}=0-{X}{A}$
14 11 13 eqtrd ${⊢}{\phi }\to {B}{A}-{X}{A}-{A}{B}=0-{X}{A}$
15 14 oveq2d ${⊢}{\phi }\to {X}{B}+\left({B}{A}-{X}{A}\right)-{A}{B}={X}{B}+0-{X}{A}$
16 10 15 eqtrd ${⊢}{\phi }\to \left({B}{A}-{X}{A}\right)+{X}{B}-{A}{B}={X}{B}+0-{X}{A}$
17 0cnd ${⊢}{\phi }\to 0\in ℂ$
18 8 17 6 addsubassd ${⊢}{\phi }\to {X}{B}+0-{X}{A}={X}{B}+0-{X}{A}$
19 8 addid1d ${⊢}{\phi }\to {X}{B}+0={X}{B}$
20 19 oveq1d ${⊢}{\phi }\to {X}{B}+0-{X}{A}={X}{B}-{X}{A}$
21 16 18 20 3eqtr2d ${⊢}{\phi }\to \left({B}{A}-{X}{A}\right)+{X}{B}-{A}{B}={X}{B}-{X}{A}$
22 2 3 1 subdird ${⊢}{\phi }\to \left({B}-{X}\right){A}={B}{A}-{X}{A}$
23 3 1 2 subdird ${⊢}{\phi }\to \left({X}-{A}\right){B}={X}{B}-{A}{B}$
24 22 23 oveq12d ${⊢}{\phi }\to \left({B}-{X}\right){A}+\left({X}-{A}\right){B}=\left({B}{A}-{X}{A}\right)+{X}{B}-{A}{B}$
25 3 2 1 subdid ${⊢}{\phi }\to {X}\left({B}-{A}\right)={X}{B}-{X}{A}$
26 21 24 25 3eqtr4rd ${⊢}{\phi }\to {X}\left({B}-{A}\right)=\left({B}-{X}\right){A}+\left({X}-{A}\right){B}$
27 26 oveq1d ${⊢}{\phi }\to \frac{{X}\left({B}-{A}\right)}{{B}-{A}}=\frac{\left({B}-{X}\right){A}+\left({X}-{A}\right){B}}{{B}-{A}}$
28 2 3 subcld ${⊢}{\phi }\to {B}-{X}\in ℂ$
29 28 1 mulcld ${⊢}{\phi }\to \left({B}-{X}\right){A}\in ℂ$
30 3 1 subcld ${⊢}{\phi }\to {X}-{A}\in ℂ$
31 30 2 mulcld ${⊢}{\phi }\to \left({X}-{A}\right){B}\in ℂ$
32 2 1 subcld ${⊢}{\phi }\to {B}-{A}\in ℂ$
33 4 necomd ${⊢}{\phi }\to {B}\ne {A}$
34 2 1 33 subne0d ${⊢}{\phi }\to {B}-{A}\ne 0$
35 29 31 32 34 divdird ${⊢}{\phi }\to \frac{\left({B}-{X}\right){A}+\left({X}-{A}\right){B}}{{B}-{A}}=\left(\frac{\left({B}-{X}\right){A}}{{B}-{A}}\right)+\left(\frac{\left({X}-{A}\right){B}}{{B}-{A}}\right)$
36 27 35 eqtrd ${⊢}{\phi }\to \frac{{X}\left({B}-{A}\right)}{{B}-{A}}=\left(\frac{\left({B}-{X}\right){A}}{{B}-{A}}\right)+\left(\frac{\left({X}-{A}\right){B}}{{B}-{A}}\right)$
37 3 32 34 divcan4d ${⊢}{\phi }\to \frac{{X}\left({B}-{A}\right)}{{B}-{A}}={X}$
38 28 1 32 34 div23d ${⊢}{\phi }\to \frac{\left({B}-{X}\right){A}}{{B}-{A}}=\left(\frac{{B}-{X}}{{B}-{A}}\right){A}$
39 30 2 32 34 div23d ${⊢}{\phi }\to \frac{\left({X}-{A}\right){B}}{{B}-{A}}=\left(\frac{{X}-{A}}{{B}-{A}}\right){B}$
40 38 39 oveq12d ${⊢}{\phi }\to \left(\frac{\left({B}-{X}\right){A}}{{B}-{A}}\right)+\left(\frac{\left({X}-{A}\right){B}}{{B}-{A}}\right)=\left(\frac{{B}-{X}}{{B}-{A}}\right){A}+\left(\frac{{X}-{A}}{{B}-{A}}\right){B}$
41 36 37 40 3eqtr3d ${⊢}{\phi }\to {X}=\left(\frac{{B}-{X}}{{B}-{A}}\right){A}+\left(\frac{{X}-{A}}{{B}-{A}}\right){B}$