Proof of Theorem bj-bary1lem
Step | Hyp | Ref
| Expression |
1 | | bj-bary1.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
2 | | bj-bary1.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | 1, 2 | mulcld 10995 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · 𝐴) ∈ ℂ) |
4 | | bj-bary1.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
5 | 4, 2 | mulcld 10995 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 · 𝐴) ∈ ℂ) |
6 | 3, 5 | subcld 11332 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · 𝐴) − (𝑋 · 𝐴)) ∈ ℂ) |
7 | 4, 1 | mulcld 10995 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 · 𝐵) ∈ ℂ) |
8 | 2, 1 | mulcld 10995 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
9 | 6, 7, 8 | addsub12d 11355 |
. . . . . . 7
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)))) |
10 | 3, 5, 8 | sub32d 11364 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)) = (((𝐵 · 𝐴) − (𝐴 · 𝐵)) − (𝑋 · 𝐴))) |
11 | 1, 2 | bj-subcom 35479 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · 𝐴) − (𝐴 · 𝐵)) = 0) |
12 | 11 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝐴 · 𝐵)) − (𝑋 · 𝐴)) = (0 − (𝑋 · 𝐴))) |
13 | 10, 12 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)) = (0 − (𝑋 · 𝐴))) |
14 | 13 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · 𝐵) + (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) |
15 | 9, 14 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) |
16 | | 0cnd 10968 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℂ) |
17 | 7, 16, 5 | addsubassd 11352 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝐵) + 0) − (𝑋 · 𝐴)) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) |
18 | 7 | addid1d 11175 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · 𝐵) + 0) = (𝑋 · 𝐵)) |
19 | 18 | oveq1d 7290 |
. . . . . 6
⊢ (𝜑 → (((𝑋 · 𝐵) + 0) − (𝑋 · 𝐴)) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) |
20 | 15, 17, 19 | 3eqtr2d 2784 |
. . . . 5
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) |
21 | 1, 4, 2 | subdird 11432 |
. . . . . 6
⊢ (𝜑 → ((𝐵 − 𝑋) · 𝐴) = ((𝐵 · 𝐴) − (𝑋 · 𝐴))) |
22 | 4, 2, 1 | subdird 11432 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − 𝐴) · 𝐵) = ((𝑋 · 𝐵) − (𝐴 · 𝐵))) |
23 | 21, 22 | oveq12d 7293 |
. . . . 5
⊢ (𝜑 → (((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) = (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵)))) |
24 | 4, 1, 2 | subdid 11431 |
. . . . 5
⊢ (𝜑 → (𝑋 · (𝐵 − 𝐴)) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) |
25 | 20, 23, 24 | 3eqtr4rd 2789 |
. . . 4
⊢ (𝜑 → (𝑋 · (𝐵 − 𝐴)) = (((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵))) |
26 | 25 | oveq1d 7290 |
. . 3
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) / (𝐵 − 𝐴))) |
27 | 1, 4 | subcld 11332 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ) |
28 | 27, 2 | mulcld 10995 |
. . . 4
⊢ (𝜑 → ((𝐵 − 𝑋) · 𝐴) ∈ ℂ) |
29 | 4, 2 | subcld 11332 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ) |
30 | 29, 1 | mulcld 10995 |
. . . 4
⊢ (𝜑 → ((𝑋 − 𝐴) · 𝐵) ∈ ℂ) |
31 | 1, 2 | subcld 11332 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
32 | | bj-bary1.neq |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
33 | 32 | necomd 2999 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
34 | 1, 2, 33 | subne0d 11341 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
35 | 28, 30, 31, 34 | divdird 11789 |
. . 3
⊢ (𝜑 → ((((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)))) |
36 | 26, 35 | eqtrd 2778 |
. 2
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)))) |
37 | 4, 31, 34 | divcan4d 11757 |
. 2
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝑋) |
38 | 27, 2, 31, 34 | div23d 11788 |
. . 3
⊢ (𝜑 → (((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) = (((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴)) |
39 | 29, 1, 31, 34 | div23d 11788 |
. . 3
⊢ (𝜑 → (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)) = (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)) |
40 | 38, 39 | oveq12d 7293 |
. 2
⊢ (𝜑 → ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴))) = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) |
41 | 36, 37, 40 | 3eqtr3d 2786 |
1
⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) |