Theorem cevath

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	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) · ( 𝐶 − 𝐸 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐹 − 𝐵 ) · ( 𝐸 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) )

Proof

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	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) · ( 𝐶 − 𝐸 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐹 − 𝐵 ) · ( 𝐸 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) )