Theorem chordthmlem5

Description: If P is on the segment AB and AQ = BQ, then PA x. PB = BQ² - PQ². This follows from two uses of chordthmlem3 to show that PQ² = QM² + PM² and BQ² = QM² + BM², so BQ² - PQ² = (QM² + BM²) - (QM² + PM²) = BM² - PM², which equals PA x. PB by chordthmlem4 . (Contributed by David Moews, 28-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		chordthmlem5.A	$$⊢\phi \to A\in ℂ$$
2		chordthmlem5.B	$$⊢\phi \to B\in ℂ$$
3		chordthmlem5.Q	$$⊢\phi \to Q\in ℂ$$
4		chordthmlem5.X	$$⊢\phi \to X\in \left[0,1\right]$$
5		chordthmlem5.P	$$⊢\phi \to P=XA+\left(1-X\right)B$$
6		chordthmlem5.ABequidistQ	$$⊢\phi \to \left|A-Q\right|=\left|B-Q\right|$$
7	1 2	addcld	$$⊢\phi \to A+B\in ℂ$$
8	7	halfcld	$$⊢\phi \to \frac{A+B}{2}\in ℂ$$
9	3 8	subcld	$$⊢\phi \to Q-\left(\frac{A+B}{2}\right)\in ℂ$$
10	9	abscld	$$⊢\phi \to \left|Q-\left(\frac{A+B}{2}\right)\right|\in ℝ$$
11	10	recnd	$$⊢\phi \to \left|Q-\left(\frac{A+B}{2}\right)\right|\in ℂ$$
12	11	sqcld	$$⊢\phi \to {\left|Q-\left(\frac{A+B}{2}\right)\right|}^2\in ℂ$$
13	2 8	subcld	$$⊢\phi \to B-\left(\frac{A+B}{2}\right)\in ℂ$$
14	13	abscld	$$⊢\phi \to \left|B-\left(\frac{A+B}{2}\right)\right|\in ℝ$$
15	14	recnd	$$⊢\phi \to \left|B-\left(\frac{A+B}{2}\right)\right|\in ℂ$$
16	15	sqcld	$$⊢\phi \to {\left|B-\left(\frac{A+B}{2}\right)\right|}^2\in ℂ$$
17		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
18	17 4	sseldi	$$⊢\phi \to X\in ℝ$$
19	18	recnd	$$⊢\phi \to X\in ℂ$$
20	19 1	mulcld	$$⊢\phi \to XA\in ℂ$$
21		1cnd	$$⊢\phi \to 1\in ℂ$$
22	21 19	subcld	$$⊢\phi \to 1-X\in ℂ$$
23	22 2	mulcld	$$⊢\phi \to \left(1-X\right)B\in ℂ$$
24	20 23	addcld	$$⊢\phi \to XA+\left(1-X\right)B\in ℂ$$
25	5 24	eqeltrd	$$⊢\phi \to P\in ℂ$$
26	25 8	subcld	$$⊢\phi \to P-\left(\frac{A+B}{2}\right)\in ℂ$$
27	26	abscld	$$⊢\phi \to \left|P-\left(\frac{A+B}{2}\right)\right|\in ℝ$$
28	27	recnd	$$⊢\phi \to \left|P-\left(\frac{A+B}{2}\right)\right|\in ℂ$$
29	28	sqcld	$$⊢\phi \to {\left|P-\left(\frac{A+B}{2}\right)\right|}^2\in ℂ$$
30	12 16 29	pnpcand	$$⊢\phi \to {\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|B-\left(\frac{A+B}{2}\right)\right|}^2-\left({\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|P-\left(\frac{A+B}{2}\right)\right|}^2\right)={\left|B-\left(\frac{A+B}{2}\right)\right|}^2-{\left|P-\left(\frac{A+B}{2}\right)\right|}^2$$
31		0red	$$⊢\phi \to 0\in ℝ$$
32		eqidd	$$⊢\phi \to \frac{A+B}{2}=\frac{A+B}{2}$$
33	1	mul02d	$$⊢\phi \to 0\cdot A=0$$
34	21	subid1d	$$⊢\phi \to 1-0=1$$
35	34	oveq1d	$$⊢\phi \to \left(1-0\right)B=1B$$
36	2	mulid2d	$$⊢\phi \to 1B=B$$
37	35 36	eqtrd	$$⊢\phi \to \left(1-0\right)B=B$$
38	33 37	oveq12d	$$⊢\phi \to 0\cdot A+\left(1-0\right)B=0+B$$
39	2	addid2d	$$⊢\phi \to 0+B=B$$
40	38 39	eqtr2d	$$⊢\phi \to B=0\cdot A+\left(1-0\right)B$$
41	1 2 3 31 32 40 6	chordthmlem3	$$⊢\phi \to {\left|B-Q\right|}^2={\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|B-\left(\frac{A+B}{2}\right)\right|}^2$$
42	1 2 3 18 32 5 6	chordthmlem3	$$⊢\phi \to {\left|P-Q\right|}^2={\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|P-\left(\frac{A+B}{2}\right)\right|}^2$$
43	41 42	oveq12d	$$⊢\phi \to {\left|B-Q\right|}^2-{\left|P-Q\right|}^2={\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|B-\left(\frac{A+B}{2}\right)\right|}^2-\left({\left|Q-\left(\frac{A+B}{2}\right)\right|}^2+{\left|P-\left(\frac{A+B}{2}\right)\right|}^2\right)$$
44	1 2 4 32 5	chordthmlem4	$$⊢\phi \to \left|P-A\right|\left|P-B\right|={\left|B-\left(\frac{A+B}{2}\right)\right|}^2-{\left|P-\left(\frac{A+B}{2}\right)\right|}^2$$
45	30 43 44	3eqtr4rd	$$⊢\phi \to \left|P-A\right|\left|P-B\right|={\left|B-Q\right|}^2-{\left|P-Q\right|}^2$$