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

Theorem constrrtlc1 33737
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.)
Hypotheses
Ref Expression
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
Ref Expression
constrrtlc1 (𝜑 → (((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0 ∧ 𝑄 ≠ 0))

Proof of Theorem constrrtlc1
StepHypRef Expression
1 constrrtlc.s . . . . . . . . . . . . . 14 (𝜑𝑆 ⊆ ℂ)
2 constrrtlc.a . . . . . . . . . . . . . 14 (𝜑𝐴𝑆)
31, 2sseldd 3995 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℂ)
43cjcld 15231 . . . . . . . . . . . 12 (𝜑 → (∗‘𝐴) ∈ ℂ)
5 constrrtlc.q . . . . . . . . . . . . . 14 𝑄 = (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴))
6 constrrtlc.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑆)
71, 6sseldd 3995 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℂ)
87cjcld 15231 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘𝐵) ∈ ℂ)
98, 4subcld 11617 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐵) − (∗‘𝐴)) ∈ ℂ)
107, 3subcld 11617 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝐴) ∈ ℂ)
11 constrrtlc1.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐴𝐵)
1211necomd 2993 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐴)
137, 3, 12subne0d 11626 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝐴) ≠ 0)
149, 10, 13divcld 12040 . . . . . . . . . . . . . 14 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴)) ∈ ℂ)
155, 14eqeltrid 2842 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℂ)
163, 15mulcld 11278 . . . . . . . . . . . 12 (𝜑 → (𝐴 · 𝑄) ∈ ℂ)
174, 16subcld 11617 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) − (𝐴 · 𝑄)) ∈ ℂ)
18 constrrtlc.c . . . . . . . . . . . . 13 (𝜑𝐶𝑆)
191, 18sseldd 3995 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
2019cjcld 15231 . . . . . . . . . . 11 (𝜑 → (∗‘𝐶) ∈ ℂ)
2117, 20subcld 11617 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) ∈ ℂ)
2219, 15mulcld 11278 . . . . . . . . . 10 (𝜑 → (𝐶 · 𝑄) ∈ ℂ)
2321, 22subcld 11617 . . . . . . . . 9 (𝜑 → ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) ∈ ℂ)
247, 3cjsubd 32758 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐴)) = ((∗‘𝐵) − (∗‘𝐴)))
2510, 13cjne0d 15238 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐴)) ≠ 0)
2624, 25eqnetrrd 3006 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) − (∗‘𝐴)) ≠ 0)
279, 10, 26, 13divne0d 12056 . . . . . . . . . 10 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴)) ≠ 0)
285neeq1i 3002 . . . . . . . . . 10 (𝑄 ≠ 0 ↔ (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴)) ≠ 0)
2927, 28sylibr 234 . . . . . . . . 9 (𝜑𝑄 ≠ 0)
3023, 15, 29divcld 12040 . . . . . . . 8 (𝜑 → (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄) ∈ ℂ)
31 constrrtlc.1 . . . . . . . . 9 (𝜑𝑋 = (𝐴 + (𝑇 · (𝐵𝐴))))
32 constrrtlc.t . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
3332recnd 11286 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
3433, 10mulcld 11278 . . . . . . . . . 10 (𝜑 → (𝑇 · (𝐵𝐴)) ∈ ℂ)
353, 34addcld 11277 . . . . . . . . 9 (𝜑 → (𝐴 + (𝑇 · (𝐵𝐴))) ∈ ℂ)
3631, 35eqeltrd 2838 . . . . . . . 8 (𝜑𝑋 ∈ ℂ)
3730, 36mulcomd 11279 . . . . . . 7 (𝜑 → ((((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄) · 𝑋) = (𝑋 · (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄)))
38 constrrtlc.m . . . . . . . . 9 𝑀 = (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄)
3938a1i 11 . . . . . . . 8 (𝜑𝑀 = (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄))
4039oveq1d 7445 . . . . . . 7 (𝜑 → (𝑀 · 𝑋) = ((((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄) · 𝑋))
4136, 23, 15, 29divassd 12075 . . . . . . 7 (𝜑 → ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) / 𝑄) = (𝑋 · (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄)))
4237, 40, 413eqtr4d 2784 . . . . . 6 (𝜑 → (𝑀 · 𝑋) = ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) / 𝑄))
43 constrrtlc.n . . . . . . 7 𝑁 = (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄)
4443a1i 11 . . . . . 6 (𝜑𝑁 = (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄))
4542, 44oveq12d 7448 . . . . 5 (𝜑 → ((𝑀 · 𝑋) + 𝑁) = (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) / 𝑄) + (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄)))
4636, 23mulcld 11278 . . . . . 6 (𝜑 → (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) ∈ ℂ)
4719, 21mulcld 11278 . . . . . . . 8 (𝜑 → (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) ∈ ℂ)
4836sqvald 14179 . . . . . . . . . . . . . 14 (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
4948oveq1d 7445 . . . . . . . . . . . . 13 (𝜑 → ((𝑋↑2) · 𝑄) = ((𝑋 · 𝑋) · 𝑄))
5036, 36, 15mulassd 11281 . . . . . . . . . . . . 13 (𝜑 → ((𝑋 · 𝑋) · 𝑄) = (𝑋 · (𝑋 · 𝑄)))
5149, 50eqtrd 2774 . . . . . . . . . . . 12 (𝜑 → ((𝑋↑2) · 𝑄) = (𝑋 · (𝑋 · 𝑄)))
5236, 15mulcld 11278 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · 𝑄) ∈ ℂ)
5336, 52mulcld 11278 . . . . . . . . . . . 12 (𝜑 → (𝑋 · (𝑋 · 𝑄)) ∈ ℂ)
5451, 53eqeltrd 2838 . . . . . . . . . . 11 (𝜑 → ((𝑋↑2) · 𝑄) ∈ ℂ)
5554, 46, 47addsubd 11638 . . . . . . . . . 10 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((((𝑋↑2) · 𝑄) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))))
5651oveq1d 7445 . . . . . . . . . . . 12 (𝜑 → (((𝑋↑2) · 𝑄) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((𝑋 · (𝑋 · 𝑄)) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))))
5736, 21, 22subdid 11716 . . . . . . . . . . . 12 (𝜑 → (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) = ((𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) − (𝑋 · (𝐶 · 𝑄))))
5856, 57oveq12d 7448 . . . . . . . . . . 11 (𝜑 → ((((𝑋↑2) · 𝑄) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) = (((𝑋 · (𝑋 · 𝑄)) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) + ((𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) − (𝑋 · (𝐶 · 𝑄)))))
5936, 21mulcld 11278 . . . . . . . . . . . 12 (𝜑 → (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) ∈ ℂ)
6036, 22mulcld 11278 . . . . . . . . . . . 12 (𝜑 → (𝑋 · (𝐶 · 𝑄)) ∈ ℂ)
6153, 59, 47, 60addsub4d 11664 . . . . . . . . . . 11 (𝜑 → (((𝑋 · (𝑋 · 𝑄)) + (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + (𝑋 · (𝐶 · 𝑄)))) = (((𝑋 · (𝑋 · 𝑄)) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) + ((𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) − (𝑋 · (𝐶 · 𝑄)))))
6236, 19, 52, 21submuladdd 32756 . . . . . . . . . . . 12 (𝜑 → ((𝑋𝐶) · ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = (((𝑋 · (𝑋 · 𝑄)) + (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐶 · (𝑋 · 𝑄)) + (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))))))
63 constrrtlc.2 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝑋𝐶)) = (abs‘(𝐸𝐹)))
6463oveq1d 7445 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝑋𝐶))↑2) = ((abs‘(𝐸𝐹))↑2))
6536, 19subcld 11617 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋𝐶) ∈ ℂ)
6665absvalsqd 15477 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝑋𝐶))↑2) = ((𝑋𝐶) · (∗‘(𝑋𝐶))))
67 constrrtlc.e . . . . . . . . . . . . . . . . 17 (𝜑𝐸𝑆)
681, 67sseldd 3995 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ ℂ)
69 constrrtlc.f . . . . . . . . . . . . . . . . 17 (𝜑𝐹𝑆)
701, 69sseldd 3995 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ ℂ)
7168, 70subcld 11617 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝐹) ∈ ℂ)
7271absvalsqd 15477 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐸𝐹))↑2) = ((𝐸𝐹) · (∗‘(𝐸𝐹))))
7364, 66, 723eqtr3d 2782 . . . . . . . . . . . . 13 (𝜑 → ((𝑋𝐶) · (∗‘(𝑋𝐶))) = ((𝐸𝐹) · (∗‘(𝐸𝐹))))
7431fvoveq1d 7452 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝑋𝐶)) = (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)))
7535, 19cjsubd 32758 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)))
763, 34cjaddd 15255 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))))
7733, 10cjmuld 15256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = ((∗‘𝑇) · (∗‘(𝐵𝐴))))
7832cjred 15261 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (∗‘𝑇) = 𝑇)
793, 34, 31mvrladdd 11673 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋𝐴) = (𝑇 · (𝐵𝐴)))
8079, 34eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑋𝐴) ∈ ℂ)
8180, 33, 10, 13divmul3d 12074 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑋𝐴) / (𝐵𝐴)) = 𝑇 ↔ (𝑋𝐴) = (𝑇 · (𝐵𝐴))))
8279, 81mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐴) / (𝐵𝐴)) = 𝑇)
8378, 82eqtr4d 2777 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (∗‘𝑇) = ((𝑋𝐴) / (𝐵𝐴)))
8483, 24oveq12d 7448 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((∗‘𝑇) · (∗‘(𝐵𝐴))) = (((𝑋𝐴) / (𝐵𝐴)) · ((∗‘𝐵) − (∗‘𝐴))))
8580, 10, 9, 13div32d 12063 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑋𝐴) / (𝐵𝐴)) · ((∗‘𝐵) − (∗‘𝐴))) = ((𝑋𝐴) · (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴))))
865oveq2i 7441 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐴) · 𝑄) = ((𝑋𝐴) · (((∗‘𝐵) − (∗‘𝐴)) / (𝐵𝐴)))
8785, 86eqtr4di 2792 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑋𝐴) / (𝐵𝐴)) · ((∗‘𝐵) − (∗‘𝐴))) = ((𝑋𝐴) · 𝑄))
8836, 3, 15subdird 11717 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐴) · 𝑄) = ((𝑋 · 𝑄) − (𝐴 · 𝑄)))
8984, 87, 883eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((∗‘𝑇) · (∗‘(𝐵𝐴))) = ((𝑋 · 𝑄) − (𝐴 · 𝑄)))
9077, 89eqtrd 2774 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = ((𝑋 · 𝑄) − (𝐴 · 𝑄)))
9190oveq2d 7446 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + ((𝑋 · 𝑄) − (𝐴 · 𝑄))))
924, 52, 16addsub12d 11640 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((∗‘𝐴) + ((𝑋 · 𝑄) − (𝐴 · 𝑄))) = ((𝑋 · 𝑄) + ((∗‘𝐴) − (𝐴 · 𝑄))))
9376, 91, 923eqtrd 2778 . . . . . . . . . . . . . . . . 17 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((𝑋 · 𝑄) + ((∗‘𝐴) − (𝐴 · 𝑄))))
9493oveq1d 7445 . . . . . . . . . . . . . . . 16 (𝜑 → ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)) = (((𝑋 · 𝑄) + ((∗‘𝐴) − (𝐴 · 𝑄))) − (∗‘𝐶)))
9552, 17, 20addsubassd 11637 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑋 · 𝑄) + ((∗‘𝐴) − (𝐴 · 𝑄))) − (∗‘𝐶)) = ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))))
9675, 94, 953eqtrd 2778 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))))
9774, 96eqtrd 2774 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝑋𝐶)) = ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))))
9897oveq2d 7446 . . . . . . . . . . . . 13 (𝜑 → ((𝑋𝐶) · (∗‘(𝑋𝐶))) = ((𝑋𝐶) · ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))))
9968, 70cjsubd 32758 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐸𝐹)) = ((∗‘𝐸) − (∗‘𝐹)))
10099oveq2d 7446 . . . . . . . . . . . . 13 (𝜑 → ((𝐸𝐹) · (∗‘(𝐸𝐹))) = ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))
10173, 98, 1003eqtr3d 2782 . . . . . . . . . . . 12 (𝜑 → ((𝑋𝐶) · ((𝑋 · 𝑄) + (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))
10219, 36, 15mul12d 11467 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · (𝑋 · 𝑄)) = (𝑋 · (𝐶 · 𝑄)))
103102oveq1d 7445 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 · (𝑋 · 𝑄)) + (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((𝑋 · (𝐶 · 𝑄)) + (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))))
10460, 47, 103comraddd 11472 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (𝑋 · 𝑄)) + (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + (𝑋 · (𝐶 · 𝑄))))
105104oveq2d 7446 . . . . . . . . . . . 12 (𝜑 → (((𝑋 · (𝑋 · 𝑄)) + (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐶 · (𝑋 · 𝑄)) + (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))))) = (((𝑋 · (𝑋 · 𝑄)) + (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + (𝑋 · (𝐶 · 𝑄)))))
10662, 101, 1053eqtr3rd 2783 . . . . . . . . . . 11 (𝜑 → (((𝑋 · (𝑋 · 𝑄)) + (𝑋 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + (𝑋 · (𝐶 · 𝑄)))) = ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))
10758, 61, 1063eqtr2d 2780 . . . . . . . . . 10 (𝜑 → ((((𝑋↑2) · 𝑄) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) = ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))
10855, 107eqtrd 2774 . . . . . . . . 9 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) = ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))
10954, 46addcld 11277 . . . . . . . . . 10 (𝜑 → (((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) ∈ ℂ)
110109, 47subcld 11617 . . . . . . . . 9 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) ∈ ℂ)
111108, 110eqeltrrd 2839 . . . . . . . 8 (𝜑 → ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))) ∈ ℂ)
11247, 111addcld 11277 . . . . . . 7 (𝜑 → ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) ∈ ℂ)
113112negcld 11604 . . . . . 6 (𝜑 → -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) ∈ ℂ)
11446, 113, 15, 29divdird 12078 . . . . 5 (𝜑 → (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) / 𝑄) = (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) / 𝑄) + (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄)))
11545, 114eqtr4d 2777 . . . 4 (𝜑 → ((𝑀 · 𝑋) + 𝑁) = (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) / 𝑄))
116115oveq2d 7446 . . 3 (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) / 𝑄)))
11736sqcld 14180 . . . 4 (𝜑 → (𝑋↑2) ∈ ℂ)
11846, 113addcld 11277 . . . 4 (𝜑 → ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) ∈ ℂ)
119117, 15, 118, 29muldivdid 32757 . . 3 (𝜑 → ((((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) / 𝑄) = ((𝑋↑2) + (((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) / 𝑄)))
12054, 46, 113addassd 11280 . . . . 5 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) = (((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))))
121109, 112negsubd 11623 . . . . . 6 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) = ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))))
122109, 47, 111subsub4d 11648 . . . . . 6 (𝜑 → (((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) = ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − ((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))))
123110, 108subeq0bd 11686 . . . . . 6 (𝜑 → (((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) − (𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)))) − ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) = 0)
124121, 122, 1233eqtr2d 2780 . . . . 5 (𝜑 → ((((𝑋↑2) · 𝑄) + (𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹))))) = 0)
125120, 124eqtr3d 2776 . . . 4 (𝜑 → (((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) = 0)
12654, 118addcld 11277 . . . . 5 (𝜑 → (((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) ∈ ℂ)
127126, 15, 29diveq0ad 12050 . . . 4 (𝜑 → (((((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) / 𝑄) = 0 ↔ (((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) = 0))
128125, 127mpbird 257 . . 3 (𝜑 → ((((𝑋↑2) · 𝑄) + ((𝑋 · ((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄))) + -((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸𝐹) · ((∗‘𝐸) − (∗‘𝐹)))))) / 𝑄) = 0)
129116, 119, 1283eqtr2d 2780 . 2 (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
130129, 29jca 511 1 (𝜑 → (((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0 ∧ 𝑄 ≠ 0))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wne 2937  wss 3962  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152   + caddc 11155   · cmul 11157  cmin 11489  -cneg 11490   / cdiv 11917  2c2 12318  cexp 14098  ccj 15131  abscabs 15269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-sup 9479  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271
This theorem is referenced by:  constrfin  33750  constrelextdg2  33751
  Copyright terms: Public domain W3C validator