Metamath Proof Explorer

Theorem constrrtcc

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (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 ⊢ 𝑁 = - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
Assertion constrrtcc ( 𝜑 → ( ( 𝑋 ↑ 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 14 a1i ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑀 = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
17 1 6 sseldd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
18 1 7 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
19 17 18 subcld ⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) ∈ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐸 − 𝐹 ) ∈ ℂ )
21 20 absvalsqd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
22 13 21 eqtr4id ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑄 = ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑋 ∈ ℂ )
24 1 2 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐴 ∈ ℂ )
26 8 24 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑋 − 𝐴 ) ∈ ℂ )
28 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
29 1 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ ℂ )
31 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
32 30 31 subeq0bd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐶 ) = 0 )
33 32 abs00bd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) = 0 )
34 28 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = 0 )
35 27 34 abs00d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑋 − 𝐴 ) = 0 )
36 23 25 35 subeq0d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑋 = 𝐴 )
37 36 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐴 − 𝐷 ) ) )
38 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
39 1 5 sseldd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐷 ∈ ℂ )
41 25 40 abssubd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝐴 − 𝐷 ) ) = ( abs ‘ ( 𝐷 − 𝐴 ) ) )
42 37 38 41 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝐸 − 𝐹 ) ) = ( abs ‘ ( 𝐷 − 𝐴 ) ) )
43 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐷 − 𝐴 ) ) ↑ 2 ) )
44 39 24 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ∈ ℂ )
45 44 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐷 − 𝐴 ) ) ↑ 2 ) = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( abs ‘ ( 𝐷 − 𝐴 ) ) ↑ 2 ) = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
47 22 43 46 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑄 = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
48 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) )
49 32 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) = ( 0 · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) )
50 1 4 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
51 29 50 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
52 51 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
54 53 mul02d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 0 · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) = 0 )
55 49 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) = 0 )
56 12 55 eqtrid ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 = 0 )
57 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( 0 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) )
58 48 57 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 0 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
59 44 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
60 59 cjcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ∈ ℂ )
61 59 60 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ∈ ℂ )
62 40 cjcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ 𝐷 ) ∈ ℂ )
63 40 25 addcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐷 + 𝐴 ) ∈ ℂ )
64 62 63 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
65 0cnd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 0 ∈ ℂ )
66 25 cjcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
67 66 63 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
68 61 64 65 67 sub4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 0 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − 0 ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
69 61 subid1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − 0 ) = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
70 39 24 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
71 70 oveq1d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 + 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 + 𝐴 ) ) )
72 44 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ∈ ℂ )
73 39 24 addcld ⊢ ( 𝜑 → ( 𝐷 + 𝐴 ) ∈ ℂ )
74 72 73 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 + 𝐴 ) ) = ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
75 39 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐷 ) ∈ ℂ )
76 24 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℂ )
77 75 76 73 subdird ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 + 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) )
78 71 74 77 3eqtr3rd ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
80 69 79 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − 0 ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
81 58 68 80 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
82 59 63 60 subdird ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) − ( 𝐷 + 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
83 63 59 negsubdi2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( ( 𝐷 + 𝐴 ) − ( 𝐷 − 𝐴 ) ) = ( ( 𝐷 − 𝐴 ) − ( 𝐷 + 𝐴 ) ) )
84 40 25 25 pnncand ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 + 𝐴 ) − ( 𝐷 − 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
85 25 2timesd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
86 84 85 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 + 𝐴 ) − ( 𝐷 − 𝐴 ) ) = ( 2 · 𝐴 ) )
87 86 negeqd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( ( 𝐷 + 𝐴 ) − ( 𝐷 − 𝐴 ) ) = - ( 2 · 𝐴 ) )
88 83 87 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 − 𝐴 ) − ( 𝐷 + 𝐴 ) ) = - ( 2 · 𝐴 ) )
89 88 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) − ( 𝐷 + 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( - ( 2 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
90 81 82 89 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( - ( 2 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
91 70 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
92 90 91 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( - ( 2 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
93 2cnd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 2 ∈ ℂ )
94 93 25 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 2 · 𝐴 ) ∈ ℂ )
95 94 negcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 2 · 𝐴 ) ∈ ℂ )
96 9 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
97 39 24 96 subne0d ⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ≠ 0 )
98 44 97 cjne0d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ≠ 0 )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ≠ 0 )
100 95 60 99 divcan4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( - ( 2 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( 2 · 𝐴 ) )
101 16 92 100 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑀 = - ( 2 · 𝐴 ) )
102 101 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑀 · 𝑋 ) = ( - ( 2 · 𝐴 ) · 𝑋 ) )
103 94 23 mulneg1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( - ( 2 · 𝐴 ) · 𝑋 ) = - ( ( 2 · 𝐴 ) · 𝑋 ) )
104 93 25 23 mulassd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 2 · 𝐴 ) · 𝑋 ) = ( 2 · ( 𝐴 · 𝑋 ) ) )
105 25 23 mulcomd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐴 · 𝑋 ) = ( 𝑋 · 𝐴 ) )
106 105 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 2 · ( 𝐴 · 𝑋 ) ) = ( 2 · ( 𝑋 · 𝐴 ) ) )
107 104 106 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 2 · 𝐴 ) · 𝑋 ) = ( 2 · ( 𝑋 · 𝐴 ) ) )
108 107 negeqd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( ( 2 · 𝐴 ) · 𝑋 ) = - ( 2 · ( 𝑋 · 𝐴 ) ) )
109 102 103 108 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑀 · 𝑋 ) = - ( 2 · ( 𝑋 · 𝐴 ) ) )
110 25 sqcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
111 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑃 · 𝐷 ) = ( 0 · 𝐷 ) )
112 40 mul02d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 0 · 𝐷 ) = 0 )
113 111 112 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑃 · 𝐷 ) = 0 )
114 113 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − 0 ) )
115 40 25 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐷 · 𝐴 ) ∈ ℂ )
116 66 115 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
117 116 subid1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − 0 ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) )
118 114 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) )
119 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑄 · 𝐴 ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) )
120 119 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) )
121 118 120 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) ) )
122 62 115 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
123 61 25 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ∈ ℂ )
124 116 122 123 subsubd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) )
125 70 negeqd ⊢ ( 𝜑 → - ( ∗ ‘ ( 𝐷 − 𝐴 ) ) = - ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
126 75 76 negsubdi2d ⊢ ( 𝜑 → - ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐷 ) ) )
127 125 126 eqtr2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐷 ) ) = - ( ∗ ‘ ( 𝐷 − 𝐴 ) ) )
128 127 oveq1d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐷 ) ) · ( 𝐷 · 𝐴 ) ) = ( - ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) )
129 39 24 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℂ )
130 76 75 129 subdird ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐷 ) ) · ( 𝐷 · 𝐴 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) )
131 72 129 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
132 131 negeqd ⊢ ( 𝜑 → - ( ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) = - ( ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
133 72 129 mulneg1d ⊢ ( 𝜑 → ( - ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) = - ( ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) )
134 129 72 mulneg1d ⊢ ( 𝜑 → ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
135 132 133 134 3eqtr4d ⊢ ( 𝜑 → ( - ( ∗ ‘ ( 𝐷 − 𝐴 ) ) · ( 𝐷 · 𝐴 ) ) = ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
136 128 130 135 3eqtr3d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) = ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
137 136 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) = ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
138 59 60 25 mul32d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) = ( ( ( 𝐷 − 𝐴 ) · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
139 40 25 25 subdird ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 − 𝐴 ) · 𝐴 ) = ( ( 𝐷 · 𝐴 ) − ( 𝐴 · 𝐴 ) ) )
140 25 sqvald ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
141 140 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) = ( ( 𝐷 · 𝐴 ) − ( 𝐴 · 𝐴 ) ) )
142 139 141 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 − 𝐴 ) · 𝐴 ) = ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) )
143 142 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
144 138 143 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
145 137 144 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) = ( ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) + ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
146 115 negcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 𝐷 · 𝐴 ) ∈ ℂ )
147 115 110 subcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
148 146 147 60 adddird ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( - ( 𝐷 · 𝐴 ) + ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) + ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
149 115 subidd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) = 0 )
150 149 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) − ( 𝐴 ↑ 2 ) ) = ( 0 − ( 𝐴 ↑ 2 ) ) )
151 146 147 addcomd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( - ( 𝐷 · 𝐴 ) + ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) + - ( 𝐷 · 𝐴 ) ) )
152 147 115 negsubd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) + - ( 𝐷 · 𝐴 ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) − ( 𝐷 · 𝐴 ) ) )
153 115 110 115 sub32d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) − ( 𝐷 · 𝐴 ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) − ( 𝐴 ↑ 2 ) ) )
154 151 152 153 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( - ( 𝐷 · 𝐴 ) + ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) − ( 𝐴 ↑ 2 ) ) )
155 df-neg ⊢ - ( 𝐴 ↑ 2 ) = ( 0 − ( 𝐴 ↑ 2 ) )
156 155 a1i ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 𝐴 ↑ 2 ) = ( 0 − ( 𝐴 ↑ 2 ) ) )
157 150 154 156 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( - ( 𝐷 · 𝐴 ) + ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ) = - ( 𝐴 ↑ 2 ) )
158 157 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( - ( 𝐷 · 𝐴 ) + ( ( 𝐷 · 𝐴 ) − ( 𝐴 ↑ 2 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( - ( 𝐴 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
159 145 148 158 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) + ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐴 ) ) = ( - ( 𝐴 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
160 121 124 159 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) = ( - ( 𝐴 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
161 91 eqcomd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( 𝐷 − 𝐴 ) ) )
162 160 161 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( - ( 𝐴 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
163 110 negcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 𝐴 ↑ 2 ) ∈ ℂ )
164 163 60 99 divcan4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( - ( 𝐴 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( 𝐴 ↑ 2 ) )
165 162 164 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 𝐴 ↑ 2 ) = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
166 110 165 negcon1ad ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( 𝐴 ↑ 2 ) )
167 15 166 eqtrid ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑁 = ( 𝐴 ↑ 2 ) )
168 109 167 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑀 · 𝑋 ) + 𝑁 ) = ( - ( 2 · ( 𝑋 · 𝐴 ) ) + ( 𝐴 ↑ 2 ) ) )
169 168 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = ( ( 𝑋 ↑ 2 ) + ( - ( 2 · ( 𝑋 · 𝐴 ) ) + ( 𝐴 ↑ 2 ) ) ) )
170 23 sqcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑋 ↑ 2 ) ∈ ℂ )
171 23 25 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝑋 · 𝐴 ) ∈ ℂ )
172 93 171 mulcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 2 · ( 𝑋 · 𝐴 ) ) ∈ ℂ )
173 172 negcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → - ( 2 · ( 𝑋 · 𝐴 ) ) ∈ ℂ )
174 170 173 110 addassd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( - ( 2 · ( 𝑋 · 𝐴 ) ) + ( 𝐴 ↑ 2 ) ) ) )
175 170 172 negsubd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐴 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐴 ) ) ) )
176 175 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) )
177 169 174 176 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) )
178 binom2sub ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑋 − 𝐴 ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) )
179 23 25 178 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 − 𝐴 ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐴 ) ) ) + ( 𝐴 ↑ 2 ) ) )
180 35 sq0id ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 − 𝐴 ) ↑ 2 ) = 0 )
181 177 179 180 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )
182 14 a1i ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑀 = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
183 17 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝐸 ∈ ℂ )
184 simpr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝐸 = 𝐹 )
185 183 184 subeq0bd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐸 − 𝐹 ) = 0 )
186 185 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) = ( 0 · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
187 19 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ∈ ℂ )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ∈ ℂ )
189 188 mul02d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 0 · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) = 0 )
190 186 189 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) = 0 )
191 13 190 eqtrid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑄 = 0 )
192 191 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) = ( 0 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) )
193 51 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
194 193 absvalsqd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) = ( ( 𝐵 − 𝐶 ) · ( ∗ ‘ ( 𝐵 − 𝐶 ) ) ) )
195 12 194 eqtr4id ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑃 = ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) )
196 10 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
197 8 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑋 ∈ ℂ )
198 39 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝐷 ∈ ℂ )
199 8 39 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐷 ) ∈ ℂ )
200 199 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑋 − 𝐷 ) ∈ ℂ )
201 11 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
202 185 abs00bd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝐸 − 𝐹 ) ) = 0 )
203 201 202 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = 0 )
204 200 203 abs00d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑋 − 𝐷 ) = 0 )
205 197 198 204 subeq0d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑋 = 𝐷 )
206 205 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐷 − 𝐴 ) ) )
207 196 206 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) = ( abs ‘ ( 𝐷 − 𝐴 ) ) )
208 207 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐷 − 𝐴 ) ) ↑ 2 ) )
209 45 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( abs ‘ ( 𝐷 − 𝐴 ) ) ↑ 2 ) = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
210 195 208 209 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑃 = ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
211 210 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) )
212 192 211 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( 0 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
213 0cnd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 0 ∈ ℂ )
214 198 cjcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ 𝐷 ) ∈ ℂ )
215 24 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝐴 ∈ ℂ )
216 198 215 addcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 + 𝐴 ) ∈ ℂ )
217 214 216 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
218 44 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
219 218 cjcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ∈ ℂ )
220 218 219 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ∈ ℂ )
221 215 cjcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
222 221 216 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ∈ ℂ )
223 213 217 220 222 sub4d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 0 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( 0 − ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
224 218 219 mulneg1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
225 198 215 negsubdi2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 𝐷 − 𝐴 ) = ( 𝐴 − 𝐷 ) )
226 225 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( 𝐴 − 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
227 df-neg ⊢ - ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( 0 − ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
228 227 a1i ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( 0 − ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
229 224 226 228 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 0 − ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) = ( ( 𝐴 − 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
230 78 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) = ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
231 229 230 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 0 − ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( 𝐴 − 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
232 212 223 231 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) = ( ( ( 𝐴 − 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
233 215 198 subcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐴 − 𝐷 ) ∈ ℂ )
234 233 216 219 subdird ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐴 − 𝐷 ) − ( 𝐷 + 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝐴 − 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( 𝐷 + 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
235 216 233 negsubdi2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( ( 𝐷 + 𝐴 ) − ( 𝐴 − 𝐷 ) ) = ( ( 𝐴 − 𝐷 ) − ( 𝐷 + 𝐴 ) ) )
236 198 2timesd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 2 · 𝐷 ) = ( 𝐷 + 𝐷 ) )
237 215 198 198 pnncand ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐴 + 𝐷 ) − ( 𝐴 − 𝐷 ) ) = ( 𝐷 + 𝐷 ) )
238 215 198 addcomd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐴 + 𝐷 ) = ( 𝐷 + 𝐴 ) )
239 238 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐴 + 𝐷 ) − ( 𝐴 − 𝐷 ) ) = ( ( 𝐷 + 𝐴 ) − ( 𝐴 − 𝐷 ) ) )
240 236 237 239 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 + 𝐴 ) − ( 𝐴 − 𝐷 ) ) = ( 2 · 𝐷 ) )
241 240 negeqd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( ( 𝐷 + 𝐴 ) − ( 𝐴 − 𝐷 ) ) = - ( 2 · 𝐷 ) )
242 235 241 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐴 − 𝐷 ) − ( 𝐷 + 𝐴 ) ) = - ( 2 · 𝐷 ) )
243 242 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐴 − 𝐷 ) − ( 𝐷 + 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( - ( 2 · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
244 232 234 243 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 2 · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) )
245 70 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) )
246 244 245 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 2 · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝑄 − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 + 𝐴 ) ) ) − ( 𝑃 − ( ( ∗ ‘ 𝐴 ) · ( 𝐷 + 𝐴 ) ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
247 2cnd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 2 ∈ ℂ )
248 247 198 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 2 · 𝐷 ) ∈ ℂ )
249 248 negcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 2 · 𝐷 ) ∈ ℂ )
250 98 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ≠ 0 )
251 249 219 250 divcan4d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 2 · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( 2 · 𝐷 ) )
252 182 246 251 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑀 = - ( 2 · 𝐷 ) )
253 252 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑀 · 𝑋 ) = ( - ( 2 · 𝐷 ) · 𝑋 ) )
254 248 197 mulneg1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 2 · 𝐷 ) · 𝑋 ) = - ( ( 2 · 𝐷 ) · 𝑋 ) )
255 247 198 197 mulassd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 2 · 𝐷 ) · 𝑋 ) = ( 2 · ( 𝐷 · 𝑋 ) ) )
256 198 197 mulcomd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 · 𝑋 ) = ( 𝑋 · 𝐷 ) )
257 256 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 2 · ( 𝐷 · 𝑋 ) ) = ( 2 · ( 𝑋 · 𝐷 ) ) )
258 255 257 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 2 · 𝐷 ) · 𝑋 ) = ( 2 · ( 𝑋 · 𝐷 ) ) )
259 258 negeqd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( ( 2 · 𝐷 ) · 𝑋 ) = - ( 2 · ( 𝑋 · 𝐷 ) ) )
260 253 254 259 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑀 · 𝑋 ) = - ( 2 · ( 𝑋 · 𝐷 ) ) )
261 198 sqcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
262 210 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑃 · 𝐷 ) = ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) )
263 262 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) = ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) )
264 191 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑄 · 𝐴 ) = ( 0 · 𝐴 ) )
265 215 mul02d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 0 · 𝐴 ) = 0 )
266 264 265 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑄 · 𝐴 ) = 0 )
267 266 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − 0 ) )
268 198 215 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 · 𝐴 ) ∈ ℂ )
269 214 268 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
270 269 subid1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − 0 ) = ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) )
271 267 270 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) = ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) )
272 263 271 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) )
273 221 268 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) ∈ ℂ )
274 220 198 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ∈ ℂ )
275 273 274 269 sub32d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) )
276 136 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) = ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
277 218 219 198 mul32d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) = ( ( ( 𝐷 − 𝐴 ) · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
278 198 215 198 subdird ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 − 𝐴 ) · 𝐷 ) = ( ( 𝐷 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) )
279 198 sqvald ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 ↑ 2 ) = ( 𝐷 · 𝐷 ) )
280 198 215 mulcomd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐷 · 𝐴 ) = ( 𝐴 · 𝐷 ) )
281 279 280 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) = ( ( 𝐷 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) )
282 278 281 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 − 𝐴 ) · 𝐷 ) = ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) )
283 282 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐷 − 𝐴 ) · 𝐷 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
284 277 283 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) = ( ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
285 276 284 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) = ( ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
286 268 negcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 𝐷 · 𝐴 ) ∈ ℂ )
287 261 268 subcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) ∈ ℂ )
288 286 287 219 subdird ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 𝐷 · 𝐴 ) − ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( ( - ( 𝐷 · 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) − ( ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) ) )
289 286 268 addcomd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 · 𝐴 ) + ( 𝐷 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) + - ( 𝐷 · 𝐴 ) ) )
290 268 268 negsubd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 · 𝐴 ) + - ( 𝐷 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) )
291 268 subidd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝐷 · 𝐴 ) − ( 𝐷 · 𝐴 ) ) = 0 )
292 289 290 291 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 · 𝐴 ) + ( 𝐷 · 𝐴 ) ) = 0 )
293 292 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 𝐷 · 𝐴 ) + ( 𝐷 · 𝐴 ) ) − ( 𝐷 ↑ 2 ) ) = ( 0 − ( 𝐷 ↑ 2 ) ) )
294 286 261 268 subsub3d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 · 𝐴 ) − ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) ) = ( ( - ( 𝐷 · 𝐴 ) + ( 𝐷 · 𝐴 ) ) − ( 𝐷 ↑ 2 ) ) )
295 df-neg ⊢ - ( 𝐷 ↑ 2 ) = ( 0 − ( 𝐷 ↑ 2 ) )
296 295 a1i ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 𝐷 ↑ 2 ) = ( 0 − ( 𝐷 ↑ 2 ) ) )
297 293 294 296 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( - ( 𝐷 · 𝐴 ) − ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) ) = - ( 𝐷 ↑ 2 ) )
298 297 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 𝐷 · 𝐴 ) − ( ( 𝐷 ↑ 2 ) − ( 𝐷 · 𝐴 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = ( - ( 𝐷 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
299 285 288 298 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) ) − ( ( ( 𝐷 − 𝐴 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) · 𝐷 ) ) = ( - ( 𝐷 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
300 272 275 299 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) = ( - ( 𝐷 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
301 245 eqcomd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( 𝐷 − 𝐴 ) ) )
302 300 301 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( - ( 𝐷 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) )
303 261 negcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 𝐷 ↑ 2 ) ∈ ℂ )
304 303 219 250 divcan4d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( - ( 𝐷 ↑ 2 ) · ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) / ( ∗ ‘ ( 𝐷 − 𝐴 ) ) ) = - ( 𝐷 ↑ 2 ) )
305 302 304 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 𝐷 ↑ 2 ) = ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) )
306 261 305 negcon1ad ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( ( ( ( ( ∗ ‘ 𝐴 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑃 · 𝐷 ) ) − ( ( ( ∗ ‘ 𝐷 ) · ( 𝐷 · 𝐴 ) ) − ( 𝑄 · 𝐴 ) ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐴 ) ) ) = ( 𝐷 ↑ 2 ) )
307 15 306 eqtrid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝑁 = ( 𝐷 ↑ 2 ) )
308 260 307 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑀 · 𝑋 ) + 𝑁 ) = ( - ( 2 · ( 𝑋 · 𝐷 ) ) + ( 𝐷 ↑ 2 ) ) )
309 308 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = ( ( 𝑋 ↑ 2 ) + ( - ( 2 · ( 𝑋 · 𝐷 ) ) + ( 𝐷 ↑ 2 ) ) ) )
310 197 sqcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑋 ↑ 2 ) ∈ ℂ )
311 197 198 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝑋 · 𝐷 ) ∈ ℂ )
312 247 311 mulcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 2 · ( 𝑋 · 𝐷 ) ) ∈ ℂ )
313 312 negcld ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → - ( 2 · ( 𝑋 · 𝐷 ) ) ∈ ℂ )
314 310 313 261 addassd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( - ( 2 · ( 𝑋 · 𝐷 ) ) + ( 𝐷 ↑ 2 ) ) ) )
315 310 312 negsubd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐷 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐷 ) ) ) )
316 315 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( ( 𝑋 ↑ 2 ) + - ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
317 309 314 316 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
318 binom2sub ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝑋 − 𝐷 ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
319 197 198 318 syl2anc ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 − 𝐷 ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) − ( 2 · ( 𝑋 · 𝐷 ) ) ) + ( 𝐷 ↑ 2 ) ) )
320 204 sq0id ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 − 𝐷 ) ↑ 2 ) = 0 )
321 317 319 320 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )
322 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝑆 ⊆ ℂ )
323 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐴 ∈ 𝑆 )
324 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐵 ∈ 𝑆 )
325 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐶 ∈ 𝑆 )
326 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐷 ∈ 𝑆 )
327 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐸 ∈ 𝑆 )
328 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐹 ∈ 𝑆 )
329 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝑋 ∈ ℂ )
330 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐴 ≠ 𝐷 )
331 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
332 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
333 simprl ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐵 ≠ 𝐶 )
334 simprr ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → 𝐸 ≠ 𝐹 )
335 322 323 324 325 326 327 328 329 330 331 332 12 13 14 15 333 334 constrrtcclem ⊢ ( ( 𝜑 ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹 ) ) → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )
336 181 321 335 pm2.61da2ne ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )