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