Theorem chordthmlem

Description: If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right angles. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	chordthmlem.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)$$
	chordthmlem.A	$$⊢\phi \to A\in ℂ$$
	chordthmlem.B	$$⊢\phi \to B\in ℂ$$
	chordthmlem.Q	$$⊢\phi \to Q\in ℂ$$
	chordthmlem.M	$$⊢\phi \to M=\frac{A+B}{2}$$
	chordthmlem.ABequidistQ	$$⊢\phi \to \left|A-Q\right|=\left|B-Q\right|$$
	chordthmlem.AneB	$$⊢\phi \to A\ne B$$
	chordthmlem.QneM	$$⊢\phi \to Q\ne M$$
Assertion	chordthmlem	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		chordthmlem.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		chordthmlem.A	$$⊢\phi \to A\in ℂ$$
3		chordthmlem.B	$$⊢\phi \to B\in ℂ$$
4		chordthmlem.Q	$$⊢\phi \to Q\in ℂ$$
5		chordthmlem.M	$$⊢\phi \to M=\frac{A+B}{2}$$
6		chordthmlem.ABequidistQ	$$⊢\phi \to \left|A-Q\right|=\left|B-Q\right|$$
7		chordthmlem.AneB	$$⊢\phi \to A\ne B$$
8		chordthmlem.QneM	$$⊢\phi \to Q\ne M$$
9		negpitopissre	$$⊢\left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$$
10	2 3	addcld	$$⊢\phi \to A+B\in ℂ$$
11	10	halfcld	$$⊢\phi \to \frac{A+B}{2}\in ℂ$$
12	5 11	eqeltrd	$$⊢\phi \to M\in ℂ$$
13	4 12	subcld	$$⊢\phi \to Q-M\in ℂ$$
14	4 12 8	subne0d	$$⊢\phi \to Q-M\ne 0$$
15	3 12	subcld	$$⊢\phi \to B-M\in ℂ$$
16	5	oveq1d	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 2=\left(\frac{A+B}{2}\right)\cdot 2$$
17	12	times2d	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 2=M+M$$
18		2cnd	$$⊢\phi \to 2\in ℂ$$
19		2ne0	$$⊢2\ne 0$$
20	19	a1i	$$⊢\phi \to 2\ne 0$$
21	10 18 20	divcan1d	$$⊢\phi \to \left(\frac{A+B}{2}\right)\cdot 2=A+B$$
22	16 17 21	3eqtr3d	$$⊢\phi \to M+M=A+B$$
23	2 3 3 7	addneintr2d	$$⊢\phi \to A+B\ne B+B$$
24	22 23	eqnetrd	$$⊢\phi \to M+M\ne B+B$$
25	24	neneqd	$$⊢\phi \to \neg M+M=B+B$$
26		oveq12	$$⊢\left(M=B\wedge M=B\right)\to M+M=B+B$$
27	26	anidms	$$⊢M=B\to M+M=B+B$$
28	25 27	nsyl	$$⊢\phi \to \neg M=B$$
29	28	neqned	$$⊢\phi \to M\ne B$$
30	29	necomd	$$⊢\phi \to B\ne M$$
31	3 12 30	subne0d	$$⊢\phi \to B-M\ne 0$$
32	1 13 14 15 31	angcld	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$$
33	9 32	sselid	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in ℝ$$
34	33	recnd	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in ℂ$$
35	34	coscld	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(B-M\right)\right)\in ℂ$$
36	3 12	negsubdi2d	$$⊢\phi \to -\left(B-M\right)=M-B$$
37	12 12 2 3	addsubeq4d	$$⊢\phi \to \left(M+M=A+B\leftrightarrow A-M=M-B\right)$$
38	22 37	mpbid	$$⊢\phi \to A-M=M-B$$
39	36 38	eqtr4d	$$⊢\phi \to -\left(B-M\right)=A-M$$
40	39	oveq2d	$$⊢\phi \to \left(Q-M\right)F\left(-\left(B-M\right)\right)=\left(Q-M\right)F\left(A-M\right)$$
41	40	fveq2d	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(-\left(B-M\right)\right)\right)=\cos \left(\left(Q-M\right)F\left(A-M\right)\right)$$
42	1 13 14 15 31	cosangneg2d	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(-\left(B-M\right)\right)\right)=-\cos \left(\left(Q-M\right)F\left(B-M\right)\right)$$
43	2 2 3 7	addneintrd	$$⊢\phi \to A+A\ne A+B$$
44	43 22	neeqtrrd	$$⊢\phi \to A+A\ne M+M$$
45	44	necomd	$$⊢\phi \to M+M\ne A+A$$
46	45	neneqd	$$⊢\phi \to \neg M+M=A+A$$
47		oveq12	$$⊢\left(M=A\wedge M=A\right)\to M+M=A+A$$
48	47	anidms	$$⊢M=A\to M+M=A+A$$
49	46 48	nsyl	$$⊢\phi \to \neg M=A$$
50	49	neqned	$$⊢\phi \to M\ne A$$
51		eqidd	$$⊢\phi \to \left|Q-M\right|=\left|Q-M\right|$$
52	2 12	subcld	$$⊢\phi \to A-M\in ℂ$$
53	52	absnegd	$$⊢\phi \to \left|-\left(A-M\right)\right|=\left|A-M\right|$$
54	2 12	negsubdi2d	$$⊢\phi \to -\left(A-M\right)=M-A$$
55	54	fveq2d	$$⊢\phi \to \left|-\left(A-M\right)\right|=\left|M-A\right|$$
56	38	fveq2d	$$⊢\phi \to \left|A-M\right|=\left|M-B\right|$$
57	53 55 56	3eqtr3d	$$⊢\phi \to \left|M-A\right|=\left|M-B\right|$$
58	1 4 12 2 4 12 3 8 50 8 29 51 57 6	ssscongptld	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(A-M\right)\right)=\cos \left(\left(Q-M\right)F\left(B-M\right)\right)$$
59	41 42 58	3eqtr3rd	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(B-M\right)\right)=-\cos \left(\left(Q-M\right)F\left(B-M\right)\right)$$
60	35 59	eqnegad	$$⊢\phi \to \cos \left(\left(Q-M\right)F\left(B-M\right)\right)=0$$
61		coseq0negpitopi	$$⊢\left(Q-M\right)F\left(B-M\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to \left(\cos \left(\left(Q-M\right)F\left(B-M\right)\right)=0\leftrightarrow \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}\right)$$
62	32 61	syl	$$⊢\phi \to \left(\cos \left(\left(Q-M\right)F\left(B-M\right)\right)=0\leftrightarrow \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}\right)$$
63	60 62	mpbid	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}$$