Theorem chordthmlem4

Description: If P is on the segment AB and M is the midpoint of AB, then PA x. PB = BM² - PM². If all lengths are reexpressed as fractions of AB, this reduces to the identity X x. ( 1 - X ) = ( 1 / 2 )² - ( ( 1 / 2 ) - X )². (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	chordthmlem4.A	$$⊢\phi \to A\in ℂ$$
	chordthmlem4.B	$$⊢\phi \to B\in ℂ$$
	chordthmlem4.X	$$⊢\phi \to X\in \left[0,1\right]$$
	chordthmlem4.M	$$⊢\phi \to M=\frac{A+B}{2}$$
	chordthmlem4.P	$$⊢\phi \to P=XA+\left(1-X\right)B$$
Assertion	chordthmlem4	$$⊢\phi \to \left|P-A\right|\left|P-B\right|={\left|B-M\right|}^2-{\left|P-M\right|}^2$$

Proof

Step	Hyp	Ref	Expression
1		chordthmlem4.A	$$⊢\phi \to A\in ℂ$$
2		chordthmlem4.B	$$⊢\phi \to B\in ℂ$$
3		chordthmlem4.X	$$⊢\phi \to X\in \left[0,1\right]$$
4		chordthmlem4.M	$$⊢\phi \to M=\frac{A+B}{2}$$
5		chordthmlem4.P	$$⊢\phi \to P=XA+\left(1-X\right)B$$
6		1red	$$⊢\phi \to 1\in ℝ$$
7		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
8	7 3	sseldi	$$⊢\phi \to X\in ℝ$$
9	6 8	resubcld	$$⊢\phi \to 1-X\in ℝ$$
10	9	recnd	$$⊢\phi \to 1-X\in ℂ$$
11	10	abscld	$$⊢\phi \to \left|1-X\right|\in ℝ$$
12	11	recnd	$$⊢\phi \to \left|1-X\right|\in ℂ$$
13	2 1	subcld	$$⊢\phi \to B-A\in ℂ$$
14	13	abscld	$$⊢\phi \to \left|B-A\right|\in ℝ$$
15	14	recnd	$$⊢\phi \to \left|B-A\right|\in ℂ$$
16	8	recnd	$$⊢\phi \to X\in ℂ$$
17	16	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
18	17	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
19	12 15 18 15	mul4d	$$⊢\phi \to \left|1-X\right|\left|B-A\right|\left|X\right|\left|B-A\right|=\left|1-X\right|\left|X\right|\left|B-A\right|\left|B-A\right|$$
20	16 1	mulcld	$$⊢\phi \to XA\in ℂ$$
21	10 2	mulcld	$$⊢\phi \to \left(1-X\right)B\in ℂ$$
22	20 21	addcld	$$⊢\phi \to XA+\left(1-X\right)B\in ℂ$$
23	5 22	eqeltrd	$$⊢\phi \to P\in ℂ$$
24	1 23 2 16	affineequiv2	$$⊢\phi \to \left(P=XA+\left(1-X\right)B\leftrightarrow P-A=\left(1-X\right)\left(B-A\right)\right)$$
25	5 24	mpbid	$$⊢\phi \to P-A=\left(1-X\right)\left(B-A\right)$$
26	25	fveq2d	$$⊢\phi \to \left|P-A\right|=\left|\left(1-X\right)\left(B-A\right)\right|$$
27	10 13	absmuld	$$⊢\phi \to \left|\left(1-X\right)\left(B-A\right)\right|=\left|1-X\right|\left|B-A\right|$$
28	26 27	eqtrd	$$⊢\phi \to \left|P-A\right|=\left|1-X\right|\left|B-A\right|$$
29	23 2	abssubd	$$⊢\phi \to \left|P-B\right|=\left|B-P\right|$$
30	1 23 2 16	affineequiv	$$⊢\phi \to \left(P=XA+\left(1-X\right)B\leftrightarrow B-P=X\left(B-A\right)\right)$$
31	5 30	mpbid	$$⊢\phi \to B-P=X\left(B-A\right)$$
32	31	fveq2d	$$⊢\phi \to \left|B-P\right|=\left|X\left(B-A\right)\right|$$
33	16 13	absmuld	$$⊢\phi \to \left|X\left(B-A\right)\right|=\left|X\right|\left|B-A\right|$$
34	29 32 33	3eqtrd	$$⊢\phi \to \left|P-B\right|=\left|X\right|\left|B-A\right|$$
35	28 34	oveq12d	$$⊢\phi \to \left|P-A\right|\left|P-B\right|=\left|1-X\right|\left|B-A\right|\left|X\right|\left|B-A\right|$$
36	15	sqvald	$$⊢\phi \to {\left|B-A\right|}^2=\left|B-A\right|\left|B-A\right|$$
37	36	oveq2d	$$⊢\phi \to \left|1-X\right|\left|X\right|{\left|B-A\right|}^2=\left|1-X\right|\left|X\right|\left|B-A\right|\left|B-A\right|$$
38	19 35 37	3eqtr4d	$$⊢\phi \to \left|P-A\right|\left|P-B\right|=\left|1-X\right|\left|X\right|{\left|B-A\right|}^2$$
39	6	recnd	$$⊢\phi \to 1\in ℂ$$
40	39	halfcld	$$⊢\phi \to \frac{1}{2}\in ℂ$$
41	40	sqcld	$$⊢\phi \to {\left(\frac{1}{2}\right)}^2\in ℂ$$
42	6	rehalfcld	$$⊢\phi \to \frac{1}{2}\in ℝ$$
43	42 8	resubcld	$$⊢\phi \to \left(\frac{1}{2}\right)-X\in ℝ$$
44	43	recnd	$$⊢\phi \to \left(\frac{1}{2}\right)-X\in ℂ$$
45	44	abscld	$$⊢\phi \to \left|\left(\frac{1}{2}\right)-X\right|\in ℝ$$
46	45	recnd	$$⊢\phi \to \left|\left(\frac{1}{2}\right)-X\right|\in ℂ$$
47	46	sqcld	$$⊢\phi \to {\left|\left(\frac{1}{2}\right)-X\right|}^2\in ℂ$$
48	15	sqcld	$$⊢\phi \to {\left|B-A\right|}^2\in ℂ$$
49	41 47 48	subdird	$$⊢\phi \to \left({\left(\frac{1}{2}\right)}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2\right){\left|B-A\right|}^2={\left(\frac{1}{2}\right)}^2{\left|B-A\right|}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2{\left|B-A\right|}^2$$
50		subsq	$$⊢\left(\frac{1}{2}\in ℂ\wedge \left(\frac{1}{2}\right)-X\in ℂ\right)\to {\left(\frac{1}{2}\right)}^2-{\left(\left(\frac{1}{2}\right)-X\right)}^2=\left(\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X\right)\left(\left(\frac{1}{2}\right)-\left(\left(\frac{1}{2}\right)-X\right)\right)$$
51	40 44 50	syl2anc	$$⊢\phi \to {\left(\frac{1}{2}\right)}^2-{\left(\left(\frac{1}{2}\right)-X\right)}^2=\left(\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X\right)\left(\left(\frac{1}{2}\right)-\left(\left(\frac{1}{2}\right)-X\right)\right)$$
52	40 40 16	addsubassd	$$⊢\phi \to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X$$
53	39	2halvesd	$$⊢\phi \to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
54	53	oveq1d	$$⊢\phi \to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X=1-X$$
55	52 54	eqtr3d	$$⊢\phi \to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X=1-X$$
56	40 16	nncand	$$⊢\phi \to \left(\frac{1}{2}\right)-\left(\left(\frac{1}{2}\right)-X\right)=X$$
57	55 56	oveq12d	$$⊢\phi \to \left(\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)-X\right)\left(\left(\frac{1}{2}\right)-\left(\left(\frac{1}{2}\right)-X\right)\right)=\left(1-X\right)X$$
58	51 57	eqtr2d	$$⊢\phi \to \left(1-X\right)X={\left(\frac{1}{2}\right)}^2-{\left(\left(\frac{1}{2}\right)-X\right)}^2$$
59		elicc01	$$⊢X\in \left[0,1\right]\leftrightarrow \left(X\in ℝ\wedge 0\le X\wedge X\le 1\right)$$
60	3 59	sylib	$$⊢\phi \to \left(X\in ℝ\wedge 0\le X\wedge X\le 1\right)$$
61	60	simp3d	$$⊢\phi \to X\le 1$$
62	8 6 61	abssubge0d	$$⊢\phi \to \left|1-X\right|=1-X$$
63	60	simp2d	$$⊢\phi \to 0\le X$$
64	8 63	absidd	$$⊢\phi \to \left|X\right|=X$$
65	62 64	oveq12d	$$⊢\phi \to \left|1-X\right|\left|X\right|=\left(1-X\right)X$$
66		absresq	$$⊢\left(\frac{1}{2}\right)-X\in ℝ\to {\left|\left(\frac{1}{2}\right)-X\right|}^2={\left(\left(\frac{1}{2}\right)-X\right)}^2$$
67	43 66	syl	$$⊢\phi \to {\left|\left(\frac{1}{2}\right)-X\right|}^2={\left(\left(\frac{1}{2}\right)-X\right)}^2$$
68	67	oveq2d	$$⊢\phi \to {\left(\frac{1}{2}\right)}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2={\left(\frac{1}{2}\right)}^2-{\left(\left(\frac{1}{2}\right)-X\right)}^2$$
69	58 65 68	3eqtr4d	$$⊢\phi \to \left|1-X\right|\left|X\right|={\left(\frac{1}{2}\right)}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2$$
70	69	oveq1d	$$⊢\phi \to \left|1-X\right|\left|X\right|{\left|B-A\right|}^2=\left({\left(\frac{1}{2}\right)}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2\right){\left|B-A\right|}^2$$
71		2cnd	$$⊢\phi \to 2\in ℂ$$
72		2ne0	$$⊢2\ne 0$$
73	72	a1i	$$⊢\phi \to 2\ne 0$$
74	2 71 73	divcan4d	$$⊢\phi \to \frac{B\cdot 2}{2}=B$$
75	2	times2d	$$⊢\phi \to B\cdot 2=B+B$$
76	75	oveq1d	$$⊢\phi \to \frac{B\cdot 2}{2}=\frac{B+B}{2}$$
77	74 76	eqtr3d	$$⊢\phi \to B=\frac{B+B}{2}$$
78	77 4	oveq12d	$$⊢\phi \to B-M=\left(\frac{B+B}{2}\right)-\left(\frac{A+B}{2}\right)$$
79	2 2	addcld	$$⊢\phi \to B+B\in ℂ$$
80	1 2	addcld	$$⊢\phi \to A+B\in ℂ$$
81	79 80 71 73	divsubdird	$$⊢\phi \to \frac{B+B-\left(A+B\right)}{2}=\left(\frac{B+B}{2}\right)-\left(\frac{A+B}{2}\right)$$
82	2 1 2	pnpcan2d	$$⊢\phi \to B+B-\left(A+B\right)=B-A$$
83	82	oveq1d	$$⊢\phi \to \frac{B+B-\left(A+B\right)}{2}=\frac{B-A}{2}$$
84	78 81 83	3eqtr2d	$$⊢\phi \to B-M=\frac{B-A}{2}$$
85	13 71 73	divrec2d	$$⊢\phi \to \frac{B-A}{2}=\left(\frac{1}{2}\right)\left(B-A\right)$$
86	84 85	eqtrd	$$⊢\phi \to B-M=\left(\frac{1}{2}\right)\left(B-A\right)$$
87	86	fveq2d	$$⊢\phi \to \left|B-M\right|=\left|\left(\frac{1}{2}\right)\left(B-A\right)\right|$$
88	40 13	absmuld	$$⊢\phi \to \left|\left(\frac{1}{2}\right)\left(B-A\right)\right|=\left|\frac{1}{2}\right|\left|B-A\right|$$
89		0red	$$⊢\phi \to 0\in ℝ$$
90		halfgt0	$$⊢0<\frac{1}{2}$$
91	90	a1i	$$⊢\phi \to 0<\frac{1}{2}$$
92	89 42 91	ltled	$$⊢\phi \to 0\le \frac{1}{2}$$
93	42 92	absidd	$$⊢\phi \to \left|\frac{1}{2}\right|=\frac{1}{2}$$
94	93	oveq1d	$$⊢\phi \to \left|\frac{1}{2}\right|\left|B-A\right|=\left(\frac{1}{2}\right)\left|B-A\right|$$
95	87 88 94	3eqtrd	$$⊢\phi \to \left|B-M\right|=\left(\frac{1}{2}\right)\left|B-A\right|$$
96	95	oveq1d	$$⊢\phi \to {\left|B-M\right|}^2={\left(\frac{1}{2}\right)\left|B-A\right|}^2$$
97	40 15	sqmuld	$$⊢\phi \to {\left(\frac{1}{2}\right)\left|B-A\right|}^2={\left(\frac{1}{2}\right)}^2{\left|B-A\right|}^2$$
98	96 97	eqtrd	$$⊢\phi \to {\left|B-M\right|}^2={\left(\frac{1}{2}\right)}^2{\left|B-A\right|}^2$$
99	40 16 13	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)$$
100	86 31	oveq12d	$$⊢\phi \to B-M-\left(B-P\right)=\left(\frac{1}{2}\right)\left(B-A\right)-X\left(B-A\right)$$
101	80	halfcld	$$⊢\phi \to \frac{A+B}{2}\in ℂ$$
102	4 101	eqeltrd	$$⊢\phi \to M\in ℂ$$
103	2 102 23	nnncan1d	$$⊢\phi \to B-M-\left(B-P\right)=P-M$$
104	99 100 103	3eqtr2rd	$$⊢\phi \to P-M=\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)$$
105	104	fveq2d	$$⊢\phi \to \left|P-M\right|=\left|\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)\right|$$
106	44 13	absmuld	$$⊢\phi \to \left|\left(\left(\frac{1}{2}\right)-X\right)\left(B-A\right)\right|=\left|\left(\frac{1}{2}\right)-X\right|\left|B-A\right|$$
107	105 106	eqtrd	$$⊢\phi \to \left|P-M\right|=\left|\left(\frac{1}{2}\right)-X\right|\left|B-A\right|$$
108	107	oveq1d	$$⊢\phi \to {\left|P-M\right|}^2={\left|\left(\frac{1}{2}\right)-X\right|\left|B-A\right|}^2$$
109	46 15	sqmuld	$$⊢\phi \to {\left|\left(\frac{1}{2}\right)-X\right|\left|B-A\right|}^2={\left|\left(\frac{1}{2}\right)-X\right|}^2{\left|B-A\right|}^2$$
110	108 109	eqtrd	$$⊢\phi \to {\left|P-M\right|}^2={\left|\left(\frac{1}{2}\right)-X\right|}^2{\left|B-A\right|}^2$$
111	98 110	oveq12d	$$⊢\phi \to {\left|B-M\right|}^2-{\left|P-M\right|}^2={\left(\frac{1}{2}\right)}^2{\left|B-A\right|}^2-{\left|\left(\frac{1}{2}\right)-X\right|}^2{\left|B-A\right|}^2$$
112	49 70 111	3eqtr4rd	$$⊢\phi \to {\left|B-M\right|}^2-{\left|P-M\right|}^2=\left|1-X\right|\left|X\right|{\left|B-A\right|}^2$$
113	38 112	eqtr4d	$$⊢\phi \to \left|P-A\right|\left|P-B\right|={\left|B-M\right|}^2-{\left|P-M\right|}^2$$