Metamath Proof Explorer

Theorem constrrtcclem

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. Case of non-degenerate circles. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constrrtcc.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
constrrtcc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
constrrtcc.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
constrrtcc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
constrrtcc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )
constrrtcc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
constrrtcc.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
constrrtcc.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
constrrtcc.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
constrrtcc.2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
constrrtcc.3 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
constrrtcc.4 ⊢ 𝑃 = ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) )
constrrtcc.5 ⊢ 𝑄 = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) )
constrrtcc.m ⊢ 𝑀 = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
constrrtcc.n ⊢ 𝑁 = - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
constrrtcclem.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
constrrtcclem.2 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
Assertion constrrtcclem ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 constrrtcc.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 constrrtcc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
3 constrrtcc.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
4 constrrtcc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
5 constrrtcc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )
6 constrrtcc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
7 constrrtcc.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
8 constrrtcc.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
9 constrrtcc.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
10 constrrtcc.2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
11 constrrtcc.3 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
12 constrrtcc.4 ⊢ 𝑃 = ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) )
13 constrrtcc.5 ⊢ 𝑄 = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) )
14 constrrtcc.m ⊢ 𝑀 = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
15 constrrtcc.n ⊢ 𝑁 = - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
16 constrrtcclem.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
17 constrrtcclem.2 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
18 8 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
19 1 6 sseldd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
20 1 7 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
21 19 20 subcld ⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) ∈ ℂ )
22 21 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ∈ ℂ )
23 21 22 mulcld ⊢ ( 𝜑 → ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) ∈ ℂ )
24 13 23 eqeltrid ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
25 1 5 sseldd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
26 25 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐷 ) ∈ ℂ )
27 1 2 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 25 27 addcld ⊢ ( 𝜑 → ( 𝐷 + 𝐴 ) ∈ ℂ )
29 26 28 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
30 24 29 subcld ⊢ ( 𝜑 → ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) ∈ ℂ )
31 1 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
32 1 4 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
33 31 32 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
34 33 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
35 33 34 mulcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℂ )
36 12 35 eqeltrid ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
37 27 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℂ )
38 37 28 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
39 36 38 subcld ⊢ ( 𝜑 → ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ∈ ℂ )
40 30 39 subcld ⊢ ( 𝜑 → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) ∈ ℂ )
41 26 37 subcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
42 25 27 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
43 25 27 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ∈ ℂ )
44 9 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
45 25 27 44 subne0d ⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ≠ 0 )
46 43 45 cjne0d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ≠ 0 )
47 42 46 eqnetrrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ≠ 0 )
48 40 41 47 divcld ⊢ ( 𝜑 → ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
49 14 48 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
50 49 8 mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) ∈ ℂ )
51 25 27 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℂ )
52 37 51 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
53 36 25 mulcld ⊢ ( 𝜑 → ( 𝑃 · 𝐷 ) ∈ ℂ )
54 52 53 subcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ∈ ℂ )
55 26 51 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
56 24 27 mulcld ⊢ ( 𝜑 → ( 𝑄 · 𝐴 ) ∈ ℂ )
57 55 56 subcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ∈ ℂ )
58 54 57 subcld ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) ∈ ℂ )
59 58 41 47 divcld ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
60 59 negcld ⊢ ( 𝜑 → - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
61 15 60 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
62 18 50 61 addassd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) + 𝑁 ) = ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) )
63 15 eqcomi ⊢ - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = 𝑁
64 63 a1i ⊢ ( 𝜑 → - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = 𝑁 )
65 59 64 negcon1ad ⊢ ( 𝜑 → - 𝑁 = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
66 65 59 eqeltrd ⊢ ( 𝜑 → - 𝑁 ∈ ℂ )
67 41 18 mulcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
68 40 8 mulcld ⊢ ( 𝜑 → ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ∈ ℂ )
69 26 37 18 subdird ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝑋 ↑ 2 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) )
70 30 39 8 subdird ⊢ ( 𝜑 → ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) − ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) )
71 69 70 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) − ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ) )
72 26 18 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
73 30 8 mulcld ⊢ ( 𝜑 → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ∈ ℂ )
74 37 18 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
75 39 8 mulcld ⊢ ( 𝜑 → ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ∈ ℂ )
76 72 73 74 75 addsub4d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) − ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ) )
77 8 27 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
78 8 25 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐷 ) ∈ ℂ )
79 77 78 mulcomd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) = ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) )
80 79 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) )
81 77 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐴 ) ) ∈ ℂ )
82 31 32 16 subne0d ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ≠ 0 )
83 33 82 absne0d ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐶 ) ) ≠ 0 )
84 10 83 eqnetrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) ≠ 0 )
85 77 abs00ad ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) = 0 ↔ ( 𝑋 − 𝐴 ) = 0 ) )
86 85 necon3bid ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) ≠ 0 ↔ ( 𝑋 − 𝐴 ) ≠ 0 ) )
87 84 86 mpbid ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ≠ 0 )
88 10 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) )
89 77 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐴 ) ) ↑ 2 ) = ( ( 𝑋 − 𝐴 ) · ( ∗ ‘ ( 𝑋 − 𝐴 ) ) ) )
90 33 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) = ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) )
91 88 89 90 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · ( ∗ ‘ ( 𝑋 − 𝐴 ) ) ) = ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) )
92 91 12 eqtr4di ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · ( ∗ ‘ ( 𝑋 − 𝐴 ) ) ) = 𝑃 )
93 77 81 87 92 mvllmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐴 ) ) = ( 𝑃 / ( 𝑋 − 𝐴 ) ) )
94 93 81 eqeltrrd ⊢ ( 𝜑 → ( 𝑃 / ( 𝑋 − 𝐴 ) ) ∈ ℂ )
95 37 94 addcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) ∈ ℂ )
96 95 77 78 mulassd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) )
97 36 77 87 divcan1d ⊢ ( 𝜑 → ( ( 𝑃 / ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐴 ) ) = 𝑃 )
98 97 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) + ( ( 𝑃 / ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) + 𝑃 ) )
99 37 77 94 98 joinlmuladdmuld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) + 𝑃 ) )
100 99 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) + 𝑃 ) · ( 𝑋 − 𝐷 ) ) )
101 37 77 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) ∈ ℂ )
102 101 36 78 adddird ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) + 𝑃 ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) + ( 𝑃 · ( 𝑋 − 𝐷 ) ) ) )
103 37 77 78 mulassd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) )
104 8 27 8 25 mulsubd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) = ( ( ( 𝑋 · 𝑋 ) + ( 𝐷 · 𝐴 ) ) − ( ( 𝑋 · 𝐷 ) + ( 𝑋 · 𝐴 ) ) ) )
105 8 sqvald ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
106 105 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝐷 · 𝐴 ) ) = ( ( 𝑋 · 𝑋 ) + ( 𝐷 · 𝐴 ) ) )
107 8 25 27 adddid ⊢ ( 𝜑 → ( 𝑋 · ( 𝐷 + 𝐴 ) ) = ( ( 𝑋 · 𝐷 ) + ( 𝑋 · 𝐴 ) ) )
108 106 107 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐷 · 𝐴 ) ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( ( ( 𝑋 · 𝑋 ) + ( 𝐷 · 𝐴 ) ) − ( ( 𝑋 · 𝐷 ) + ( 𝑋 · 𝐴 ) ) ) )
109 8 28 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
110 18 51 109 addsubd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐷 · 𝐴 ) ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) )
111 104 108 110 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) )
112 111 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) ) )
113 18 109 subcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ∈ ℂ )
114 37 113 51 adddid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) )
115 103 112 114 3eqtrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) )
116 36 8 25 subdid ⊢ ( 𝜑 → ( 𝑃 · ( 𝑋 − 𝐷 ) ) = ( ( 𝑃 · 𝑋 ) − ( 𝑃 · 𝐷 ) ) )
117 115 116 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) + ( 𝑃 · ( 𝑋 − 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑃 · 𝑋 ) − ( 𝑃 · 𝐷 ) ) ) )
118 100 102 117 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( 𝑋 − 𝐴 ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑃 · 𝑋 ) − ( 𝑃 · 𝐷 ) ) ) )
119 8 27 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐴 ) ) = ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐴 ) ) )
120 119 93 eqtr3d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐴 ) ) = ( 𝑃 / ( 𝑋 − 𝐴 ) ) )
121 8 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ∈ ℂ )
122 121 37 94 subaddd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐴 ) ) = ( 𝑃 / ( 𝑋 − 𝐴 ) ) ↔ ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) = ( ∗ ‘ 𝑋 ) ) )
123 120 122 mpbid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) = ( ∗ ‘ 𝑋 ) )
124 123 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) + ( 𝑃 / ( 𝑋 − 𝐴 ) ) ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) )
125 96 118 124 3eqtr3rd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑃 · 𝑋 ) − ( 𝑃 · 𝐷 ) ) ) )
126 37 113 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) ∈ ℂ )
127 126 52 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) ∈ ℂ )
128 36 8 mulcld ⊢ ( 𝜑 → ( 𝑃 · 𝑋 ) ∈ ℂ )
129 127 128 53 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑃 · 𝑋 ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑃 · 𝑋 ) − ( 𝑃 · 𝐷 ) ) ) )
130 126 52 128 add32d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑃 · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) )
131 130 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑃 · 𝑋 ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑃 · 𝐷 ) ) )
132 125 129 131 3eqtr2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑃 · 𝐷 ) ) )
133 126 128 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) ∈ ℂ )
134 133 52 53 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) )
135 38 8 mulcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ∈ ℂ )
136 74 135 128 subadd23d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) + ( 𝑃 · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 · 𝑋 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) ) )
137 37 18 109 subdid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) )
138 37 8 28 mul12d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( 𝑋 · ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) )
139 8 38 mulcomd ⊢ ( 𝜑 → ( 𝑋 · ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) )
140 138 139 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) )
141 140 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
142 137 141 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
143 142 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) + ( 𝑃 · 𝑋 ) ) )
144 36 38 8 subdird ⊢ ( 𝜑 → ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) = ( ( 𝑃 · 𝑋 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
145 144 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 · 𝑋 ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) ) )
146 136 143 145 3eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) )
147 146 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑃 · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) )
148 132 134 147 3eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) )
149 78 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐷 ) ) ∈ ℂ )
150 19 20 17 subne0d ⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) ≠ 0 )
151 21 150 absne0d ⊢ ( 𝜑 → ( abs ‘ ( 𝐸 − 𝐹 ) ) ≠ 0 )
152 11 151 eqnetrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) ≠ 0 )
153 78 abs00ad ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) = 0 ↔ ( 𝑋 − 𝐷 ) = 0 ) )
154 153 necon3bid ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) ≠ 0 ↔ ( 𝑋 − 𝐷 ) ≠ 0 ) )
155 152 154 mpbid ⊢ ( 𝜑 → ( 𝑋 − 𝐷 ) ≠ 0 )
156 11 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) )
157 78 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐷 ) ) ↑ 2 ) = ( ( 𝑋 − 𝐷 ) · ( ∗ ‘ ( 𝑋 − 𝐷 ) ) ) )
158 21 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
159 156 157 158 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐷 ) · ( ∗ ‘ ( 𝑋 − 𝐷 ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
160 159 13 eqtr4di ⊢ ( 𝜑 → ( ( 𝑋 − 𝐷 ) · ( ∗ ‘ ( 𝑋 − 𝐷 ) ) ) = 𝑄 )
161 78 149 155 160 mvllmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐷 ) ) = ( 𝑄 / ( 𝑋 − 𝐷 ) ) )
162 161 149 eqeltrrd ⊢ ( 𝜑 → ( 𝑄 / ( 𝑋 − 𝐷 ) ) ∈ ℂ )
163 26 162 addcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) ∈ ℂ )
164 163 78 77 mulassd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) )
165 24 78 155 divcan1d ⊢ ( 𝜑 → ( ( 𝑄 / ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐷 ) ) = 𝑄 )
166 165 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) + ( ( 𝑄 / ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) + 𝑄 ) )
167 26 78 162 166 joinlmuladdmuld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( 𝑋 − 𝐷 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) + 𝑄 ) )
168 167 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) + 𝑄 ) · ( 𝑋 − 𝐴 ) ) )
169 26 78 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) ∈ ℂ )
170 169 24 77 adddird ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) + 𝑄 ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) + ( 𝑄 · ( 𝑋 − 𝐴 ) ) ) )
171 26 78 77 mulassd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) )
172 79 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) )
173 171 172 eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) )
174 111 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 − 𝐴 ) · ( 𝑋 − 𝐷 ) ) ) = ( ( ∗ ‘ 𝐷 ) · ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) ) )
175 26 113 51 adddid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) + ( 𝐷 · 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) )
176 173 174 175 3eqtrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) )
177 24 8 27 subdid ⊢ ( 𝜑 → ( 𝑄 · ( 𝑋 − 𝐴 ) ) = ( ( 𝑄 · 𝑋 ) − ( 𝑄 · 𝐴 ) ) )
178 176 177 oveq12d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) + ( 𝑄 · ( 𝑋 − 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑄 · 𝑋 ) − ( 𝑄 · 𝐴 ) ) ) )
179 168 170 178 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( 𝑋 − 𝐷 ) ) · ( 𝑋 − 𝐴 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑄 · 𝑋 ) − ( 𝑄 · 𝐴 ) ) ) )
180 8 25 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐷 ) ) = ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐷 ) ) )
181 180 161 eqtr3d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐷 ) ) = ( 𝑄 / ( 𝑋 − 𝐷 ) ) )
182 121 26 162 subaddd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝑋 ) − ( ∗ ‘ 𝐷 ) ) = ( 𝑄 / ( 𝑋 − 𝐷 ) ) ↔ ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) = ( ∗ ‘ 𝑋 ) ) )
183 181 182 mpbid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) = ( ∗ ‘ 𝑋 ) )
184 183 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) + ( 𝑄 / ( 𝑋 − 𝐷 ) ) ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) = ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) )
185 164 179 184 3eqtr3rd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑄 · 𝑋 ) − ( 𝑄 · 𝐴 ) ) ) )
186 26 113 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) ∈ ℂ )
187 186 55 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) ∈ ℂ )
188 24 8 mulcld ⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) ∈ ℂ )
189 187 188 56 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑄 · 𝑋 ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( 𝑄 · 𝑋 ) − ( 𝑄 · 𝐴 ) ) ) )
190 186 55 188 add32d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑄 · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) )
191 190 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( 𝑄 · 𝑋 ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑄 · 𝐴 ) ) )
192 185 189 191 3eqtr2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) = ( ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑄 · 𝐴 ) ) )
193 186 188 addcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) ∈ ℂ )
194 193 55 56 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
195 29 8 mulcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ∈ ℂ )
196 72 195 188 subadd23d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) + ( 𝑄 · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 · 𝑋 ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) ) )
197 26 18 109 subdid ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) )
198 26 8 28 mul12d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( 𝑋 · ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) )
199 8 29 mulcomd ⊢ ( 𝜑 → ( 𝑋 · ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) )
200 198 199 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) )
201 200 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
202 197 201 eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
203 202 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) + ( 𝑄 · 𝑋 ) ) )
204 24 29 8 subdird ⊢ ( 𝜑 → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) = ( ( 𝑄 · 𝑋 ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) )
205 204 oveq2d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 · 𝑋 ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) · 𝑋 ) ) ) )
206 196 203 205 3eqtr4d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) )
207 206 oveq1d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 · ( 𝐷 + 𝐴 ) ) ) ) + ( 𝑄 · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
208 192 194 207 3eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) · ( ( 𝑋 − 𝐷 ) · ( 𝑋 − 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
209 80 148 208 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
210 146 133 eqeltrrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ∈ ℂ )
211 206 193 eqeltrrd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ∈ ℂ )
212 210 54 211 57 addsubeq4d ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) ) = ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) + ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) ↔ ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) ) )
213 209 212 mpbid ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) − ( ( ( ∗ ‘ 𝐴 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) · 𝑋 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
214 71 76 213 3eqtr2d ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝑋 ↑ 2 ) ) + ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) )
215 67 68 214 mvlraddd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝑋 ↑ 2 ) ) = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) − ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) )
216 41 18 47 215 mvllmuld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) = ( ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) − ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
217 58 68 41 47 divsubdird ⊢ ( 𝜑 → ( ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) − ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) − ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ) )
218 65 oveq1d ⊢ ( 𝜑 → ( - 𝑁 − ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ) = ( ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) − ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ) )
219 217 218 eqtr4d ⊢ ( 𝜑 → ( ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) − ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( - 𝑁 − ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ) )
220 40 8 41 47 div23d ⊢ ( 𝜑 → ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) · 𝑋 ) )
221 14 oveq1i ⊢ ( 𝑀 · 𝑋 ) = ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) · 𝑋 )
222 220 221 eqtr4di ⊢ ( 𝜑 → ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( 𝑀 · 𝑋 ) )
223 222 oveq2d ⊢ ( 𝜑 → ( - 𝑁 − ( ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) · 𝑋 ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) ) = ( - 𝑁 − ( 𝑀 · 𝑋 ) ) )
224 216 219 223 3eqtrd ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) = ( - 𝑁 − ( 𝑀 · 𝑋 ) ) )
225 66 50 224 mvrrsubd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) = - 𝑁 )
226 18 50 addcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) ∈ ℂ )
227 addeq0 ⊢ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) + 𝑁 ) = 0 ↔ ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) = - 𝑁 ) )
228 226 61 227 syl2anc ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) + 𝑁 ) = 0 ↔ ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) = - 𝑁 ) )
229 225 228 mpbird ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑀 · 𝑋 ) ) + 𝑁 ) = 0 )
230 62 229 eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )