Metamath Proof Explorer

Theorem chordthmlem4

Description: If P is on the segment AB and M is the midpoint of AB, then PA x. PB = BM2 - PM2. If all lengths are reexpressed as fractions of AB, this reduces to the identity X x. ( 1 - X ) = ( 1 / 2 )2 - ( ( 1 / 2 ) - X )2. (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 ) ) )