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

Theorem constrrtcclem 33717
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.)
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 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
constrrtcclem.1 (𝜑𝐵𝐶)
constrrtcclem.2 (𝜑𝐸𝐹)
Assertion
Ref Expression
constrrtcclem (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Proof of Theorem constrrtcclem
StepHypRef Expression
1 constrrtcc.x . . . 4 (𝜑𝑋 ∈ ℂ)
21sqcld 14190 . . 3 (𝜑 → (𝑋↑2) ∈ ℂ)
3 constrrtcc.m . . . . 5 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
4 constrrtcc.5 . . . . . . . . 9 𝑄 = ((𝐸𝐹) · (∗‘(𝐸𝐹)))
5 constrrtcc.s . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℂ)
6 constrrtcc.e . . . . . . . . . . . 12 (𝜑𝐸𝑆)
75, 6sseldd 4003 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℂ)
8 constrrtcc.f . . . . . . . . . . . 12 (𝜑𝐹𝑆)
95, 8sseldd 4003 . . . . . . . . . . 11 (𝜑𝐹 ∈ ℂ)
107, 9subcld 11643 . . . . . . . . . 10 (𝜑 → (𝐸𝐹) ∈ ℂ)
1110cjcld 15241 . . . . . . . . . 10 (𝜑 → (∗‘(𝐸𝐹)) ∈ ℂ)
1210, 11mulcld 11306 . . . . . . . . 9 (𝜑 → ((𝐸𝐹) · (∗‘(𝐸𝐹))) ∈ ℂ)
134, 12eqeltrid 2842 . . . . . . . 8 (𝜑𝑄 ∈ ℂ)
14 constrrtcc.d . . . . . . . . . . 11 (𝜑𝐷𝑆)
155, 14sseldd 4003 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
1615cjcld 15241 . . . . . . . . 9 (𝜑 → (∗‘𝐷) ∈ ℂ)
17 constrrtcc.a . . . . . . . . . . 11 (𝜑𝐴𝑆)
185, 17sseldd 4003 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
1915, 18addcld 11305 . . . . . . . . 9 (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
2016, 19mulcld 11306 . . . . . . . 8 (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
2113, 20subcld 11643 . . . . . . 7 (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ)
22 constrrtcc.4 . . . . . . . . 9 𝑃 = ((𝐵𝐶) · (∗‘(𝐵𝐶)))
23 constrrtcc.b . . . . . . . . . . . 12 (𝜑𝐵𝑆)
245, 23sseldd 4003 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
25 constrrtcc.c . . . . . . . . . . . 12 (𝜑𝐶𝑆)
265, 25sseldd 4003 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℂ)
2724, 26subcld 11643 . . . . . . . . . 10 (𝜑 → (𝐵𝐶) ∈ ℂ)
2827cjcld 15241 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵𝐶)) ∈ ℂ)
2927, 28mulcld 11306 . . . . . . . . 9 (𝜑 → ((𝐵𝐶) · (∗‘(𝐵𝐶))) ∈ ℂ)
3022, 29eqeltrid 2842 . . . . . . . 8 (𝜑𝑃 ∈ ℂ)
3118cjcld 15241 . . . . . . . . 9 (𝜑 → (∗‘𝐴) ∈ ℂ)
3231, 19mulcld 11306 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
3330, 32subcld 11643 . . . . . . 7 (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ)
3421, 33subcld 11643 . . . . . 6 (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ)
3516, 31subcld 11643 . . . . . 6 (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈ ℂ)
3615, 18cjsubd 32747 . . . . . . 7 (𝜑 → (∗‘(𝐷𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
3715, 18subcld 11643 . . . . . . . 8 (𝜑 → (𝐷𝐴) ∈ ℂ)
38 constrrtcc.1 . . . . . . . . . 10 (𝜑𝐴𝐷)
3938necomd 2998 . . . . . . . . 9 (𝜑𝐷𝐴)
4015, 18, 39subne0d 11652 . . . . . . . 8 (𝜑 → (𝐷𝐴) ≠ 0)
4137, 40cjne0d 15248 . . . . . . 7 (𝜑 → (∗‘(𝐷𝐴)) ≠ 0)
4236, 41eqnetrrd 3011 . . . . . 6 (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0)
4334, 35, 42divcld 12066 . . . . 5 (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
443, 43eqeltrid 2842 . . . 4 (𝜑𝑀 ∈ ℂ)
4544, 1mulcld 11306 . . 3 (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
46 constrrtcc.n . . . 4 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
4715, 18mulcld 11306 . . . . . . . . 9 (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
4831, 47mulcld 11306 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
4930, 15mulcld 11306 . . . . . . . 8 (𝜑 → (𝑃 · 𝐷) ∈ ℂ)
5048, 49subcld 11643 . . . . . . 7 (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ)
5116, 47mulcld 11306 . . . . . . . 8 (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
5213, 18mulcld 11306 . . . . . . . 8 (𝜑 → (𝑄 · 𝐴) ∈ ℂ)
5351, 52subcld 11643 . . . . . . 7 (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ)
5450, 53subcld 11643 . . . . . 6 (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ)
5554, 35, 42divcld 12066 . . . . 5 (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
5655negcld 11630 . . . 4 (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
5746, 56eqeltrid 2842 . . 3 (𝜑𝑁 ∈ ℂ)
582, 45, 57addassd 11308 . 2 (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)))
5935, 2mulcld 11306 . . . . . . 7 (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ)
6034, 1mulcld 11306 . . . . . . 7 (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ)
6116, 31, 2subdird 11743 . . . . . . . . 9 (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))))
6221, 33, 1subdird 11743 . . . . . . . . 9 (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
6361, 62oveq12d 7463 . . . . . . . 8 (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
6416, 2mulcld 11306 . . . . . . . . 9 (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ)
6521, 1mulcld 11306 . . . . . . . . 9 (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
6631, 2mulcld 11306 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ)
6733, 1mulcld 11306 . . . . . . . . 9 (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
6864, 65, 66, 67addsub4d 11690 . . . . . . . 8 (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
691, 18subcld 11643 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐴) ∈ ℂ)
701, 15subcld 11643 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐷) ∈ ℂ)
7169, 70mulcomd 11307 . . . . . . . . . . 11 (𝜑 → ((𝑋𝐴) · (𝑋𝐷)) = ((𝑋𝐷) · (𝑋𝐴)))
7271oveq2d 7461 . . . . . . . . . 10 (𝜑 → ((∗‘𝑋) · ((𝑋𝐴) · (𝑋𝐷))) = ((∗‘𝑋) · ((𝑋𝐷) · (𝑋𝐴))))
7369cjcld 15241 . . . . . . . . . . . . . . . . 17 (𝜑 → (∗‘(𝑋𝐴)) ∈ ℂ)
74 constrrtcc.2 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋𝐴)) = (abs‘(𝐵𝐶)))
75 constrrtcclem.1 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝐶)
7624, 26, 75subne0d 11652 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐶) ≠ 0)
7727, 76absne0d 15492 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝐵𝐶)) ≠ 0)
7874, 77eqnetrd 3010 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘(𝑋𝐴)) ≠ 0)
7969abs00ad 15335 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐴)) = 0 ↔ (𝑋𝐴) = 0))
8079necon3bid 2987 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝑋𝐴)) ≠ 0 ↔ (𝑋𝐴) ≠ 0))
8178, 80mpbid 232 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋𝐴) ≠ 0)
8274oveq1d 7460 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐴))↑2) = ((abs‘(𝐵𝐶))↑2))
8369absvalsqd 15487 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐴))↑2) = ((𝑋𝐴) · (∗‘(𝑋𝐴))))
8427absvalsqd 15487 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝐵𝐶))↑2) = ((𝐵𝐶) · (∗‘(𝐵𝐶))))
8582, 83, 843eqtr3d 2782 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑋𝐴) · (∗‘(𝑋𝐴))) = ((𝐵𝐶) · (∗‘(𝐵𝐶))))
8685, 22eqtr4di 2792 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋𝐴) · (∗‘(𝑋𝐴))) = 𝑃)
8769, 73, 81, 86mvllmuld 12122 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝑋𝐴)) = (𝑃 / (𝑋𝐴)))
8887, 73eqeltrrd 2839 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 / (𝑋𝐴)) ∈ ℂ)
8931, 88addcld 11305 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋𝐴))) ∈ ℂ)
9089, 69, 70mulassd 11309 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · (𝑋𝐴)) · (𝑋𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · ((𝑋𝐴) · (𝑋𝐷))))
9130, 69, 81divcan1d 12067 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑃 / (𝑋𝐴)) · (𝑋𝐴)) = 𝑃)
9291oveq2d 7461 . . . . . . . . . . . . . . . 16 (𝜑 → (((∗‘𝐴) · (𝑋𝐴)) + ((𝑃 / (𝑋𝐴)) · (𝑋𝐴))) = (((∗‘𝐴) · (𝑋𝐴)) + 𝑃))
9331, 69, 88, 92joinlmuladdmuld 11313 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · (𝑋𝐴)) = (((∗‘𝐴) · (𝑋𝐴)) + 𝑃))
9493oveq1d 7460 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · (𝑋𝐴)) · (𝑋𝐷)) = ((((∗‘𝐴) · (𝑋𝐴)) + 𝑃) · (𝑋𝐷)))
9531, 69mulcld 11306 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐴) · (𝑋𝐴)) ∈ ℂ)
9695, 30, 70adddird 11311 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐴) · (𝑋𝐴)) + 𝑃) · (𝑋𝐷)) = ((((∗‘𝐴) · (𝑋𝐴)) · (𝑋𝐷)) + (𝑃 · (𝑋𝐷))))
9731, 69, 70mulassd 11309 . . . . . . . . . . . . . . . 16 (𝜑 → (((∗‘𝐴) · (𝑋𝐴)) · (𝑋𝐷)) = ((∗‘𝐴) · ((𝑋𝐴) · (𝑋𝐷))))
981, 18, 1, 15mulsubd 11745 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑋𝐴) · (𝑋𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
991sqvald 14189 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
10099oveq1d 7460 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴)))
1011, 15, 18adddid 11310 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴)))
102100, 101oveq12d 7463 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
1031, 19mulcld 11306 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ)
1042, 47, 103addsubd 11664 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
10598, 102, 1043eqtr2d 2780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋𝐴) · (𝑋𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
106105oveq2d 7461 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐴) · ((𝑋𝐴) · (𝑋𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
1072, 103subcld 11643 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ)
10831, 107, 47adddid 11310 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
10997, 106, 1083eqtrd 2778 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐴) · (𝑋𝐴)) · (𝑋𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
11030, 1, 15subdid 11742 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 · (𝑋𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷)))
111109, 110oveq12d 7463 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐴) · (𝑋𝐴)) · (𝑋𝐷)) + (𝑃 · (𝑋𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
11294, 96, 1113eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · (𝑋𝐴)) · (𝑋𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
1131, 18cjsubd 32747 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝑋𝐴)) = ((∗‘𝑋) − (∗‘𝐴)))
114113, 87eqtr3d 2776 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋𝐴)))
1151cjcld 15241 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘𝑋) ∈ ℂ)
116115, 31, 88subaddd 11661 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋𝐴))) = (∗‘𝑋)))
117114, 116mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋𝐴))) = (∗‘𝑋))
118117oveq1d 7460 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋𝐴))) · ((𝑋𝐴) · (𝑋𝐷))) = ((∗‘𝑋) · ((𝑋𝐴) · (𝑋𝐷))))
11990, 112, 1183eqtr3rd 2783 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝑋) · ((𝑋𝐴) · (𝑋𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
12031, 107mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
121120, 48addcld 11305 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ)
12230, 1mulcld 11306 . . . . . . . . . . . . 13 (𝜑 → (𝑃 · 𝑋) ∈ ℂ)
123121, 122, 49addsubassd 11663 . . . . . . . . . . . 12 (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
124120, 48, 122add32d 11513 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))))
125124oveq1d 7460 . . . . . . . . . . . 12 (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
126119, 123, 1253eqtr2d 2780 . . . . . . . . . . 11 (𝜑 → ((∗‘𝑋) · ((𝑋𝐴) · (𝑋𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
127120, 122addcld 11305 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ)
128127, 48, 49addsubassd 11663 . . . . . . . . . . 11 (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
12932, 1mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
13066, 129, 122subadd23d 11665 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
13131, 2, 103subdid 11742 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))))
13231, 1, 19mul12d 11495 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))))
1331, 32mulcomd 11307 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
134132, 133eqtrd 2774 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
135134oveq2d 7461 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
136131, 135eqtrd 2774 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
137136oveq1d 7460 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)))
13830, 32, 1subdird 11743 . . . . . . . . . . . . . 14 (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
139138oveq2d 7461 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
140130, 137, 1393eqtr4d 2784 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
141140oveq1d 7460 . . . . . . . . . . 11 (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
142126, 128, 1413eqtrd 2778 . . . . . . . . . 10 (𝜑 → ((∗‘𝑋) · ((𝑋𝐴) · (𝑋𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
14370cjcld 15241 . . . . . . . . . . . . . . . . 17 (𝜑 → (∗‘(𝑋𝐷)) ∈ ℂ)
144 constrrtcc.3 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋𝐷)) = (abs‘(𝐸𝐹)))
145 constrrtcclem.2 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸𝐹)
1467, 9, 145subne0d 11652 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝐹) ≠ 0)
14710, 146absne0d 15492 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝐸𝐹)) ≠ 0)
148144, 147eqnetrd 3010 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘(𝑋𝐷)) ≠ 0)
14970abs00ad 15335 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐷)) = 0 ↔ (𝑋𝐷) = 0))
150149necon3bid 2987 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝑋𝐷)) ≠ 0 ↔ (𝑋𝐷) ≠ 0))
151148, 150mpbid 232 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋𝐷) ≠ 0)
152144oveq1d 7460 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐷))↑2) = ((abs‘(𝐸𝐹))↑2))
15370absvalsqd 15487 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝑋𝐷))↑2) = ((𝑋𝐷) · (∗‘(𝑋𝐷))))
15410absvalsqd 15487 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘(𝐸𝐹))↑2) = ((𝐸𝐹) · (∗‘(𝐸𝐹))))
155152, 153, 1543eqtr3d 2782 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑋𝐷) · (∗‘(𝑋𝐷))) = ((𝐸𝐹) · (∗‘(𝐸𝐹))))
156155, 4eqtr4di 2792 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋𝐷) · (∗‘(𝑋𝐷))) = 𝑄)
15770, 143, 151, 156mvllmuld 12122 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝑋𝐷)) = (𝑄 / (𝑋𝐷)))
158157, 143eqeltrrd 2839 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 / (𝑋𝐷)) ∈ ℂ)
15916, 158addcld 11305 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋𝐷))) ∈ ℂ)
160159, 70, 69mulassd 11309 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · (𝑋𝐷)) · (𝑋𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · ((𝑋𝐷) · (𝑋𝐴))))
16113, 70, 151divcan1d 12067 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄 / (𝑋𝐷)) · (𝑋𝐷)) = 𝑄)
162161oveq2d 7461 . . . . . . . . . . . . . . . 16 (𝜑 → (((∗‘𝐷) · (𝑋𝐷)) + ((𝑄 / (𝑋𝐷)) · (𝑋𝐷))) = (((∗‘𝐷) · (𝑋𝐷)) + 𝑄))
16316, 70, 158, 162joinlmuladdmuld 11313 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · (𝑋𝐷)) = (((∗‘𝐷) · (𝑋𝐷)) + 𝑄))
164163oveq1d 7460 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · (𝑋𝐷)) · (𝑋𝐴)) = ((((∗‘𝐷) · (𝑋𝐷)) + 𝑄) · (𝑋𝐴)))
16516, 70mulcld 11306 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐷) · (𝑋𝐷)) ∈ ℂ)
166165, 13, 69adddird 11311 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐷) · (𝑋𝐷)) + 𝑄) · (𝑋𝐴)) = ((((∗‘𝐷) · (𝑋𝐷)) · (𝑋𝐴)) + (𝑄 · (𝑋𝐴))))
16716, 70, 69mulassd 11309 . . . . . . . . . . . . . . . . 17 (𝜑 → (((∗‘𝐷) · (𝑋𝐷)) · (𝑋𝐴)) = ((∗‘𝐷) · ((𝑋𝐷) · (𝑋𝐴))))
16871oveq2d 7461 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘𝐷) · ((𝑋𝐴) · (𝑋𝐷))) = ((∗‘𝐷) · ((𝑋𝐷) · (𝑋𝐴))))
169167, 168eqtr4d 2777 . . . . . . . . . . . . . . . 16 (𝜑 → (((∗‘𝐷) · (𝑋𝐷)) · (𝑋𝐴)) = ((∗‘𝐷) · ((𝑋𝐴) · (𝑋𝐷))))
170105oveq2d 7461 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐷) · ((𝑋𝐴) · (𝑋𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
17116, 107, 47adddid 11310 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
172169, 170, 1713eqtrd 2778 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐷) · (𝑋𝐷)) · (𝑋𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
17313, 1, 18subdid 11742 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 · (𝑋𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴)))
174172, 173oveq12d 7463 . . . . . . . . . . . . . 14 (𝜑 → ((((∗‘𝐷) · (𝑋𝐷)) · (𝑋𝐴)) + (𝑄 · (𝑋𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
175164, 166, 1743eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · (𝑋𝐷)) · (𝑋𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
1761, 15cjsubd 32747 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝑋𝐷)) = ((∗‘𝑋) − (∗‘𝐷)))
177176, 157eqtr3d 2776 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋𝐷)))
178115, 16, 158subaddd 11661 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋𝐷))) = (∗‘𝑋)))
179177, 178mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋𝐷))) = (∗‘𝑋))
180179oveq1d 7460 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋𝐷))) · ((𝑋𝐷) · (𝑋𝐴))) = ((∗‘𝑋) · ((𝑋𝐷) · (𝑋𝐴))))
181160, 175, 1803eqtr3rd 2783 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝑋) · ((𝑋𝐷) · (𝑋𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
18216, 107mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
183182, 51addcld 11305 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ)
18413, 1mulcld 11306 . . . . . . . . . . . . 13 (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
185183, 184, 52addsubassd 11663 . . . . . . . . . . . 12 (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
186182, 51, 184add32d 11513 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))))
187186oveq1d 7460 . . . . . . . . . . . 12 (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
188181, 185, 1873eqtr2d 2780 . . . . . . . . . . 11 (𝜑 → ((∗‘𝑋) · ((𝑋𝐷) · (𝑋𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
189182, 184addcld 11305 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ)
190189, 51, 52addsubassd 11663 . . . . . . . . . . 11 (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
19120, 1mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
19264, 191, 184subadd23d 11665 . . . . . . . . . . . . 13 (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
19316, 2, 103subdid 11742 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))))
19416, 1, 19mul12d 11495 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))))
1951, 20mulcomd 11307 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
196194, 195eqtrd 2774 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
197196oveq2d 7461 . . . . . . . . . . . . . . 15 (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
198193, 197eqtrd 2774 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
199198oveq1d 7460 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)))
20013, 20, 1subdird 11743 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
201200oveq2d 7461 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
202192, 199, 2013eqtr4d 2784 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)))
203202oveq1d 7460 . . . . . . . . . . 11 (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
204188, 190, 2033eqtrd 2778 . . . . . . . . . 10 (𝜑 → ((∗‘𝑋) · ((𝑋𝐷) · (𝑋𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
20572, 142, 2043eqtr3d 2782 . . . . . . . . 9 (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
206140, 127eqeltrrd 2839 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
207202, 189eqeltrrd 2839 . . . . . . . . . 10 (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
208206, 50, 207, 53addsubeq4d 11694 . . . . . . . . 9 (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))))
209205, 208mpbid 232 . . . . . . . 8 (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
21063, 68, 2093eqtr2d 2780 . . . . . . 7 (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
21159, 60, 210mvlraddd 11696 . . . . . 6 (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)))
21235, 2, 42, 211mvllmuld 12122 . . . . 5 (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))))
21354, 60, 35, 42divsubdird 12105 . . . . . 6 (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
21446eqcomi 2743 . . . . . . . . 9 -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁
215214a1i 11 . . . . . . . 8 (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁)
21655, 215negcon1ad 11638 . . . . . . 7 (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
217216oveq1d 7460 . . . . . 6 (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
218213, 217eqtr4d 2777 . . . . 5 (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
21934, 1, 35, 42div23d 12103 . . . . . . 7 (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋))
2203oveq1i 7455 . . . . . . 7 (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)
221219, 220eqtr4di 2792 . . . . . 6 (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋))
222221oveq2d 7461 . . . . 5 (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋)))
223212, 218, 2223eqtrd 2778 . . . 4 (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))
224216, 55eqeltrd 2838 . . . . 5 (𝜑 → -𝑁 ∈ ℂ)
2252, 45, 224addlsub 11702 . . . 4 (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))))
226223, 225mpbird 257 . . 3 (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)
2272, 45addcld 11305 . . . 4 (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ)
228 addeq0 11709 . . . 4 ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
229227, 57, 228syl2anc 583 . . 3 (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
230226, 229mpbird 257 . 2 (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0)
23158, 230eqtr3d 2776 1 (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = 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:  constrrtcc  33718
  Copyright terms: Public domain W3C validator