Proof of Theorem affinecomb2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | affinecomb1.a | . . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 |  | affinecomb1.b | . . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 3 |  | affinecomb1.c | . . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 4 |  | affinecomb1.d | . . 3
⊢ (𝜑 → 𝐵 ≠ 𝐶) | 
| 5 |  | affinecomb1.e | . . 3
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 6 |  | affinecomb1.f | . . 3
⊢ (𝜑 → 𝐹 ∈ ℝ) | 
| 7 |  | affinecomb1.g | . . 3
⊢ (𝜑 → 𝐺 ∈ ℝ) | 
| 8 |  | eqid 2737 | . . 3
⊢ ((𝐺 − 𝐹) / (𝐶 − 𝐵)) = ((𝐺 − 𝐹) / (𝐶 − 𝐵)) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | affinecomb1 48623 | . 2
⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹))) | 
| 10 | 5 | recnd 11289 | . . 3
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 11 | 7 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ ℂ) | 
| 12 | 6 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈ ℂ) | 
| 13 | 11, 12 | subcld 11620 | . . . . . 6
⊢ (𝜑 → (𝐺 − 𝐹) ∈ ℂ) | 
| 14 | 3 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 15 | 2 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 16 | 14, 15 | subcld 11620 | . . . . . 6
⊢ (𝜑 → (𝐶 − 𝐵) ∈ ℂ) | 
| 17 | 4 | necomd 2996 | . . . . . . 7
⊢ (𝜑 → 𝐶 ≠ 𝐵) | 
| 18 | 14, 15, 17 | subne0d 11629 | . . . . . 6
⊢ (𝜑 → (𝐶 − 𝐵) ≠ 0) | 
| 19 | 13, 16, 18 | divcld 12043 | . . . . 5
⊢ (𝜑 → ((𝐺 − 𝐹) / (𝐶 − 𝐵)) ∈ ℂ) | 
| 20 | 1 | recnd 11289 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 21 | 20, 15 | subcld 11620 | . . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) | 
| 22 | 19, 21 | mulcld 11281 | . . . 4
⊢ (𝜑 → (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) ∈ ℂ) | 
| 23 | 22, 12 | addcld 11280 | . . 3
⊢ (𝜑 → ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹) ∈ ℂ) | 
| 24 | 10, 23, 16, 18 | mulcand 11896 | . 2
⊢ (𝜑 → (((𝐶 − 𝐵) · 𝐸) = ((𝐶 − 𝐵) · ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹)) ↔ 𝐸 = ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹))) | 
| 25 | 16, 22, 12 | adddid 11285 | . . . 4
⊢ (𝜑 → ((𝐶 − 𝐵) · ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹)) = (((𝐶 − 𝐵) · (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵))) + ((𝐶 − 𝐵) · 𝐹))) | 
| 26 | 13, 16, 18 | divcan2d 12045 | . . . . . . . 8
⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐺 − 𝐹) / (𝐶 − 𝐵))) = (𝐺 − 𝐹)) | 
| 27 | 26 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (((𝐶 − 𝐵) · ((𝐺 − 𝐹) / (𝐶 − 𝐵))) · (𝐴 − 𝐵)) = ((𝐺 − 𝐹) · (𝐴 − 𝐵))) | 
| 28 | 16, 19, 21 | mulassd 11284 | . . . . . . 7
⊢ (𝜑 → (((𝐶 − 𝐵) · ((𝐺 − 𝐹) / (𝐶 − 𝐵))) · (𝐴 − 𝐵)) = ((𝐶 − 𝐵) · (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)))) | 
| 29 | 13, 20, 15 | subdid 11719 | . . . . . . 7
⊢ (𝜑 → ((𝐺 − 𝐹) · (𝐴 − 𝐵)) = (((𝐺 − 𝐹) · 𝐴) − ((𝐺 − 𝐹) · 𝐵))) | 
| 30 | 27, 28, 29 | 3eqtr3d 2785 | . . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐵) · (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵))) = (((𝐺 − 𝐹) · 𝐴) − ((𝐺 − 𝐹) · 𝐵))) | 
| 31 | 14, 15, 12 | subdird 11720 | . . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐵) · 𝐹) = ((𝐶 · 𝐹) − (𝐵 · 𝐹))) | 
| 32 | 30, 31 | oveq12d 7449 | . . . . 5
⊢ (𝜑 → (((𝐶 − 𝐵) · (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵))) + ((𝐶 − 𝐵) · 𝐹)) = ((((𝐺 − 𝐹) · 𝐴) − ((𝐺 − 𝐹) · 𝐵)) + ((𝐶 · 𝐹) − (𝐵 · 𝐹)))) | 
| 33 | 13, 20 | mulcld 11281 | . . . . . 6
⊢ (𝜑 → ((𝐺 − 𝐹) · 𝐴) ∈ ℂ) | 
| 34 | 13, 15 | mulcld 11281 | . . . . . 6
⊢ (𝜑 → ((𝐺 − 𝐹) · 𝐵) ∈ ℂ) | 
| 35 | 14, 12 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝐶 · 𝐹) ∈ ℂ) | 
| 36 | 15, 12 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ) | 
| 37 | 35, 36 | subcld 11620 | . . . . . 6
⊢ (𝜑 → ((𝐶 · 𝐹) − (𝐵 · 𝐹)) ∈ ℂ) | 
| 38 | 33, 34, 37 | subadd23d 11642 | . . . . 5
⊢ (𝜑 → ((((𝐺 − 𝐹) · 𝐴) − ((𝐺 − 𝐹) · 𝐵)) + ((𝐶 · 𝐹) − (𝐵 · 𝐹))) = (((𝐺 − 𝐹) · 𝐴) + (((𝐶 · 𝐹) − (𝐵 · 𝐹)) − ((𝐺 − 𝐹) · 𝐵)))) | 
| 39 | 32, 38 | eqtrd 2777 | . . . 4
⊢ (𝜑 → (((𝐶 − 𝐵) · (((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵))) + ((𝐶 − 𝐵) · 𝐹)) = (((𝐺 − 𝐹) · 𝐴) + (((𝐶 · 𝐹) − (𝐵 · 𝐹)) − ((𝐺 − 𝐹) · 𝐵)))) | 
| 40 | 14, 12 | mulcomd 11282 | . . . . . . . 8
⊢ (𝜑 → (𝐶 · 𝐹) = (𝐹 · 𝐶)) | 
| 41 | 15, 12 | mulcomd 11282 | . . . . . . . 8
⊢ (𝜑 → (𝐵 · 𝐹) = (𝐹 · 𝐵)) | 
| 42 | 40, 41 | oveq12d 7449 | . . . . . . 7
⊢ (𝜑 → ((𝐶 · 𝐹) − (𝐵 · 𝐹)) = ((𝐹 · 𝐶) − (𝐹 · 𝐵))) | 
| 43 | 11, 12, 15 | subdird 11720 | . . . . . . 7
⊢ (𝜑 → ((𝐺 − 𝐹) · 𝐵) = ((𝐺 · 𝐵) − (𝐹 · 𝐵))) | 
| 44 | 42, 43 | oveq12d 7449 | . . . . . 6
⊢ (𝜑 → (((𝐶 · 𝐹) − (𝐵 · 𝐹)) − ((𝐺 − 𝐹) · 𝐵)) = (((𝐹 · 𝐶) − (𝐹 · 𝐵)) − ((𝐺 · 𝐵) − (𝐹 · 𝐵)))) | 
| 45 | 12, 14 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝐹 · 𝐶) ∈ ℂ) | 
| 46 | 11, 15 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝐺 · 𝐵) ∈ ℂ) | 
| 47 | 12, 15 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (𝐹 · 𝐵) ∈ ℂ) | 
| 48 | 45, 46, 47 | nnncan2d 11655 | . . . . . 6
⊢ (𝜑 → (((𝐹 · 𝐶) − (𝐹 · 𝐵)) − ((𝐺 · 𝐵) − (𝐹 · 𝐵))) = ((𝐹 · 𝐶) − (𝐺 · 𝐵))) | 
| 49 | 11, 15 | mulcomd 11282 | . . . . . . 7
⊢ (𝜑 → (𝐺 · 𝐵) = (𝐵 · 𝐺)) | 
| 50 | 49 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → ((𝐹 · 𝐶) − (𝐺 · 𝐵)) = ((𝐹 · 𝐶) − (𝐵 · 𝐺))) | 
| 51 | 44, 48, 50 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → (((𝐶 · 𝐹) − (𝐵 · 𝐹)) − ((𝐺 − 𝐹) · 𝐵)) = ((𝐹 · 𝐶) − (𝐵 · 𝐺))) | 
| 52 | 51 | oveq2d 7447 | . . . 4
⊢ (𝜑 → (((𝐺 − 𝐹) · 𝐴) + (((𝐶 · 𝐹) − (𝐵 · 𝐹)) − ((𝐺 − 𝐹) · 𝐵))) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))) | 
| 53 | 25, 39, 52 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → ((𝐶 − 𝐵) · ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹)) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))) | 
| 54 | 53 | eqeq2d 2748 | . 2
⊢ (𝜑 → (((𝐶 − 𝐵) · 𝐸) = ((𝐶 − 𝐵) · ((((𝐺 − 𝐹) / (𝐶 − 𝐵)) · (𝐴 − 𝐵)) + 𝐹)) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | 
| 55 | 9, 24, 54 | 3bitr2d 307 | 1
⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) |