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 | |- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) ) |
|
| cevath.a | |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) ) |
||
| cevath.b | |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) ) |
||
| cevath.c | |- ( ph -> O e. CC ) |
||
| cevath.d | |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) ) |
||
| cevath.e | |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) ) |
||
| cevath.f | |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) ) |
||
| Assertion | cevath | |- ( ph -> ( ( ( A - F ) x. ( C - E ) ) x. ( B - D ) ) = ( ( ( F - B ) x. ( E - A ) ) x. ( D - C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cevath.sigar | |- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) ) |
|
| 2 | cevath.a | |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) ) |
|
| 3 | cevath.b | |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) ) |
|
| 4 | cevath.c | |- ( ph -> O e. CC ) |
|
| 5 | cevath.d | |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) ) |
|
| 6 | cevath.e | |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) ) |
|
| 7 | cevath.f | |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) ) |
|
| 8 | 2 | simp2d | |- ( ph -> B e. CC ) |
| 9 | 8 4 | subcld | |- ( ph -> ( B - O ) e. CC ) |
| 10 | 2 | simp3d | |- ( ph -> C e. CC ) |
| 11 | 10 4 | subcld | |- ( ph -> ( C - O ) e. CC ) |
| 12 | 9 11 | jca | |- ( ph -> ( ( B - O ) e. CC /\ ( C - O ) e. CC ) ) |
| 13 | 1 12 | sigarimcd | |- ( ph -> ( ( B - O ) G ( C - O ) ) e. CC ) |
| 14 | 2 | simp1d | |- ( ph -> A e. CC ) |
| 15 | 3 | simp1d | |- ( ph -> F e. CC ) |
| 16 | 14 15 | subcld | |- ( ph -> ( A - F ) e. CC ) |
| 17 | 14 4 | subcld | |- ( ph -> ( A - O ) e. CC ) |
| 18 | 11 17 | jca | |- ( ph -> ( ( C - O ) e. CC /\ ( A - O ) e. CC ) ) |
| 19 | 1 18 | sigarimcd | |- ( ph -> ( ( C - O ) G ( A - O ) ) e. CC ) |
| 20 | 13 16 19 | 3jca | |- ( ph -> ( ( ( B - O ) G ( C - O ) ) e. CC /\ ( A - F ) e. CC /\ ( ( C - O ) G ( A - O ) ) e. CC ) ) |
| 21 | 15 8 | subcld | |- ( ph -> ( F - B ) e. CC ) |
| 22 | 17 9 | jca | |- ( ph -> ( ( A - O ) e. CC /\ ( B - O ) e. CC ) ) |
| 23 | 1 22 | sigarimcd | |- ( ph -> ( ( A - O ) G ( B - O ) ) e. CC ) |
| 24 | 3 | simp3d | |- ( ph -> E e. CC ) |
| 25 | 10 24 | subcld | |- ( ph -> ( C - E ) e. CC ) |
| 26 | 21 23 25 | 3jca | |- ( ph -> ( ( F - B ) e. CC /\ ( ( A - O ) G ( B - O ) ) e. CC /\ ( C - E ) e. CC ) ) |
| 27 | 24 14 | subcld | |- ( ph -> ( E - A ) e. CC ) |
| 28 | 3 | simp2d | |- ( ph -> D e. CC ) |
| 29 | 8 28 | subcld | |- ( ph -> ( B - D ) e. CC ) |
| 30 | 28 10 | subcld | |- ( ph -> ( D - C ) e. CC ) |
| 31 | 27 29 30 | 3jca | |- ( ph -> ( ( E - A ) e. CC /\ ( B - D ) e. CC /\ ( D - C ) e. CC ) ) |
| 32 | 7 | simp2d | |- ( ph -> ( ( B - O ) G ( C - O ) ) =/= 0 ) |
| 33 | 7 | simp1d | |- ( ph -> ( ( A - O ) G ( B - O ) ) =/= 0 ) |
| 34 | 7 | simp3d | |- ( ph -> ( ( C - O ) G ( A - O ) ) =/= 0 ) |
| 35 | 32 33 34 | 3jca | |- ( ph -> ( ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) ) |
| 36 | 10 14 8 | 3jca | |- ( ph -> ( C e. CC /\ A e. CC /\ B e. CC ) ) |
| 37 | 24 15 28 | 3jca | |- ( ph -> ( E e. CC /\ F e. CC /\ D e. CC ) ) |
| 38 | 5 | simp3d | |- ( ph -> ( ( C - O ) G ( F - O ) ) = 0 ) |
| 39 | 5 | simp1d | |- ( ph -> ( ( A - O ) G ( D - O ) ) = 0 ) |
| 40 | 5 | simp2d | |- ( ph -> ( ( B - O ) G ( E - O ) ) = 0 ) |
| 41 | 38 39 40 | 3jca | |- ( ph -> ( ( ( C - O ) G ( F - O ) ) = 0 /\ ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 ) ) |
| 42 | 6 | simp3d | |- ( ph -> ( ( C - E ) G ( A - E ) ) = 0 ) |
| 43 | 6 | simp1d | |- ( ph -> ( ( A - F ) G ( B - F ) ) = 0 ) |
| 44 | 6 | simp2d | |- ( ph -> ( ( B - D ) G ( C - D ) ) = 0 ) |
| 45 | 42 43 44 | 3jca | |- ( ph -> ( ( ( C - E ) G ( A - E ) ) = 0 /\ ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 ) ) |
| 46 | 34 33 32 | 3jca | |- ( ph -> ( ( ( C - O ) G ( A - O ) ) =/= 0 /\ ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 ) ) |
| 47 | 1 36 37 4 41 45 46 | cevathlem2 | |- ( ph -> ( ( ( B - O ) G ( C - O ) ) x. ( A - F ) ) = ( ( ( C - O ) G ( A - O ) ) x. ( F - B ) ) ) |
| 48 | 8 10 14 | 3jca | |- ( ph -> ( B e. CC /\ C e. CC /\ A e. CC ) ) |
| 49 | 28 24 15 | 3jca | |- ( ph -> ( D e. CC /\ E e. CC /\ F e. CC ) ) |
| 50 | 40 38 39 | 3jca | |- ( ph -> ( ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 /\ ( ( A - O ) G ( D - O ) ) = 0 ) ) |
| 51 | 44 42 43 | 3jca | |- ( ph -> ( ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 /\ ( ( A - F ) G ( B - F ) ) = 0 ) ) |
| 52 | 32 34 33 | 3jca | |- ( ph -> ( ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 /\ ( ( A - O ) G ( B - O ) ) =/= 0 ) ) |
| 53 | 1 48 49 4 50 51 52 | cevathlem2 | |- ( ph -> ( ( ( A - O ) G ( B - O ) ) x. ( C - E ) ) = ( ( ( B - O ) G ( C - O ) ) x. ( E - A ) ) ) |
| 54 | 1 2 3 4 5 6 7 | cevathlem2 | |- ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) ) |
| 55 | 47 53 54 | 3jca | |- ( ph -> ( ( ( ( B - O ) G ( C - O ) ) x. ( A - F ) ) = ( ( ( C - O ) G ( A - O ) ) x. ( F - B ) ) /\ ( ( ( A - O ) G ( B - O ) ) x. ( C - E ) ) = ( ( ( B - O ) G ( C - O ) ) x. ( E - A ) ) /\ ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) ) ) |
| 56 | 20 26 31 35 55 | cevathlem1 | |- ( ph -> ( ( ( A - F ) x. ( C - E ) ) x. ( B - D ) ) = ( ( ( F - B ) x. ( E - A ) ) x. ( D - C ) ) ) |