Theorem angpined

Description: If the angle at ABC is _pi , then A is not equal to C . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	angpieqvd.angdef	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
	angpieqvd.A	$$⊢\phi \to A\in ℂ$$
	angpieqvd.B	$$⊢\phi \to B\in ℂ$$
	angpieqvd.C	$$⊢\phi \to C\in ℂ$$
	angpieqvd.AneB	$$⊢\phi \to A\ne B$$
	angpieqvd.BneC	$$⊢\phi \to B\ne C$$
Assertion	angpined	$$⊢\phi \to \left(\left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\to A\ne C\right)$$

Proof

Step	Hyp	Ref	Expression
1		angpieqvd.angdef	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
2		angpieqvd.A	$$⊢\phi \to A\in ℂ$$
3		angpieqvd.B	$$⊢\phi \to B\in ℂ$$
4		angpieqvd.C	$$⊢\phi \to C\in ℂ$$
5		angpieqvd.AneB	$$⊢\phi \to A\ne B$$
6		angpieqvd.BneC	$$⊢\phi \to B\ne C$$
7	1 2 3 4 5 6	angpieqvdlem2	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\right)$$
8		1rp	$$⊢1\in {ℝ}^{+}$$
9		1re	$$⊢1\in ℝ$$
10		ax-1ne0	$$⊢1\ne 0$$
11		rpneg	$$⊢\left(1\in ℝ\wedge 1\ne 0\right)\to \left(1\in {ℝ}^{+}\leftrightarrow \neg -1\in {ℝ}^{+}\right)$$
12	9 10 11	mp2an	$$⊢1\in {ℝ}^{+}\leftrightarrow \neg -1\in {ℝ}^{+}$$
13	8 12	mpbi	$$⊢\neg -1\in {ℝ}^{+}$$
14	2 3	subcld	$$⊢\phi \to A-B\in ℂ$$
15	14	adantr	$$⊢\left(\phi \wedge C=A\right)\to A-B\in ℂ$$
16	2 3 5	subne0d	$$⊢\phi \to A-B\ne 0$$
17	16	adantr	$$⊢\left(\phi \wedge C=A\right)\to A-B\ne 0$$
18		simpr	$$⊢\left(\phi \wedge C=A\right)\to C=A$$
19	18	oveq1d	$$⊢\left(\phi \wedge C=A\right)\to C-B=A-B$$
20	15 17 19	diveq1bd	$$⊢\left(\phi \wedge C=A\right)\to \frac{C-B}{A-B}=1$$
21	20	adantlr	$$⊢\left(\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\wedge C=A\right)\to \frac{C-B}{A-B}=1$$
22	21	negeqd	$$⊢\left(\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\wedge C=A\right)\to -\frac{C-B}{A-B}=-1$$
23		simplr	$$⊢\left(\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\wedge C=A\right)\to -\frac{C-B}{A-B}\in {ℝ}^{+}$$
24	22 23	eqeltrrd	$$⊢\left(\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\wedge C=A\right)\to -1\in {ℝ}^{+}$$
25	24	ex	$$⊢\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\to \left(C=A\to -1\in {ℝ}^{+}\right)$$
26	25	necon3bd	$$⊢\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\to \left(\neg -1\in {ℝ}^{+}\to C\ne A\right)$$
27	13 26	mpi	$$⊢\left(\phi \wedge -\frac{C-B}{A-B}\in {ℝ}^{+}\right)\to C\ne A$$
28	27	ex	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\to C\ne A\right)$$
29		necom	$$⊢C\ne A\leftrightarrow A\ne C$$
30	28 29	imbitrdi	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\to A\ne C\right)$$
31	7 30	sylbird	$$⊢\phi \to \left(\left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\to A\ne C\right)$$