Metamath Proof Explorer

Theorem constrrtlc1

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

Ref Expression
Hypotheses constrrtlc.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
constrrtlc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
constrrtlc.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
constrrtlc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
constrrtlc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
constrrtlc.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
constrrtlc.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
constrrtlc.1 ⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
constrrtlc.2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
constrrtlc.q ⊢ 𝑄 = ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) )
constrrtlc.m ⊢ 𝑀 = ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 )
constrrtlc.n ⊢ 𝑁 = ( - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) / 𝑄 )
constrrtlc1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion constrrtlc1 ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 ∧ 𝑄 ≠ 0 ) )

Proof

Step Hyp Ref Expression
1 constrrtlc.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 constrrtlc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
3 constrrtlc.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
4 constrrtlc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
5 constrrtlc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
6 constrrtlc.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
7 constrrtlc.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
8 constrrtlc.1 ⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
9 constrrtlc.2 ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
10 constrrtlc.q ⊢ 𝑄 = ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) )
11 constrrtlc.m ⊢ 𝑀 = ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 )
12 constrrtlc.n ⊢ 𝑁 = ( - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) / 𝑄 )
13 constrrtlc1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
14 1 2 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
15 14 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℂ )
16 1 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
17 16 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐵 ) ∈ ℂ )
18 17 15 subcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
19 16 14 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
20 13 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
21 16 14 20 subne0d ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
22 18 19 21 divcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ∈ ℂ )
23 10 22 eqeltrid ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
24 14 23 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝑄 ) ∈ ℂ )
25 15 24 subcld ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) ∈ ℂ )
26 1 4 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
27 26 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝐶 ) ∈ ℂ )
28 25 27 subcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ∈ ℂ )
29 26 23 mulcld ⊢ ( 𝜑 → ( 𝐶 · 𝑄 ) ∈ ℂ )
30 28 29 subcld ⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ∈ ℂ )
31 16 14 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) = ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) )
32 19 21 cjne0d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ≠ 0 )
33 31 32 eqnetrrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ≠ 0 )
34 18 19 33 21 divne0d ⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ≠ 0 )
35 10 neeq1i ⊢ ( 𝑄 ≠ 0 ↔ ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ≠ 0 )
36 34 35 sylibr ⊢ ( 𝜑 → 𝑄 ≠ 0 )
37 30 23 36 divcld ⊢ ( 𝜑 → ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) ∈ ℂ )
38 7 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
39 38 19 mulcld ⊢ ( 𝜑 → ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ℂ )
40 14 39 addcld ⊢ ( 𝜑 → ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∈ ℂ )
41 8 40 eqeltrd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
42 37 41 mulcomd ⊢ ( 𝜑 → ( ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) · 𝑋 ) = ( 𝑋 · ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) ) )
43 11 a1i ⊢ ( 𝜑 → 𝑀 = ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) )
44 43 oveq1d ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) = ( ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) · 𝑋 ) )
45 41 30 23 36 divassd ⊢ ( 𝜑 → ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) / 𝑄 ) = ( 𝑋 · ( ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) / 𝑄 ) ) )
46 42 44 45 3eqtr4d ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) = ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) / 𝑄 ) )
47 12 a1i ⊢ ( 𝜑 → 𝑁 = ( - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) / 𝑄 ) )
48 46 47 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 · 𝑋 ) + 𝑁 ) = ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) / 𝑄 ) + ( - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) / 𝑄 ) ) )
49 41 30 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ∈ ℂ )
50 26 28 mulcld ⊢ ( 𝜑 → ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ∈ ℂ )
51 41 sqvald ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
52 51 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · 𝑄 ) = ( ( 𝑋 · 𝑋 ) · 𝑄 ) )
53 41 41 23 mulassd ⊢ ( 𝜑 → ( ( 𝑋 · 𝑋 ) · 𝑄 ) = ( 𝑋 · ( 𝑋 · 𝑄 ) ) )
54 52 53 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · 𝑄 ) = ( 𝑋 · ( 𝑋 · 𝑄 ) ) )
55 41 23 mulcld ⊢ ( 𝜑 → ( 𝑋 · 𝑄 ) ∈ ℂ )
56 41 55 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝑋 · 𝑄 ) ) ∈ ℂ )
57 54 56 eqeltrd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · 𝑄 ) ∈ ℂ )
58 57 49 50 addsubd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) )
59 54 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) )
60 41 28 29 subdid ⊢ ( 𝜑 → ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) = ( ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) − ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) )
61 59 60 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) = ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) − ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) ) )
62 41 28 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ∈ ℂ )
63 41 29 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝐶 · 𝑄 ) ) ∈ ℂ )
64 56 62 50 63 addsub4d ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) + ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) ) = ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) − ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) ) )
65 41 26 55 28 submuladdd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) · ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) + ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐶 · ( 𝑋 · 𝑄 ) ) + ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) ) )
66 9 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐶 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) )
67 41 26 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐶 ) ∈ ℂ )
68 67 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐶 ) ) ↑ 2 ) = ( ( 𝑋 − 𝐶 ) · ( ∗ ‘ ( 𝑋 − 𝐶 ) ) ) )
69 1 5 sseldd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
70 1 6 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
71 69 70 subcld ⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) ∈ ℂ )
72 71 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 − 𝐹 ) ) ↑ 2 ) = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
73 66 68 72 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) · ( ∗ ‘ ( 𝑋 − 𝐶 ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) )
74 8 fvoveq1d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐶 ) ) = ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) )
75 40 26 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) = ( ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) )
76 14 39 cjaddd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) )
77 38 19 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( ( ∗ ‘ 𝑇 ) · ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) )
78 7 cjred ⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = 𝑇 )
79 14 39 8 mvrladdd ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝑇 · ( 𝐵 − 𝐴 ) ) )
80 79 39 eqeltrd ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
81 80 38 19 21 divmul3d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) = 𝑇 ↔ ( 𝑋 − 𝐴 ) = ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
82 79 81 mpbird ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) = 𝑇 )
83 78 82 eqtr4d ⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) )
84 83 31 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑇 ) · ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) )
85 80 19 18 21 div32d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( 𝑋 − 𝐴 ) · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ) )
86 10 oveq2i ⊢ ( ( 𝑋 − 𝐴 ) · 𝑄 ) = ( ( 𝑋 − 𝐴 ) · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) )
87 85 86 eqtr4di ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) = ( ( 𝑋 − 𝐴 ) · 𝑄 ) )
88 41 14 23 subdird ⊢ ( 𝜑 → ( ( 𝑋 − 𝐴 ) · 𝑄 ) = ( ( 𝑋 · 𝑄 ) − ( 𝐴 · 𝑄 ) ) )
89 84 87 88 3eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑇 ) · ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) = ( ( 𝑋 · 𝑄 ) − ( 𝐴 · 𝑄 ) ) )
90 77 89 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( ( 𝑋 · 𝑄 ) − ( 𝐴 · 𝑄 ) ) )
91 90 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ( 𝑋 · 𝑄 ) − ( 𝐴 · 𝑄 ) ) ) )
92 15 55 24 addsub12d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( ( 𝑋 · 𝑄 ) − ( 𝐴 · 𝑄 ) ) ) = ( ( 𝑋 · 𝑄 ) + ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) ) )
93 76 91 92 3eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( 𝑋 · 𝑄 ) + ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) ) )
94 93 oveq1d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) = ( ( ( 𝑋 · 𝑄 ) + ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) ) − ( ∗ ‘ 𝐶 ) ) )
95 55 25 27 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑄 ) + ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) ) − ( ∗ ‘ 𝐶 ) ) = ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) )
96 75 94 95 3eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) = ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) )
97 74 96 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 − 𝐶 ) ) = ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) )
98 97 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) · ( ∗ ‘ ( 𝑋 − 𝐶 ) ) ) = ( ( 𝑋 − 𝐶 ) · ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) )
99 69 70 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐸 − 𝐹 ) ) = ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) )
100 99 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 − 𝐹 ) · ( ∗ ‘ ( 𝐸 − 𝐹 ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) )
101 73 98 100 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐶 ) · ( ( 𝑋 · 𝑄 ) + ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) )
102 26 41 23 mul12d ⊢ ( 𝜑 → ( 𝐶 · ( 𝑋 · 𝑄 ) ) = ( 𝑋 · ( 𝐶 · 𝑄 ) ) )
103 102 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑋 · 𝑄 ) ) + ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝑋 · ( 𝐶 · 𝑄 ) ) + ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) )
104 63 50 103 comraddd ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑋 · 𝑄 ) ) + ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) )
105 104 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) + ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐶 · ( 𝑋 · 𝑄 ) ) + ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) + ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) ) )
106 65 101 105 3eqtr3rd ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝑋 · 𝑄 ) ) + ( 𝑋 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( 𝑋 · ( 𝐶 · 𝑄 ) ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) )
107 61 64 106 3eqtr2d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) )
108 58 107 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) )
109 57 49 addcld ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) ∈ ℂ )
110 109 50 subcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) ∈ ℂ )
111 108 110 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ∈ ℂ )
112 50 111 addcld ⊢ ( 𝜑 → ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ∈ ℂ )
113 112 negcld ⊢ ( 𝜑 → - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ∈ ℂ )
114 49 113 23 36 divdird ⊢ ( 𝜑 → ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) / 𝑄 ) = ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) / 𝑄 ) + ( - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) / 𝑄 ) ) )
115 48 114 eqtr4d ⊢ ( 𝜑 → ( ( 𝑀 · 𝑋 ) + 𝑁 ) = ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) / 𝑄 ) )
116 115 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) / 𝑄 ) ) )
117 41 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
118 49 113 addcld ⊢ ( 𝜑 → ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ∈ ℂ )
119 117 23 118 36 muldivdid ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) / 𝑄 ) = ( ( 𝑋 ↑ 2 ) + ( ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) / 𝑄 ) ) )
120 57 49 113 addassd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) = ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) )
121 109 112 negsubd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) = ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) )
122 109 50 111 subsub4d ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) = ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) )
123 110 108 subeq0bd ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) − ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) ) − ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) = 0 )
124 121 122 123 3eqtr2d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) = 0 )
125 120 124 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) = 0 )
126 57 118 addcld ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) ∈ ℂ )
127 126 23 36 diveq0ad ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) / 𝑄 ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) = 0 ) )
128 125 127 mpbird ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) · 𝑄 ) + ( ( 𝑋 · ( ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) − ( 𝐶 · 𝑄 ) ) ) + - ( ( 𝐶 · ( ( ( ∗ ‘ 𝐴 ) − ( 𝐴 · 𝑄 ) ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐸 − 𝐹 ) · ( ( ∗ ‘ 𝐸 ) − ( ∗ ‘ 𝐹 ) ) ) ) ) ) / 𝑄 ) = 0 )
129 116 119 128 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 )
130 129 36 jca ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 · 𝑋 ) + 𝑁 ) ) = 0 ∧ 𝑄 ≠ 0 ) )