Proof of Theorem bj-bary1lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bj-bary1.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 2 |  | bj-bary1.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 3 | 1, 2 | mulcld 11282 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 · 𝐴) ∈ ℂ) | 
| 4 |  | bj-bary1.x | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 5 | 4, 2 | mulcld 11282 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 · 𝐴) ∈ ℂ) | 
| 6 | 3, 5 | subcld 11621 | . . . . . . . 8
⊢ (𝜑 → ((𝐵 · 𝐴) − (𝑋 · 𝐴)) ∈ ℂ) | 
| 7 | 4, 1 | mulcld 11282 | . . . . . . . 8
⊢ (𝜑 → (𝑋 · 𝐵) ∈ ℂ) | 
| 8 | 2, 1 | mulcld 11282 | . . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | 
| 9 | 6, 7, 8 | addsub12d 11644 | . . . . . . 7
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)))) | 
| 10 | 3, 5, 8 | sub32d 11653 | . . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)) = (((𝐵 · 𝐴) − (𝐴 · 𝐵)) − (𝑋 · 𝐴))) | 
| 11 | 1, 2 | bj-subcom 37310 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · 𝐴) − (𝐴 · 𝐵)) = 0) | 
| 12 | 11 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝐴 · 𝐵)) − (𝑋 · 𝐴)) = (0 − (𝑋 · 𝐴))) | 
| 13 | 10, 12 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵)) = (0 − (𝑋 · 𝐴))) | 
| 14 | 13 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((𝑋 · 𝐵) + (((𝐵 · 𝐴) − (𝑋 · 𝐴)) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) | 
| 15 | 9, 14 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) | 
| 16 |  | 0cnd 11255 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℂ) | 
| 17 | 7, 16, 5 | addsubassd 11641 | . . . . . 6
⊢ (𝜑 → (((𝑋 · 𝐵) + 0) − (𝑋 · 𝐴)) = ((𝑋 · 𝐵) + (0 − (𝑋 · 𝐴)))) | 
| 18 | 7 | addridd 11462 | . . . . . . 7
⊢ (𝜑 → ((𝑋 · 𝐵) + 0) = (𝑋 · 𝐵)) | 
| 19 | 18 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (((𝑋 · 𝐵) + 0) − (𝑋 · 𝐴)) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) | 
| 20 | 15, 17, 19 | 3eqtr2d 2782 | . . . . 5
⊢ (𝜑 → (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵))) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) | 
| 21 | 1, 4, 2 | subdird 11721 | . . . . . 6
⊢ (𝜑 → ((𝐵 − 𝑋) · 𝐴) = ((𝐵 · 𝐴) − (𝑋 · 𝐴))) | 
| 22 | 4, 2, 1 | subdird 11721 | . . . . . 6
⊢ (𝜑 → ((𝑋 − 𝐴) · 𝐵) = ((𝑋 · 𝐵) − (𝐴 · 𝐵))) | 
| 23 | 21, 22 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → (((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) = (((𝐵 · 𝐴) − (𝑋 · 𝐴)) + ((𝑋 · 𝐵) − (𝐴 · 𝐵)))) | 
| 24 | 4, 1, 2 | subdid 11720 | . . . . 5
⊢ (𝜑 → (𝑋 · (𝐵 − 𝐴)) = ((𝑋 · 𝐵) − (𝑋 · 𝐴))) | 
| 25 | 20, 23, 24 | 3eqtr4rd 2787 | . . . 4
⊢ (𝜑 → (𝑋 · (𝐵 − 𝐴)) = (((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵))) | 
| 26 | 25 | oveq1d 7447 | . . 3
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) / (𝐵 − 𝐴))) | 
| 27 | 1, 4 | subcld 11621 | . . . . 5
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ) | 
| 28 | 27, 2 | mulcld 11282 | . . . 4
⊢ (𝜑 → ((𝐵 − 𝑋) · 𝐴) ∈ ℂ) | 
| 29 | 4, 2 | subcld 11621 | . . . . 5
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ) | 
| 30 | 29, 1 | mulcld 11282 | . . . 4
⊢ (𝜑 → ((𝑋 − 𝐴) · 𝐵) ∈ ℂ) | 
| 31 | 1, 2 | subcld 11621 | . . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) | 
| 32 |  | bj-bary1.neq | . . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 33 | 32 | necomd 2995 | . . . . 5
⊢ (𝜑 → 𝐵 ≠ 𝐴) | 
| 34 | 1, 2, 33 | subne0d 11630 | . . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) | 
| 35 | 28, 30, 31, 34 | divdird 12082 | . . 3
⊢ (𝜑 → ((((𝐵 − 𝑋) · 𝐴) + ((𝑋 − 𝐴) · 𝐵)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)))) | 
| 36 | 26, 35 | eqtrd 2776 | . 2
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)))) | 
| 37 | 4, 31, 34 | divcan4d 12050 | . 2
⊢ (𝜑 → ((𝑋 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝑋) | 
| 38 | 27, 2, 31, 34 | div23d 12081 | . . 3
⊢ (𝜑 → (((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) = (((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴)) | 
| 39 | 29, 1, 31, 34 | div23d 12081 | . . 3
⊢ (𝜑 → (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴)) = (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)) | 
| 40 | 38, 39 | oveq12d 7450 | . 2
⊢ (𝜑 → ((((𝐵 − 𝑋) · 𝐴) / (𝐵 − 𝐴)) + (((𝑋 − 𝐴) · 𝐵) / (𝐵 − 𝐴))) = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | 
| 41 | 36, 37, 40 | 3eqtr3d 2784 | 1
⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) |