Theorem sigardiv

Description: If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017)

	Ref	Expression
Hypotheses	sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
	sigardiv.a	$$⊢\phi \to \left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)$$
	sigardiv.b	$$⊢\phi \to \neg C=A$$
	sigardiv.c	$$⊢\phi \to \left(B-A\right)G\left(C-A\right)=0$$
Assertion	sigardiv	$$⊢\phi \to \frac{B-A}{C-A}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
2		sigardiv.a	$$⊢\phi \to \left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)$$
3		sigardiv.b	$$⊢\phi \to \neg C=A$$
4		sigardiv.c	$$⊢\phi \to \left(B-A\right)G\left(C-A\right)=0$$
5	2	simp2d	$$⊢\phi \to B\in ℂ$$
6	2	simp1d	$$⊢\phi \to A\in ℂ$$
7	5 6	subcld	$$⊢\phi \to B-A\in ℂ$$
8	2	simp3d	$$⊢\phi \to C\in ℂ$$
9	8 6	subcld	$$⊢\phi \to C-A\in ℂ$$
10	3	neqned	$$⊢\phi \to C\ne A$$
11	8 6 10	subne0d	$$⊢\phi \to C-A\ne 0$$
12	7 9 11	cjdivd	$$⊢\phi \to \overline{\frac{B-A}{C-A}}=\frac{\overline{B-A}}{\overline{C-A}}$$
13	7	cjcld	$$⊢\phi \to \overline{B-A}\in ℂ$$
14	9	cjcld	$$⊢\phi \to \overline{C-A}\in ℂ$$
15	9 11	cjne0d	$$⊢\phi \to \overline{C-A}\ne 0$$
16	13 14 9 15 11	divcan5rd	$$⊢\phi \to \frac{\overline{B-A}\left(C-A\right)}{\overline{C-A}\left(C-A\right)}=\frac{\overline{B-A}}{\overline{C-A}}$$
17	13 9	mulcld	$$⊢\phi \to \overline{B-A}\left(C-A\right)\in ℂ$$
18	1	sigarval	$$⊢\left(B-A\in ℂ\wedge C-A\in ℂ\right)\to \left(B-A\right)G\left(C-A\right)=\Im \left(\overline{B-A}\left(C-A\right)\right)$$
19	7 9 18	syl2anc	$$⊢\phi \to \left(B-A\right)G\left(C-A\right)=\Im \left(\overline{B-A}\left(C-A\right)\right)$$
20	19 4	eqtr3d	$$⊢\phi \to \Im \left(\overline{B-A}\left(C-A\right)\right)=0$$
21	17 20	reim0bd	$$⊢\phi \to \overline{B-A}\left(C-A\right)\in ℝ$$
22	9 14	mulcomd	$$⊢\phi \to \left(C-A\right)\overline{C-A}=\overline{C-A}\left(C-A\right)$$
23	9	cjmulrcld	$$⊢\phi \to \left(C-A\right)\overline{C-A}\in ℝ$$
24	22 23	eqeltrrd	$$⊢\phi \to \overline{C-A}\left(C-A\right)\in ℝ$$
25	14 9 15 11	mulne0d	$$⊢\phi \to \overline{C-A}\left(C-A\right)\ne 0$$
26	21 24 25	redivcld	$$⊢\phi \to \frac{\overline{B-A}\left(C-A\right)}{\overline{C-A}\left(C-A\right)}\in ℝ$$
27	16 26	eqeltrrd	$$⊢\phi \to \frac{\overline{B-A}}{\overline{C-A}}\in ℝ$$
28	12 27	eqeltrd	$$⊢\phi \to \overline{\frac{B-A}{C-A}}\in ℝ$$
29	28	cjred	$$⊢\phi \to \overline{\stackrel{‾}{\frac{B-A}{C-A}}}=\overline{\frac{B-A}{C-A}}$$
30	7 9 11	divcld	$$⊢\phi \to \frac{B-A}{C-A}\in ℂ$$
31	30	cjcjd	$$⊢\phi \to \overline{\stackrel{‾}{\frac{B-A}{C-A}}}=\frac{B-A}{C-A}$$
32	29 31	eqtr3d	$$⊢\phi \to \overline{\frac{B-A}{C-A}}=\frac{B-A}{C-A}$$
33	32 28	eqeltrrd	$$⊢\phi \to \frac{B-A}{C-A}\in ℝ$$