Theorem chordthmlem2

Description: If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem , where P = B, and using angrtmuld to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		chordthmlem2.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		chordthmlem2.A	$$⊢\phi \to A\in ℂ$$
3		chordthmlem2.B	$$⊢\phi \to B\in ℂ$$
4		chordthmlem2.Q	$$⊢\phi \to Q\in ℂ$$
5		chordthmlem2.X	$$⊢\phi \to X\in ℝ$$
6		chordthmlem2.M	$$⊢\phi \to M=\frac{A+B}{2}$$
7		chordthmlem2.P	$$⊢\phi \to P=XA+\left(1-X\right)B$$
8		chordthmlem2.ABequidistQ	$$⊢\phi \to \left|A-Q\right|=\left|B-Q\right|$$
9		chordthmlem2.PneM	$$⊢\phi \to P\ne M$$
10		chordthmlem2.QneM	$$⊢\phi \to Q\ne M$$
11		2re	$$⊢2\in ℝ$$
12	11	a1i	$$⊢\phi \to 2\in ℝ$$
13		2ne0	$$⊢2\ne 0$$
14	13	a1i	$$⊢\phi \to 2\ne 0$$
15	12 14	rereccld	$$⊢\phi \to \frac{1}{2}\in ℝ$$
16	15 5	resubcld	$$⊢\phi \to \left(\frac{1}{2}\right)-X\in ℝ$$
17	16	recnd	$$⊢\phi \to \left(\frac{1}{2}\right)-X\in ℂ$$
18	3 2	subcld	$$⊢\phi \to B-A\in ℂ$$
19	15	recnd	$$⊢\phi \to \frac{1}{2}\in ℂ$$
20	5	recnd	$$⊢\phi \to X\in ℂ$$
21	19 20 18	subdird	$$⊢\phi \to \left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)=\left(\frac{1}{2}\right)\left(B-A\right)-X\left(B-A\right)$$
22		2cnd	$$⊢\phi \to 2\in ℂ$$
23	3 22 14	divcan4d	$$⊢\phi \to \frac{B\cdot 2}{2}=B$$
24	3	times2d	$$⊢\phi \to B\cdot 2=B+B$$
25	24	oveq1d	$$⊢\phi \to \frac{B\cdot 2}{2}=\frac{B+B}{2}$$
26	23 25	eqtr3d	$$⊢\phi \to B=\frac{B+B}{2}$$
27	26 6	oveq12d	$$⊢\phi \to B-M=\left(\frac{B+B}{2}\right)-\left(\frac{A+B}{2}\right)$$
28	3 3	addcld	$$⊢\phi \to B+B\in ℂ$$
29	2 3	addcld	$$⊢\phi \to A+B\in ℂ$$
30	28 29 22 14	divsubdird	$$⊢\phi \to \frac{B+B-\left(A+B\right)}{2}=\left(\frac{B+B}{2}\right)-\left(\frac{A+B}{2}\right)$$
31	3 2 3	pnpcan2d	$$⊢\phi \to B+B-\left(A+B\right)=B-A$$
32	31	oveq1d	$$⊢\phi \to \frac{B+B-\left(A+B\right)}{2}=\frac{B-A}{2}$$
33	27 30 32	3eqtr2d	$$⊢\phi \to B-M=\frac{B-A}{2}$$
34	18 22 14	divrec2d	$$⊢\phi \to \frac{B-A}{2}=\left(\frac{1}{2}\right)\left(B-A\right)$$
35	33 34	eqtrd	$$⊢\phi \to B-M=\left(\frac{1}{2}\right)\left(B-A\right)$$
36	20 2	mulcld	$$⊢\phi \to XA\in ℂ$$
37		1cnd	$$⊢\phi \to 1\in ℂ$$
38	37 20	subcld	$$⊢\phi \to 1-X\in ℂ$$
39	38 3	mulcld	$$⊢\phi \to \left(1-X\right)B\in ℂ$$
40	36 39	addcld	$$⊢\phi \to XA+\left(1-X\right)B\in ℂ$$
41	7 40	eqeltrd	$$⊢\phi \to P\in ℂ$$
42	2 41 3 20	affineequiv	$$⊢\phi \to \left(P=XA+\left(1-X\right)B\leftrightarrow B-P=X\left(B-A\right)\right)$$
43	7 42	mpbid	$$⊢\phi \to B-P=X\left(B-A\right)$$
44	35 43	oveq12d	$$⊢\phi \to B-M-\left(B-P\right)=\left(\frac{1}{2}\right)\left(B-A\right)-X\left(B-A\right)$$
45	29	halfcld	$$⊢\phi \to \frac{A+B}{2}\in ℂ$$
46	6 45	eqeltrd	$$⊢\phi \to M\in ℂ$$
47	3 46 41	nnncan1d	$$⊢\phi \to B-M-\left(B-P\right)=P-M$$
48	21 44 47	3eqtr2rd	$$⊢\phi \to P-M=\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)$$
49	41 46 9	subne0d	$$⊢\phi \to P-M\ne 0$$
50	48 49	eqnetrrd	$$⊢\phi \to \left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)\ne 0$$
51	17 18 50	mulne0bbd	$$⊢\phi \to B-A\ne 0$$
52	3 2 51	subne0ad	$$⊢\phi \to B\ne A$$
53	52	necomd	$$⊢\phi \to A\ne B$$
54	1 2 3 4 6 8 53 10	chordthmlem	$$⊢\phi \to \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}$$
55	4 46	subcld	$$⊢\phi \to Q-M\in ℂ$$
56	41 46	subcld	$$⊢\phi \to P-M\in ℂ$$
57	3 46	subcld	$$⊢\phi \to B-M\in ℂ$$
58	4 46 10	subne0d	$$⊢\phi \to Q-M\ne 0$$
59	22 14	recne0d	$$⊢\phi \to \frac{1}{2}\ne 0$$
60	19 18 59 51	mulne0d	$$⊢\phi \to \left(\frac{1}{2}\right)\left(B-A\right)\ne 0$$
61	35 60	eqnetrd	$$⊢\phi \to B-M\ne 0$$
62	35 48	oveq12d	$$⊢\phi \to \frac{B-M}{P-M}=\frac{\left(\frac{1}{2}\right)\left(B-A\right)}{\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)}$$
63	17 18 50	mulne0bad	$$⊢\phi \to \left(\frac{1}{2}\right)-X\ne 0$$
64	19 17 18 63 51	divcan5rd	$$⊢\phi \to \frac{\left(\frac{1}{2}\right)\left(B-A\right)}{\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)}=\frac{\frac{1}{2}}{\left(\frac{1}{2}\right)-X}$$
65	62 64	eqtrd	$$⊢\phi \to \frac{B-M}{P-M}=\frac{\frac{1}{2}}{\left(\frac{1}{2}\right)-X}$$
66	15 16 63	redivcld	$$⊢\phi \to \frac{\frac{1}{2}}{\left(\frac{1}{2}\right)-X}\in ℝ$$
67	65 66	eqeltrd	$$⊢\phi \to \frac{B-M}{P-M}\in ℝ$$
68	1 55 56 57 58 49 61 67	angrtmuld	$$⊢\phi \to \left(\left(Q-M\right)F\left(P-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}\leftrightarrow \left(Q-M\right)F\left(B-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}\right)$$
69	54 68	mpbird	$$⊢\phi \to \left(Q-M\right)F\left(P-M\right)\in \left\{\frac{\mathrm{\pi }}{2},-\frac{\mathrm{\pi }}{2}\right\}$$