Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  constrrtcc Structured version   Visualization version   GIF version

Theorem constrrtcc 33718
Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (Contributed by Thierry Arnoux, 6-Jul-2025.)
Hypotheses
Ref Expression
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
Ref Expression
constrrtcc (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Proof of Theorem constrrtcc
StepHypRef Expression
1 constrrtcc.m . . . . . . . . . 10 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
21a1i 11 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
3 constrrtcc.5 . . . . . . . . . . . . . . . 16 𝑄 = ((𝐸𝐹) · (∗‘(𝐸𝐹)))
4 constrrtcc.s . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆 ⊆ ℂ)
5 constrrtcc.e . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸𝑆)
64, 5sseldd 4003 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐸 ∈ ℂ)
7 constrrtcc.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹𝑆)
84, 7sseldd 4003 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 ∈ ℂ)
96, 8subcld 11643 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝐹) ∈ ℂ)
109adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (𝐸𝐹) ∈ ℂ)
1110absvalsqd 15487 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → ((abs‘(𝐸𝐹))↑2) = ((𝐸𝐹) · (∗‘(𝐸𝐹))))
123, 11eqtr4id 2793 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → 𝑄 = ((abs‘(𝐸𝐹))↑2))
13 constrrtcc.x . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋 ∈ ℂ)
1413adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵 = 𝐶) → 𝑋 ∈ ℂ)
15 constrrtcc.a . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴𝑆)
164, 15sseldd 4003 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℂ)
1716adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵 = 𝐶) → 𝐴 ∈ ℂ)
1813, 16subcld 11643 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝐴) ∈ ℂ)
1918adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵 = 𝐶) → (𝑋𝐴) ∈ ℂ)
20 constrrtcc.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (abs‘(𝑋𝐴)) = (abs‘(𝐵𝐶)))
2120adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵 = 𝐶) → (abs‘(𝑋𝐴)) = (abs‘(𝐵𝐶)))
22 constrrtcc.b . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵𝑆)
234, 22sseldd 4003 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ∈ ℂ)
2423adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵 = 𝐶) → 𝐵 ∈ ℂ)
25 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵 = 𝐶) → 𝐵 = 𝐶)
2624, 25subeq0bd 11712 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵 = 𝐶) → (𝐵𝐶) = 0)
2726abs00bd 15336 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵 = 𝐶) → (abs‘(𝐵𝐶)) = 0)
2821, 27eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵 = 𝐶) → (abs‘(𝑋𝐴)) = 0)
2919, 28abs00d 15491 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵 = 𝐶) → (𝑋𝐴) = 0)
3014, 17, 29subeq0d 11651 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵 = 𝐶) → 𝑋 = 𝐴)
3130fvoveq1d 7467 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (abs‘(𝑋𝐷)) = (abs‘(𝐴𝐷)))
32 constrrtcc.3 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘(𝑋𝐷)) = (abs‘(𝐸𝐹)))
3332adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (abs‘(𝑋𝐷)) = (abs‘(𝐸𝐹)))
34 constrrtcc.d . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷𝑆)
354, 34sseldd 4003 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ∈ ℂ)
3635adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵 = 𝐶) → 𝐷 ∈ ℂ)
3717, 36abssubd 15498 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (abs‘(𝐴𝐷)) = (abs‘(𝐷𝐴)))
3831, 33, 373eqtr3d 2782 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → (abs‘(𝐸𝐹)) = (abs‘(𝐷𝐴)))
3938oveq1d 7460 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((abs‘(𝐸𝐹))↑2) = ((abs‘(𝐷𝐴))↑2))
4035, 16subcld 11643 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷𝐴) ∈ ℂ)
4140absvalsqd 15487 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐷𝐴))↑2) = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
4241adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((abs‘(𝐷𝐴))↑2) = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
4312, 39, 423eqtrd 2778 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → 𝑄 = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
4443oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))))
45 constrrtcc.4 . . . . . . . . . . . . . . 15 𝑃 = ((𝐵𝐶) · (∗‘(𝐵𝐶)))
4626oveq1d 7460 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → ((𝐵𝐶) · (∗‘(𝐵𝐶))) = (0 · (∗‘(𝐵𝐶))))
47 constrrtcc.c . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑆)
484, 47sseldd 4003 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐶 ∈ ℂ)
4923, 48subcld 11643 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝐶) ∈ ℂ)
5049cjcld 15241 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝐵𝐶)) ∈ ℂ)
5150adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (∗‘(𝐵𝐶)) ∈ ℂ)
5251mul02d 11484 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → (0 · (∗‘(𝐵𝐶))) = 0)
5346, 52eqtrd 2774 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((𝐵𝐶) · (∗‘(𝐵𝐶))) = 0)
5445, 53eqtrid 2786 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → 𝑃 = 0)
5554oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐴) · (𝐷 + 𝐴))))
5644, 55oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
5740adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (𝐷𝐴) ∈ ℂ)
5857cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (∗‘(𝐷𝐴)) ∈ ℂ)
5957, 58mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → ((𝐷𝐴) · (∗‘(𝐷𝐴))) ∈ ℂ)
6036cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (∗‘𝐷) ∈ ℂ)
6136, 17addcld 11305 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (𝐷 + 𝐴) ∈ ℂ)
6260, 61mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
63 0cnd 11279 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → 0 ∈ ℂ)
6417cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (∗‘𝐴) ∈ ℂ)
6564, 61mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
6659, 62, 63, 65sub4d 11692 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷𝐴) · (∗‘(𝐷𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
6759subid1d 11632 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) − 0) = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
6835, 16cjsubd 32747 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝐷𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
6968oveq1d 7460 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘(𝐷𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)))
7040cjcld 15241 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝐷𝐴)) ∈ ℂ)
7135, 16addcld 11305 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
7270, 71mulcomd 11307 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘(𝐷𝐴)) · (𝐷 + 𝐴)) = ((𝐷 + 𝐴) · (∗‘(𝐷𝐴))))
7335cjcld 15241 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘𝐷) ∈ ℂ)
7416cjcld 15241 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘𝐴) ∈ ℂ)
7573, 74, 71subdird 11743 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))))
7669, 72, 753eqtr3rd 2783 . . . . . . . . . . . . . 14 (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷𝐴))))
7776adantr 480 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷𝐴))))
7867, 77oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((((𝐷𝐴) · (∗‘(𝐷𝐴))) − 0) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
7956, 66, 783eqtrd 2778 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
8057, 61, 58subdird 11743 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷𝐴))) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
8161, 57negsubdi2d 11659 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷𝐴)) = ((𝐷𝐴) − (𝐷 + 𝐴)))
8236, 17, 17pnncand 11682 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷𝐴)) = (𝐴 + 𝐴))
83172timesd 12532 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (2 · 𝐴) = (𝐴 + 𝐴))
8482, 83eqtr4d 2777 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷𝐴)) = (2 · 𝐴))
8584negeqd 11526 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷𝐴)) = -(2 · 𝐴))
8681, 85eqtr3d 2776 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((𝐷𝐴) − (𝐷 + 𝐴)) = -(2 · 𝐴))
8786oveq1d 7460 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷𝐴))) = (-(2 · 𝐴) · (∗‘(𝐷𝐴))))
8879, 80, 873eqtr2rd 2781 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → (-(2 · 𝐴) · (∗‘(𝐷𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
8968adantr 480 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → (∗‘(𝐷𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
9088, 89oveq12d 7463 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
91 2cnd 12367 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → 2 ∈ ℂ)
9291, 17mulcld 11306 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → (2 · 𝐴) ∈ ℂ)
9392negcld 11630 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → -(2 · 𝐴) ∈ ℂ)
94 constrrtcc.1 . . . . . . . . . . . . . 14 (𝜑𝐴𝐷)
9594necomd 2998 . . . . . . . . . . . . 13 (𝜑𝐷𝐴)
9635, 16, 95subne0d 11652 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐴) ≠ 0)
9740, 96cjne0d 15248 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐷𝐴)) ≠ 0)
9897adantr 480 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → (∗‘(𝐷𝐴)) ≠ 0)
9993, 58, 98divcan4d 12072 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = -(2 · 𝐴))
1002, 90, 993eqtr2d 2780 . . . . . . . 8 ((𝜑𝐵 = 𝐶) → 𝑀 = -(2 · 𝐴))
101100oveq1d 7460 . . . . . . 7 ((𝜑𝐵 = 𝐶) → (𝑀 · 𝑋) = (-(2 · 𝐴) · 𝑋))
10292, 14mulneg1d 11739 . . . . . . 7 ((𝜑𝐵 = 𝐶) → (-(2 · 𝐴) · 𝑋) = -((2 · 𝐴) · 𝑋))
10391, 17, 14mulassd 11309 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝐴 · 𝑋)))
10417, 14mulcomd 11307 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → (𝐴 · 𝑋) = (𝑋 · 𝐴))
105104oveq2d 7461 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → (2 · (𝐴 · 𝑋)) = (2 · (𝑋 · 𝐴)))
106103, 105eqtrd 2774 . . . . . . . 8 ((𝜑𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝑋 · 𝐴)))
107106negeqd 11526 . . . . . . 7 ((𝜑𝐵 = 𝐶) → -((2 · 𝐴) · 𝑋) = -(2 · (𝑋 · 𝐴)))
108101, 102, 1073eqtrd 2778 . . . . . 6 ((𝜑𝐵 = 𝐶) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐴)))
109 constrrtcc.n . . . . . . 7 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
11017sqcld 14190 . . . . . . . 8 ((𝜑𝐵 = 𝐶) → (𝐴↑2) ∈ ℂ)
11154oveq1d 7460 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (𝑃 · 𝐷) = (0 · 𝐷))
11236mul02d 11484 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (0 · 𝐷) = 0)
113111, 112eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (𝑃 · 𝐷) = 0)
114113oveq2d 7461 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − 0))
11536, 17mulcld 11306 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (𝐷 · 𝐴) ∈ ℂ)
11664, 115mulcld 11306 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
117116subid1d 11632 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐴) · (𝐷 · 𝐴)))
118114, 117eqtrd 2774 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = ((∗‘𝐴) · (𝐷 · 𝐴)))
11943oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (𝑄 · 𝐴) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴))
120119oveq2d 7461 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴)))
121118, 120oveq12d 7463 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴))))
12260, 115mulcld 11306 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
12359, 17mulcld 11306 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴) ∈ ℂ)
124116, 122, 123subsubd 11671 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴)))
12568negeqd 11526 . . . . . . . . . . . . . . . . 17 (𝜑 → -(∗‘(𝐷𝐴)) = -((∗‘𝐷) − (∗‘𝐴)))
12673, 74negsubdi2d 11659 . . . . . . . . . . . . . . . . 17 (𝜑 → -((∗‘𝐷) − (∗‘𝐴)) = ((∗‘𝐴) − (∗‘𝐷)))
127125, 126eqtr2d 2775 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐴) − (∗‘𝐷)) = -(∗‘(𝐷𝐴)))
128127oveq1d 7460 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (-(∗‘(𝐷𝐴)) · (𝐷 · 𝐴)))
12935, 16mulcld 11306 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
13074, 73, 129subdird 11743 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
13170, 129mulcomd 11307 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘(𝐷𝐴)) · (𝐷 · 𝐴)) = ((𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
132131negeqd 11526 . . . . . . . . . . . . . . . 16 (𝜑 → -((∗‘(𝐷𝐴)) · (𝐷 · 𝐴)) = -((𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
13370, 129mulneg1d 11739 . . . . . . . . . . . . . . . 16 (𝜑 → (-(∗‘(𝐷𝐴)) · (𝐷 · 𝐴)) = -((∗‘(𝐷𝐴)) · (𝐷 · 𝐴)))
134129, 70mulneg1d 11739 . . . . . . . . . . . . . . . 16 (𝜑 → (-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))) = -((𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
135132, 133, 1343eqtr4d 2784 . . . . . . . . . . . . . . 15 (𝜑 → (-(∗‘(𝐷𝐴)) · (𝐷 · 𝐴)) = (-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
136128, 130, 1353eqtr3d 2782 . . . . . . . . . . . . . 14 (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
137136adantr 480 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
13857, 58, 17mul32d 11496 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴) = (((𝐷𝐴) · 𝐴) · (∗‘(𝐷𝐴))))
13936, 17, 17subdird 11743 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → ((𝐷𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
14017sqvald 14189 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵 = 𝐶) → (𝐴↑2) = (𝐴 · 𝐴))
141140oveq2d 7461 . . . . . . . . . . . . . . . 16 ((𝜑𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) = ((𝐷 · 𝐴) − (𝐴 · 𝐴)))
142139, 141eqtr4d 2777 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((𝐷𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴↑2)))
143142oveq1d 7460 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) · 𝐴) · (∗‘(𝐷𝐴))) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷𝐴))))
144138, 143eqtrd 2774 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷𝐴))))
145137, 144oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷𝐴)))))
146115negcld 11630 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → -(𝐷 · 𝐴) ∈ ℂ)
147115, 110subcld 11643 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) ∈ ℂ)
148146, 147, 58adddird 11311 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷𝐴)))))
149115subidd 11631 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
150149oveq1d 7460 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)) = (0 − (𝐴↑2)))
151146, 147addcomd 11488 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)))
152147, 115negsubd 11649 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)))
153115, 110, 115sub32d 11675 . . . . . . . . . . . . . . 15 ((𝜑𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
154151, 152, 1533eqtrd 2778 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)))
155 df-neg 11519 . . . . . . . . . . . . . . 15 -(𝐴↑2) = (0 − (𝐴↑2))
156155a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝐵 = 𝐶) → -(𝐴↑2) = (0 − (𝐴↑2)))
157150, 154, 1563eqtr4d 2784 . . . . . . . . . . . . 13 ((𝜑𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = -(𝐴↑2))
158157oveq1d 7460 . . . . . . . . . . . 12 ((𝜑𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷𝐴))) = (-(𝐴↑2) · (∗‘(𝐷𝐴))))
159145, 148, 1583eqtr2d 2780 . . . . . . . . . . 11 ((𝜑𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐴)) = (-(𝐴↑2) · (∗‘(𝐷𝐴))))
160121, 124, 1593eqtrd 2778 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐴↑2) · (∗‘(𝐷𝐴))))
16189eqcomd 2740 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷𝐴)))
162160, 161oveq12d 7463 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐴↑2) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))))
163110negcld 11630 . . . . . . . . . 10 ((𝜑𝐵 = 𝐶) → -(𝐴↑2) ∈ ℂ)
164163, 58, 98divcan4d 12072 . . . . . . . . 9 ((𝜑𝐵 = 𝐶) → ((-(𝐴↑2) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = -(𝐴↑2))
165162, 164eqtr2d 2775 . . . . . . . 8 ((𝜑𝐵 = 𝐶) → -(𝐴↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
166110, 165negcon1ad 11638 . . . . . . 7 ((𝜑𝐵 = 𝐶) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐴↑2))
167109, 166eqtrid 2786 . . . . . 6 ((𝜑𝐵 = 𝐶) → 𝑁 = (𝐴↑2))
168108, 167oveq12d 7463 . . . . 5 ((𝜑𝐵 = 𝐶) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐴)) + (𝐴↑2)))
169168oveq2d 7461 . . . 4 ((𝜑𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
17014sqcld 14190 . . . . 5 ((𝜑𝐵 = 𝐶) → (𝑋↑2) ∈ ℂ)
17114, 17mulcld 11306 . . . . . . 7 ((𝜑𝐵 = 𝐶) → (𝑋 · 𝐴) ∈ ℂ)
17291, 171mulcld 11306 . . . . . 6 ((𝜑𝐵 = 𝐶) → (2 · (𝑋 · 𝐴)) ∈ ℂ)
173172negcld 11630 . . . . 5 ((𝜑𝐵 = 𝐶) → -(2 · (𝑋 · 𝐴)) ∈ ℂ)
174170, 173, 110addassd 11308 . . . 4 ((𝜑𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2))))
175170, 172negsubd 11649 . . . . 5 ((𝜑𝐵 = 𝐶) → ((𝑋↑2) + -(2 · (𝑋 · 𝐴))) = ((𝑋↑2) − (2 · (𝑋 · 𝐴))))
176175oveq1d 7460 . . . 4 ((𝜑𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
177169, 174, 1763eqtr2d 2780 . . 3 ((𝜑𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
178 binom2sub 14265 . . . 4 ((𝑋 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑋𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
17914, 17, 178syl2anc 583 . . 3 ((𝜑𝐵 = 𝐶) → ((𝑋𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2)))
18029sq0id 14239 . . 3 ((𝜑𝐵 = 𝐶) → ((𝑋𝐴)↑2) = 0)
181177, 179, 1803eqtr2d 2780 . 2 ((𝜑𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
1821a1i 11 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
1836adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸 = 𝐹) → 𝐸 ∈ ℂ)
184 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸 = 𝐹) → 𝐸 = 𝐹)
185183, 184subeq0bd 11712 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (𝐸𝐹) = 0)
186185oveq1d 7460 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((𝐸𝐹) · (∗‘(𝐸𝐹))) = (0 · (∗‘(𝐸𝐹))))
1879cjcld 15241 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝐸𝐹)) ∈ ℂ)
188187adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (∗‘(𝐸𝐹)) ∈ ℂ)
189188mul02d 11484 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → (0 · (∗‘(𝐸𝐹))) = 0)
190186, 189eqtrd 2774 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((𝐸𝐹) · (∗‘(𝐸𝐹))) = 0)
1913, 190eqtrid 2786 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → 𝑄 = 0)
192191oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐷) · (𝐷 + 𝐴))))
19349adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (𝐵𝐶) ∈ ℂ)
194193absvalsqd 15487 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((abs‘(𝐵𝐶))↑2) = ((𝐵𝐶) · (∗‘(𝐵𝐶))))
19545, 194eqtr4id 2793 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → 𝑃 = ((abs‘(𝐵𝐶))↑2))
19620adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (abs‘(𝑋𝐴)) = (abs‘(𝐵𝐶)))
19713adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐸 = 𝐹) → 𝑋 ∈ ℂ)
19835adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐸 = 𝐹) → 𝐷 ∈ ℂ)
19913, 35subcld 11643 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝐷) ∈ ℂ)
200199adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐸 = 𝐹) → (𝑋𝐷) ∈ ℂ)
20132adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐸 = 𝐹) → (abs‘(𝑋𝐷)) = (abs‘(𝐸𝐹)))
202185abs00bd 15336 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐸 = 𝐹) → (abs‘(𝐸𝐹)) = 0)
203201, 202eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐸 = 𝐹) → (abs‘(𝑋𝐷)) = 0)
204200, 203abs00d 15491 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐸 = 𝐹) → (𝑋𝐷) = 0)
205197, 198, 204subeq0d 11651 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐸 = 𝐹) → 𝑋 = 𝐷)
206205fvoveq1d 7467 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (abs‘(𝑋𝐴)) = (abs‘(𝐷𝐴)))
207196, 206eqtr3d 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → (abs‘(𝐵𝐶)) = (abs‘(𝐷𝐴)))
208207oveq1d 7460 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((abs‘(𝐵𝐶))↑2) = ((abs‘(𝐷𝐴))↑2))
20941adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((abs‘(𝐷𝐴))↑2) = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
210195, 208, 2093eqtrd 2778 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → 𝑃 = ((𝐷𝐴) · (∗‘(𝐷𝐴))))
211210oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴))))
212192, 211oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
213 0cnd 11279 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → 0 ∈ ℂ)
214198cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (∗‘𝐷) ∈ ℂ)
21516adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → 𝐴 ∈ ℂ)
216198, 215addcld 11305 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (𝐷 + 𝐴) ∈ ℂ)
217214, 216mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
21840adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (𝐷𝐴) ∈ ℂ)
219218cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (∗‘(𝐷𝐴)) ∈ ℂ)
220218, 219mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → ((𝐷𝐴) · (∗‘(𝐷𝐴))) ∈ ℂ)
221215cjcld 15241 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (∗‘𝐴) ∈ ℂ)
222221, 216mulcld 11306 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
223213, 217, 220, 222sub4d 11692 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((𝐷𝐴) · (∗‘(𝐷𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))))
224218, 219mulneg1d 11739 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (-(𝐷𝐴) · (∗‘(𝐷𝐴))) = -((𝐷𝐴) · (∗‘(𝐷𝐴))))
225198, 215negsubdi2d 11659 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → -(𝐷𝐴) = (𝐴𝐷))
226225oveq1d 7460 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (-(𝐷𝐴) · (∗‘(𝐷𝐴))) = ((𝐴𝐷) · (∗‘(𝐷𝐴))))
227 df-neg 11519 . . . . . . . . . . . . . . 15 -((𝐷𝐴) · (∗‘(𝐷𝐴))) = (0 − ((𝐷𝐴) · (∗‘(𝐷𝐴))))
228227a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → -((𝐷𝐴) · (∗‘(𝐷𝐴))) = (0 − ((𝐷𝐴) · (∗‘(𝐷𝐴)))))
229224, 226, 2283eqtr3rd 2783 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (0 − ((𝐷𝐴) · (∗‘(𝐷𝐴)))) = ((𝐴𝐷) · (∗‘(𝐷𝐴))))
23076adantr 480 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷𝐴))))
231229, 230oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((0 − ((𝐷𝐴) · (∗‘(𝐷𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴𝐷) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
232212, 223, 2313eqtrd 2778 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴𝐷) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
233215, 198subcld 11643 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → (𝐴𝐷) ∈ ℂ)
234233, 216, 219subdird 11743 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → (((𝐴𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷𝐴))) = (((𝐴𝐷) · (∗‘(𝐷𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷𝐴)))))
235216, 233negsubdi2d 11659 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴𝐷)) = ((𝐴𝐷) − (𝐷 + 𝐴)))
2361982timesd 12532 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → (2 · 𝐷) = (𝐷 + 𝐷))
237215, 198, 198pnncand 11682 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴𝐷)) = (𝐷 + 𝐷))
238215, 198addcomd 11488 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → (𝐴 + 𝐷) = (𝐷 + 𝐴))
239238oveq1d 7460 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴𝐷)) = ((𝐷 + 𝐴) − (𝐴𝐷)))
240236, 237, 2393eqtr2rd 2781 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → ((𝐷 + 𝐴) − (𝐴𝐷)) = (2 · 𝐷))
241240negeqd 11526 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴𝐷)) = -(2 · 𝐷))
242235, 241eqtr3d 2776 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((𝐴𝐷) − (𝐷 + 𝐴)) = -(2 · 𝐷))
243242oveq1d 7460 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → (((𝐴𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷𝐴))) = (-(2 · 𝐷) · (∗‘(𝐷𝐴))))
244232, 234, 2433eqtr2rd 2781 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → (-(2 · 𝐷) · (∗‘(𝐷𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))))
24568adantr 480 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → (∗‘(𝐷𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
246244, 245oveq12d 7463 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))))
247 2cnd 12367 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → 2 ∈ ℂ)
248247, 198mulcld 11306 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → (2 · 𝐷) ∈ ℂ)
249248negcld 11630 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → -(2 · 𝐷) ∈ ℂ)
25097adantr 480 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → (∗‘(𝐷𝐴)) ≠ 0)
251249, 219, 250divcan4d 12072 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = -(2 · 𝐷))
252182, 246, 2513eqtr2d 2780 . . . . . . . 8 ((𝜑𝐸 = 𝐹) → 𝑀 = -(2 · 𝐷))
253252oveq1d 7460 . . . . . . 7 ((𝜑𝐸 = 𝐹) → (𝑀 · 𝑋) = (-(2 · 𝐷) · 𝑋))
254248, 197mulneg1d 11739 . . . . . . 7 ((𝜑𝐸 = 𝐹) → (-(2 · 𝐷) · 𝑋) = -((2 · 𝐷) · 𝑋))
255247, 198, 197mulassd 11309 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝐷 · 𝑋)))
256198, 197mulcomd 11307 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → (𝐷 · 𝑋) = (𝑋 · 𝐷))
257256oveq2d 7461 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → (2 · (𝐷 · 𝑋)) = (2 · (𝑋 · 𝐷)))
258255, 257eqtrd 2774 . . . . . . . 8 ((𝜑𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝑋 · 𝐷)))
259258negeqd 11526 . . . . . . 7 ((𝜑𝐸 = 𝐹) → -((2 · 𝐷) · 𝑋) = -(2 · (𝑋 · 𝐷)))
260253, 254, 2593eqtrd 2778 . . . . . 6 ((𝜑𝐸 = 𝐹) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐷)))
261198sqcld 14190 . . . . . . . 8 ((𝜑𝐸 = 𝐹) → (𝐷↑2) ∈ ℂ)
262210oveq1d 7460 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (𝑃 · 𝐷) = (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷))
263262oveq2d 7461 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)))
264191oveq1d 7460 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → (𝑄 · 𝐴) = (0 · 𝐴))
265215mul02d 11484 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → (0 · 𝐴) = 0)
266264, 265eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (𝑄 · 𝐴) = 0)
267266oveq2d 7461 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − 0))
268198, 215mulcld 11306 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → (𝐷 · 𝐴) ∈ ℂ)
269214, 268mulcld 11306 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
270269subid1d 11632 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐷) · (𝐷 · 𝐴)))
271267, 270eqtrd 2774 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = ((∗‘𝐷) · (𝐷 · 𝐴)))
272263, 271oveq12d 7463 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))))
273221, 268mulcld 11306 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
274220, 198mulcld 11306 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷) ∈ ℂ)
275273, 274, 269sub32d 11675 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)))
276136adantr 480 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))))
277218, 219, 198mul32d 11496 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷) = (((𝐷𝐴) · 𝐷) · (∗‘(𝐷𝐴))))
278198, 215, 198subdird 11743 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((𝐷𝐴) · 𝐷) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
279198sqvald 14189 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (𝐷↑2) = (𝐷 · 𝐷))
280198, 215mulcomd 11307 . . . . . . . . . . . . . . . . 17 ((𝜑𝐸 = 𝐹) → (𝐷 · 𝐴) = (𝐴 · 𝐷))
281279, 280oveq12d 7463 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) = ((𝐷 · 𝐷) − (𝐴 · 𝐷)))
282278, 281eqtr4d 2777 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → ((𝐷𝐴) · 𝐷) = ((𝐷↑2) − (𝐷 · 𝐴)))
283282oveq1d 7460 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (((𝐷𝐴) · 𝐷) · (∗‘(𝐷𝐴))) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷𝐴))))
284277, 283eqtrd 2774 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷𝐴))))
285276, 284oveq12d 7463 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷𝐴)))))
286268negcld 11630 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → -(𝐷 · 𝐴) ∈ ℂ)
287261, 268subcld 11643 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) ∈ ℂ)
288286, 287, 219subdird 11743 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷𝐴)))))
289286, 268addcomd 11488 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = ((𝐷 · 𝐴) + -(𝐷 · 𝐴)))
290268, 268negsubd 11649 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((𝐷 · 𝐴) + -(𝐷 · 𝐴)) = ((𝐷 · 𝐴) − (𝐷 · 𝐴)))
291268subidd 11631 . . . . . . . . . . . . . . . 16 ((𝜑𝐸 = 𝐹) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0)
292289, 290, 2913eqtrd 2778 . . . . . . . . . . . . . . 15 ((𝜑𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = 0)
293292oveq1d 7460 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)) = (0 − (𝐷↑2)))
294286, 261, 268subsub3d 11673 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)))
295 df-neg 11519 . . . . . . . . . . . . . . 15 -(𝐷↑2) = (0 − (𝐷↑2))
296295a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝐸 = 𝐹) → -(𝐷↑2) = (0 − (𝐷↑2)))
297293, 294, 2963eqtr4d 2784 . . . . . . . . . . . . 13 ((𝜑𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = -(𝐷↑2))
298297oveq1d 7460 . . . . . . . . . . . 12 ((𝜑𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷𝐴))) = (-(𝐷↑2) · (∗‘(𝐷𝐴))))
299285, 288, 2983eqtr2d 2780 . . . . . . . . . . 11 ((𝜑𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷𝐴) · (∗‘(𝐷𝐴))) · 𝐷)) = (-(𝐷↑2) · (∗‘(𝐷𝐴))))
300272, 275, 2993eqtrd 2778 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐷↑2) · (∗‘(𝐷𝐴))))
301245eqcomd 2740 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷𝐴)))
302300, 301oveq12d 7463 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐷↑2) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))))
303261negcld 11630 . . . . . . . . . 10 ((𝜑𝐸 = 𝐹) → -(𝐷↑2) ∈ ℂ)
304303, 219, 250divcan4d 12072 . . . . . . . . 9 ((𝜑𝐸 = 𝐹) → ((-(𝐷↑2) · (∗‘(𝐷𝐴))) / (∗‘(𝐷𝐴))) = -(𝐷↑2))
305302, 304eqtr2d 2775 . . . . . . . 8 ((𝜑𝐸 = 𝐹) → -(𝐷↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
306261, 305negcon1ad 11638 . . . . . . 7 ((𝜑𝐸 = 𝐹) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐷↑2))
307109, 306eqtrid 2786 . . . . . 6 ((𝜑𝐸 = 𝐹) → 𝑁 = (𝐷↑2))
308260, 307oveq12d 7463 . . . . 5 ((𝜑𝐸 = 𝐹) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐷)) + (𝐷↑2)))
309308oveq2d 7461 . . . 4 ((𝜑𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
310197sqcld 14190 . . . . 5 ((𝜑𝐸 = 𝐹) → (𝑋↑2) ∈ ℂ)
311197, 198mulcld 11306 . . . . . . 7 ((𝜑𝐸 = 𝐹) → (𝑋 · 𝐷) ∈ ℂ)
312247, 311mulcld 11306 . . . . . 6 ((𝜑𝐸 = 𝐹) → (2 · (𝑋 · 𝐷)) ∈ ℂ)
313312negcld 11630 . . . . 5 ((𝜑𝐸 = 𝐹) → -(2 · (𝑋 · 𝐷)) ∈ ℂ)
314310, 313, 261addassd 11308 . . . 4 ((𝜑𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2))))
315310, 312negsubd 11649 . . . . 5 ((𝜑𝐸 = 𝐹) → ((𝑋↑2) + -(2 · (𝑋 · 𝐷))) = ((𝑋↑2) − (2 · (𝑋 · 𝐷))))
316315oveq1d 7460 . . . 4 ((𝜑𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
317309, 314, 3163eqtr2d 2780 . . 3 ((𝜑𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
318 binom2sub 14265 . . . 4 ((𝑋 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝑋𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
319197, 198, 318syl2anc 583 . . 3 ((𝜑𝐸 = 𝐹) → ((𝑋𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2)))
320204sq0id 14239 . . 3 ((𝜑𝐸 = 𝐹) → ((𝑋𝐷)↑2) = 0)
321317, 319, 3203eqtr2d 2780 . 2 ((𝜑𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
3224adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝑆 ⊆ ℂ)
32315adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐴𝑆)
32422adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐵𝑆)
32547adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐶𝑆)
32634adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐷𝑆)
3275adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐸𝑆)
3287adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐹𝑆)
32913adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝑋 ∈ ℂ)
33094adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐴𝐷)
33120adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → (abs‘(𝑋𝐴)) = (abs‘(𝐵𝐶)))
33232adantr 480 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → (abs‘(𝑋𝐷)) = (abs‘(𝐸𝐹)))
333 simprl 770 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐵𝐶)
334 simprr 772 . . 3 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → 𝐸𝐹)
335322, 323, 324, 325, 326, 327, 328, 329, 330, 331, 332, 45, 3, 1, 109, 333, 334constrrtcclem 33717 . 2 ((𝜑 ∧ (𝐵𝐶𝐸𝐹)) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
336181, 321, 335pm2.61da2ne 3032 1 (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2103  wne 2942  wss 3970  cfv 6572  (class class class)co 7445  cc 11178  0cc0 11180   + caddc 11183   · cmul 11185  cmin 11516  -cneg 11517   / cdiv 11943  2c2 12344  cexp 14108  ccj 15141  abscabs 15279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766  ax-cnex 11236  ax-resscn 11237  ax-1cn 11238  ax-icn 11239  ax-addcl 11240  ax-addrcl 11241  ax-mulcl 11242  ax-mulrcl 11243  ax-mulcom 11244  ax-addass 11245  ax-mulass 11246  ax-distr 11247  ax-i2m1 11248  ax-1ne0 11249  ax-1rid 11250  ax-rnegex 11251  ax-rrecex 11252  ax-cnre 11253  ax-pre-lttri 11254  ax-pre-lttrn 11255  ax-pre-ltadd 11256  ax-pre-mulgt0 11257  ax-pre-sup 11258
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-pred 6331  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-riota 7401  df-ov 7448  df-oprab 7449  df-mpo 7450  df-om 7900  df-2nd 8027  df-frecs 8318  df-wrecs 8349  df-recs 8423  df-rdg 8462  df-er 8759  df-en 9000  df-dom 9001  df-sdom 9002  df-sup 9507  df-pnf 11322  df-mnf 11323  df-xr 11324  df-ltxr 11325  df-le 11326  df-sub 11518  df-neg 11519  df-div 11944  df-nn 12290  df-2 12352  df-3 12353  df-n0 12550  df-z 12636  df-uz 12900  df-rp 13054  df-seq 14049  df-exp 14109  df-cj 15144  df-re 15145  df-im 15146  df-sqrt 15280  df-abs 15281
This theorem is referenced by:  constrfin  33728  constrelextdg2  33729
  Copyright terms: Public domain W3C validator