Description: Ceva's theorem. Let A B C be a triangle and let points F , D and E lie on sides A B , B C , C A correspondingly. Suppose that cevians A D , B E and C F intersect at one point O . Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values.
The proof goes by applying cevathlem2 three times and then using cevathlem1 to multiply obtained identities and prove the theorem.
In the theorem statement we are using function G as a collinearity indicator. For justification of that use, see sigarcol . This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cevath.sigar | ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) ) | |
| cevath.a | ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) | ||
| cevath.b | ⊢ ( 𝜑 → ( 𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) ) | ||
| cevath.c | ⊢ ( 𝜑 → 𝑂 ∈ ℂ ) | ||
| cevath.d | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ) ) | ||
| cevath.e | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ∧ ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ) ) | ||
| cevath.f | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) ) | ||
| Assertion | cevath | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) · ( 𝐶 − 𝐸 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐹 − 𝐵 ) · ( 𝐸 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cevath.sigar | ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) ) | |
| 2 | cevath.a | ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) | |
| 3 | cevath.b | ⊢ ( 𝜑 → ( 𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) ) | |
| 4 | cevath.c | ⊢ ( 𝜑 → 𝑂 ∈ ℂ ) | |
| 5 | cevath.d | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ) ) | |
| 6 | cevath.e | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ∧ ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ) ) | |
| 7 | cevath.f | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) ) | |
| 8 | 2 | simp2d | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
| 9 | 8 4 | subcld | ⊢ ( 𝜑 → ( 𝐵 − 𝑂 ) ∈ ℂ ) |
| 10 | 2 | simp3d | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
| 11 | 10 4 | subcld | ⊢ ( 𝜑 → ( 𝐶 − 𝑂 ) ∈ ℂ ) |
| 12 | 9 11 | jca | ⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) ∈ ℂ ∧ ( 𝐶 − 𝑂 ) ∈ ℂ ) ) |
| 13 | 1 12 | sigarimcd | ⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ∈ ℂ ) |
| 14 | 2 | simp1d | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
| 15 | 3 | simp1d | ⊢ ( 𝜑 → 𝐹 ∈ ℂ ) |
| 16 | 14 15 | subcld | ⊢ ( 𝜑 → ( 𝐴 − 𝐹 ) ∈ ℂ ) |
| 17 | 14 4 | subcld | ⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) ∈ ℂ ) |
| 18 | 11 17 | jca | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑂 ) ∈ ℂ ∧ ( 𝐴 − 𝑂 ) ∈ ℂ ) ) |
| 19 | 1 18 | sigarimcd | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ∈ ℂ ) |
| 20 | 13 16 19 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ∈ ℂ ∧ ( 𝐴 − 𝐹 ) ∈ ℂ ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ∈ ℂ ) ) |
| 21 | 15 8 | subcld | ⊢ ( 𝜑 → ( 𝐹 − 𝐵 ) ∈ ℂ ) |
| 22 | 17 9 | jca | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) ∈ ℂ ∧ ( 𝐵 − 𝑂 ) ∈ ℂ ) ) |
| 23 | 1 22 | sigarimcd | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ∈ ℂ ) |
| 24 | 3 | simp3d | ⊢ ( 𝜑 → 𝐸 ∈ ℂ ) |
| 25 | 10 24 | subcld | ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) ∈ ℂ ) |
| 26 | 21 23 25 | 3jca | ⊢ ( 𝜑 → ( ( 𝐹 − 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ∈ ℂ ∧ ( 𝐶 − 𝐸 ) ∈ ℂ ) ) |
| 27 | 24 14 | subcld | ⊢ ( 𝜑 → ( 𝐸 − 𝐴 ) ∈ ℂ ) |
| 28 | 3 | simp2d | ⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
| 29 | 8 28 | subcld | ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ∈ ℂ ) |
| 30 | 28 10 | subcld | ⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ∈ ℂ ) |
| 31 | 27 29 30 | 3jca | ⊢ ( 𝜑 → ( ( 𝐸 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐷 − 𝐶 ) ∈ ℂ ) ) |
| 32 | 7 | simp2d | ⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ) |
| 33 | 7 | simp1d | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ) |
| 34 | 7 | simp3d | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) |
| 35 | 32 33 34 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) ) |
| 36 | 10 14 8 | 3jca | ⊢ ( 𝜑 → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) |
| 37 | 24 15 28 | 3jca | ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) |
| 38 | 5 | simp3d | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ) |
| 39 | 5 | simp1d | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ) |
| 40 | 5 | simp2d | ⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ) |
| 41 | 38 39 40 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ) ) |
| 42 | 6 | simp3d | ⊢ ( 𝜑 → ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ) |
| 43 | 6 | simp1d | ⊢ ( 𝜑 → ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ) |
| 44 | 6 | simp2d | ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ) |
| 45 | 42 43 44 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ∧ ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ) ) |
| 46 | 34 33 32 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ) ) |
| 47 | 1 36 37 4 41 45 46 | cevathlem2 | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) · ( 𝐴 − 𝐹 ) ) = ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐹 − 𝐵 ) ) ) |
| 48 | 8 10 14 | 3jca | ⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ) |
| 49 | 28 24 15 | 3jca | ⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) |
| 50 | 40 38 39 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ) ) |
| 51 | 44 42 43 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ∧ ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ∧ ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ) ) |
| 52 | 32 34 33 | 3jca | ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ) ) |
| 53 | 1 48 49 4 50 51 52 | cevathlem2 | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐸 ) ) = ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) · ( 𝐸 − 𝐴 ) ) ) |
| 54 | 1 2 3 4 5 6 7 | cevathlem2 | ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) ) |
| 55 | 47 53 54 | 3jca | ⊢ ( 𝜑 → ( ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) · ( 𝐴 − 𝐹 ) ) = ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐹 − 𝐵 ) ) ∧ ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐸 ) ) = ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) · ( 𝐸 − 𝐴 ) ) ∧ ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
| 56 | 20 26 31 35 55 | cevathlem1 | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) · ( 𝐶 − 𝐸 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐹 − 𝐵 ) · ( 𝐸 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) |