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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	chordthmlem4.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	chordthmlem4.X	⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
	chordthmlem4.M	⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
	chordthmlem4.P	⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
Assertion	chordthmlem4	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑀 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )

Proof

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