Proof of Theorem constrrtcclem
Step | Hyp | Ref
| Expression |
1 | | constrrtcc.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℂ) |
2 | 1 | sqcld 14190 |
. . 3
⊢ (𝜑 → (𝑋↑2) ∈ ℂ) |
3 | | constrrtcc.m |
. . . . 5
⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) |
4 | | constrrtcc.5 |
. . . . . . . . 9
⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) |
5 | | constrrtcc.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
6 | | constrrtcc.e |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
7 | 5, 6 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
8 | | constrrtcc.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
9 | 5, 8 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ℂ) |
10 | 7, 9 | subcld 11643 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ) |
11 | 10 | cjcld 15241 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ) |
12 | 10, 11 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) ∈ ℂ) |
13 | 4, 12 | eqeltrid 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℂ) |
14 | | constrrtcc.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑆) |
15 | 5, 14 | sseldd 4003 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
16 | 15 | cjcld 15241 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐷) ∈
ℂ) |
17 | | constrrtcc.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
18 | 5, 17 | sseldd 4003 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
19 | 15, 18 | addcld 11305 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ) |
20 | 16, 19 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ) |
21 | 13, 20 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ) |
22 | | constrrtcc.4 |
. . . . . . . . 9
⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) |
23 | | constrrtcc.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
24 | 5, 23 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
25 | | constrrtcc.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ 𝑆) |
26 | 5, 25 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
27 | 24, 26 | subcld 11643 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ) |
28 | 27 | cjcld 15241 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ) |
29 | 27, 28 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) ∈ ℂ) |
30 | 22, 29 | eqeltrid 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℂ) |
31 | 18 | cjcld 15241 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐴) ∈
ℂ) |
32 | 31, 19 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ) |
33 | 30, 32 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ) |
34 | 21, 33 | subcld 11643 |
. . . . . 6
⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ) |
35 | 16, 31 | subcld 11643 |
. . . . . 6
⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈
ℂ) |
36 | 15, 18 | cjsubd 32747 |
. . . . . . 7
⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴))) |
37 | 15, 18 | subcld 11643 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ) |
38 | | constrrtcc.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≠ 𝐷) |
39 | 38 | necomd 2998 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ≠ 𝐴) |
40 | 15, 18, 39 | subne0d 11652 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0) |
41 | 37, 40 | cjne0d 15248 |
. . . . . . 7
⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0) |
42 | 36, 41 | eqnetrrd 3011 |
. . . . . 6
⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0) |
43 | 34, 35, 42 | divcld 12066 |
. . . . 5
⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ) |
44 | 3, 43 | eqeltrid 2842 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℂ) |
45 | 44, 1 | mulcld 11306 |
. . 3
⊢ (𝜑 → (𝑀 · 𝑋) ∈ ℂ) |
46 | | constrrtcc.n |
. . . 4
⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) |
47 | 15, 18 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ) |
48 | 31, 47 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ) |
49 | 30, 15 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 · 𝐷) ∈ ℂ) |
50 | 48, 49 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ) |
51 | 16, 47 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ) |
52 | 13, 18 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 · 𝐴) ∈ ℂ) |
53 | 51, 52 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ) |
54 | 50, 53 | subcld 11643 |
. . . . . 6
⊢ (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ) |
55 | 54, 35, 42 | divcld 12066 |
. . . . 5
⊢ (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ) |
56 | 55 | negcld 11630 |
. . . 4
⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ) |
57 | 46, 56 | eqeltrid 2842 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℂ) |
58 | 2, 45, 57 | addassd 11308 |
. 2
⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁))) |
59 | 35, 2 | mulcld 11306 |
. . . . . . 7
⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ) |
60 | 34, 1 | mulcld 11306 |
. . . . . . 7
⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ) |
61 | 16, 31, 2 | subdird 11743 |
. . . . . . . . 9
⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2)))) |
62 | 21, 33, 1 | subdird 11743 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) |
63 | 61, 62 | oveq12d 7463 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))) |
64 | 16, 2 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ) |
65 | 21, 1 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ) |
66 | 31, 2 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ) |
67 | 33, 1 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ) |
68 | 64, 65, 66, 67 | addsub4d 11690 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))) |
69 | 1, 18 | subcld 11643 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ) |
70 | 1, 15 | subcld 11643 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ) |
71 | 69, 70 | mulcomd 11307 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = ((𝑋 − 𝐷) · (𝑋 − 𝐴))) |
72 | 71 | oveq2d 7461 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴)))) |
73 | 69 | cjcld 15241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) ∈ ℂ) |
74 | | constrrtcc.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) |
75 | | constrrtcclem.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
76 | 24, 26, 75 | subne0d 11652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0) |
77 | 27, 76 | absne0d 15492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ≠ 0) |
78 | 74, 77 | eqnetrd 3010 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) ≠ 0) |
79 | 69 | abs00ad 15335 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) = 0 ↔ (𝑋 − 𝐴) = 0)) |
80 | 79 | necon3bid 2987 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) ≠ 0 ↔ (𝑋 − 𝐴) ≠ 0)) |
81 | 78, 80 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 − 𝐴) ≠ 0) |
82 | 74 | oveq1d 7460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((abs‘(𝐵 − 𝐶))↑2)) |
83 | 69 | absvalsqd 15487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴)))) |
84 | 27 | absvalsqd 15487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))) |
85 | 82, 83, 84 | 3eqtr3d 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))) |
86 | 85, 22 | eqtr4di 2792 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = 𝑃) |
87 | 69, 73, 81, 86 | mvllmuld 12122 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = (𝑃 / (𝑋 − 𝐴))) |
88 | 87, 73 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 / (𝑋 − 𝐴)) ∈ ℂ) |
89 | 31, 88 | addcld 11305 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) ∈ ℂ) |
90 | 89, 69, 70 | mulassd 11309 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷)))) |
91 | 30, 69, 81 | divcan1d 12067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴)) = 𝑃) |
92 | 91 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) + ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴))) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃)) |
93 | 31, 69, 88, 92 | joinlmuladdmuld 11313 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃)) |
94 | 93 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷))) |
95 | 31, 69 | mulcld 11306 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐴) · (𝑋 − 𝐴)) ∈ ℂ) |
96 | 95, 30, 70 | adddird 11311 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷)))) |
97 | 31, 69, 70 | mulassd 11309 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷)))) |
98 | 1, 18, 1, 15 | mulsubd 11745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴)))) |
99 | 1 | sqvald 14189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑋↑2) = (𝑋 · 𝑋)) |
100 | 99 | oveq1d 7460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴))) |
101 | 1, 15, 18 | adddid 11310 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴))) |
102 | 100, 101 | oveq12d 7463 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴)))) |
103 | 1, 19 | mulcld 11306 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ) |
104 | 2, 47, 103 | addsubd 11664 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) |
105 | 98, 102, 104 | 3eqtr2d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) |
106 | 105 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))) |
107 | 2, 103 | subcld 11643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ) |
108 | 31, 107, 47 | adddid 11310 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴)))) |
109 | 97, 106, 108 | 3eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴)))) |
110 | 30, 1, 15 | subdid 11742 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 · (𝑋 − 𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷))) |
111 | 109, 110 | oveq12d 7463 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷)))) |
112 | 94, 96, 111 | 3eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷)))) |
113 | 1, 18 | cjsubd 32747 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = ((∗‘𝑋) − (∗‘𝐴))) |
114 | 113, 87 | eqtr3d 2776 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴))) |
115 | 1 | cjcld 15241 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘𝑋) ∈
ℂ) |
116 | 115, 31, 88 | subaddd 11661 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋))) |
117 | 114, 116 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋)) |
118 | 117 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷)))) |
119 | 90, 112, 118 | 3eqtr3rd 2783 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷)))) |
120 | 31, 107 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ) |
121 | 120, 48 | addcld 11305 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ) |
122 | 30, 1 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ) |
123 | 121, 122,
49 | addsubassd 11663 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷)))) |
124 | 120, 48, 122 | add32d 11513 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴)))) |
125 | 124 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷))) |
126 | 119, 123,
125 | 3eqtr2d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷))) |
127 | 120, 122 | addcld 11305 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ) |
128 | 127, 48, 49 | addsubassd 11663 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)))) |
129 | 32, 1 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ) |
130 | 66, 129, 122 | subadd23d 11665 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))) |
131 | 31, 2, 103 | subdid 11742 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))))) |
132 | 31, 1, 19 | mul12d 11495 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴)))) |
133 | 1, 32 | mulcomd 11307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) |
134 | 132, 133 | eqtrd 2774 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) |
135 | 134 | oveq2d 7461 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))) |
136 | 131, 135 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))) |
137 | 136 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋))) |
138 | 30, 32, 1 | subdird 11743 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))) |
139 | 138 | oveq2d 7461 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))) |
140 | 130, 137,
139 | 3eqtr4d 2784 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) |
141 | 140 | oveq1d 7460 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)))) |
142 | 126, 128,
141 | 3eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)))) |
143 | 70 | cjcld 15241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) ∈ ℂ) |
144 | | constrrtcc.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) |
145 | | constrrtcclem.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ≠ 𝐹) |
146 | 7, 9, 145 | subne0d 11652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 − 𝐹) ≠ 0) |
147 | 10, 146 | absne0d 15492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝐸 − 𝐹)) ≠ 0) |
148 | 144, 147 | eqnetrd 3010 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) ≠ 0) |
149 | 70 | abs00ad 15335 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) = 0 ↔ (𝑋 − 𝐷) = 0)) |
150 | 149 | necon3bid 2987 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) ≠ 0 ↔ (𝑋 − 𝐷) ≠ 0)) |
151 | 148, 150 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 − 𝐷) ≠ 0) |
152 | 144 | oveq1d 7460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((abs‘(𝐸 − 𝐹))↑2)) |
153 | 70 | absvalsqd 15487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷)))) |
154 | 10 | absvalsqd 15487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))) |
155 | 152, 153,
154 | 3eqtr3d 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))) |
156 | 155, 4 | eqtr4di 2792 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = 𝑄) |
157 | 70, 143, 151, 156 | mvllmuld 12122 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = (𝑄 / (𝑋 − 𝐷))) |
158 | 157, 143 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 / (𝑋 − 𝐷)) ∈ ℂ) |
159 | 16, 158 | addcld 11305 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) ∈ ℂ) |
160 | 159, 70, 69 | mulassd 11309 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴)))) |
161 | 13, 70, 151 | divcan1d 12067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷)) = 𝑄) |
162 | 161 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) + ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷))) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄)) |
163 | 16, 70, 158, 162 | joinlmuladdmuld 11313 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄)) |
164 | 163 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴))) |
165 | 16, 70 | mulcld 11306 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐷) · (𝑋 − 𝐷)) ∈ ℂ) |
166 | 165, 13, 69 | adddird 11311 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴)))) |
167 | 16, 70, 69 | mulassd 11309 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴)))) |
168 | 71 | oveq2d 7461 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴)))) |
169 | 167, 168 | eqtr4d 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷)))) |
170 | 105 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))) |
171 | 16, 107, 47 | adddid 11310 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴)))) |
172 | 169, 170,
171 | 3eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴)))) |
173 | 13, 1, 18 | subdid 11742 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 · (𝑋 − 𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴))) |
174 | 172, 173 | oveq12d 7463 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴)))) |
175 | 164, 166,
174 | 3eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴)))) |
176 | 1, 15 | cjsubd 32747 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = ((∗‘𝑋) − (∗‘𝐷))) |
177 | 176, 157 | eqtr3d 2776 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷))) |
178 | 115, 16, 158 | subaddd 11661 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋))) |
179 | 177, 178 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋)) |
180 | 179 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴)))) |
181 | 160, 175,
180 | 3eqtr3rd 2783 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴)))) |
182 | 16, 107 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ) |
183 | 182, 51 | addcld 11305 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ) |
184 | 13, 1 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ) |
185 | 183, 184,
52 | addsubassd 11663 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴)))) |
186 | 182, 51, 184 | add32d 11513 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴)))) |
187 | 186 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴))) |
188 | 181, 185,
187 | 3eqtr2d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴))) |
189 | 182, 184 | addcld 11305 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ) |
190 | 189, 51, 52 | addsubassd 11663 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
191 | 20, 1 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ) |
192 | 64, 191, 184 | subadd23d 11665 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))) |
193 | 16, 2, 103 | subdid 11742 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))))) |
194 | 16, 1, 19 | mul12d 11495 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴)))) |
195 | 1, 20 | mulcomd 11307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) |
196 | 194, 195 | eqtrd 2774 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) |
197 | 196 | oveq2d 7461 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))) |
198 | 193, 197 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))) |
199 | 198 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋))) |
200 | 13, 20, 1 | subdird 11743 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))) |
201 | 200 | oveq2d 7461 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))) |
202 | 192, 199,
201 | 3eqtr4d 2784 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋))) |
203 | 202 | oveq1d 7460 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
204 | 188, 190,
203 | 3eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
205 | 72, 142, 204 | 3eqtr3d 2782 |
. . . . . . . . 9
⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
206 | 140, 127 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ) |
207 | 202, 189 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ) |
208 | 206, 50, 207, 53 | addsubeq4d 11694 |
. . . . . . . . 9
⊢ (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))) |
209 | 205, 208 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
210 | 63, 68, 209 | 3eqtr2d 2780 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))) |
211 | 59, 60, 210 | mvlraddd 11696 |
. . . . . 6
⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋))) |
212 | 35, 2, 42, 211 | mvllmuld 12122 |
. . . . 5
⊢ (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴)))) |
213 | 54, 60, 35, 42 | divsubdird 12105 |
. . . . . 6
⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))))) |
214 | 46 | eqcomi 2743 |
. . . . . . . . 9
⊢
-(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁 |
215 | 214 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁) |
216 | 55, 215 | negcon1ad 11638 |
. . . . . . 7
⊢ (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))) |
217 | 216 | oveq1d 7460 |
. . . . . 6
⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))))) |
218 | 213, 217 | eqtr4d 2777 |
. . . . 5
⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))))) |
219 | 34, 1, 35, 42 | div23d 12103 |
. . . . . . 7
⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)) |
220 | 3 | oveq1i 7455 |
. . . . . . 7
⊢ (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋) |
221 | 219, 220 | eqtr4di 2792 |
. . . . . 6
⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋)) |
222 | 221 | oveq2d 7461 |
. . . . 5
⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋))) |
223 | 212, 218,
222 | 3eqtrd 2778 |
. . . 4
⊢ (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))) |
224 | 216, 55 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → -𝑁 ∈ ℂ) |
225 | 2, 45, 224 | addlsub 11702 |
. . . 4
⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))) |
226 | 223, 225 | mpbird 257 |
. . 3
⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁) |
227 | 2, 45 | addcld 11305 |
. . . 4
⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ) |
228 | | addeq0 11709 |
. . . 4
⊢ ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)) |
229 | 227, 57, 228 | syl2anc 583 |
. . 3
⊢ (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)) |
230 | 226, 229 | mpbird 257 |
. 2
⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0) |
231 | 58, 230 | eqtr3d 2776 |
1
⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) |