Proof of Theorem constrrtcc
Step | Hyp | Ref
| Expression |
1 | | constrrtcc.m |
. . . . . . . . . 10
⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))) |
3 | | constrrtcc.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) |
4 | | constrrtcc.s |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | | constrrtcc.e |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
6 | 4, 5 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸 ∈ ℂ) |
7 | | constrrtcc.f |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
8 | 4, 7 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ∈ ℂ) |
9 | 6, 8 | subcld 11643 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐸 − 𝐹) ∈ ℂ) |
11 | 10 | absvalsqd 15487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))) |
12 | 3, 11 | eqtr4id 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((abs‘(𝐸 − 𝐹))↑2)) |
13 | | constrrtcc.x |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ ℂ) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 ∈ ℂ) |
15 | | constrrtcc.a |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
16 | 4, 15 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℂ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐴 ∈ ℂ) |
18 | 13, 16 | subcld 11643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) ∈ ℂ) |
20 | | constrrtcc.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) |
22 | | constrrtcc.b |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
23 | 4, 22 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 ∈ ℂ) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ) |
25 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶) |
26 | 24, 25 | subeq0bd 11712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐶) = 0) |
27 | 26 | abs00bd 15336 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐵 − 𝐶)) = 0) |
28 | 21, 27 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐴)) = 0) |
29 | 19, 28 | abs00d 15491 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 − 𝐴) = 0) |
30 | 14, 17, 29 | subeq0d 11651 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑋 = 𝐴) |
31 | 30 | fvoveq1d 7467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐴 − 𝐷))) |
32 | | constrrtcc.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) |
34 | | constrrtcc.d |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ 𝑆) |
35 | 4, 34 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷 ∈ ℂ) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐷 ∈ ℂ) |
37 | 17, 36 | abssubd 15498 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐴 − 𝐷)) = (abs‘(𝐷 − 𝐴))) |
38 | 31, 33, 37 | 3eqtr3d 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (abs‘(𝐸 − 𝐹)) = (abs‘(𝐷 − 𝐴))) |
39 | 38 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐸 − 𝐹))↑2) = ((abs‘(𝐷 − 𝐴))↑2)) |
40 | 35, 16 | subcld 11643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ) |
41 | 40 | absvalsqd 15487 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
43 | 12, 39, 42 | 3eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑄 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
44 | 43 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴)))) |
45 | | constrrtcc.4 |
. . . . . . . . . . . . . . 15
⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) |
46 | 26 | oveq1d 7460 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = (0 · (∗‘(𝐵 − 𝐶)))) |
47 | | constrrtcc.c |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ 𝑆) |
48 | 4, 47 | sseldd 4003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐶 ∈ ℂ) |
49 | 23, 48 | subcld 11643 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ) |
50 | 49 | cjcld 15241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐵 − 𝐶)) ∈ ℂ) |
52 | 51 | mul02d 11484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · (∗‘(𝐵 − 𝐶))) = 0) |
53 | 46, 52 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) = 0) |
54 | 45, 53 | eqtrid 2786 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 = 0) |
55 | 54 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐴) · (𝐷 + 𝐴)))) |
56 | 44, 55 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 −
((∗‘𝐴)
· (𝐷 + 𝐴))))) |
57 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 − 𝐴) ∈ ℂ) |
58 | 57 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ∈ ℂ) |
59 | 57, 58 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ) |
60 | 36 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐷) ∈ ℂ) |
61 | 36, 17 | addcld 11305 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 + 𝐴) ∈ ℂ) |
62 | 60, 61 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ) |
63 | | 0cnd 11279 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 ∈ ℂ) |
64 | 17 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘𝐴) ∈ ℂ) |
65 | 64, 61 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ) |
66 | 59, 62, 63, 65 | sub4d 11692 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐷) · (𝐷 + 𝐴))) − (0 −
((∗‘𝐴)
· (𝐷 + 𝐴)))) = ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) −
(((∗‘𝐷)
· (𝐷 + 𝐴)) −
((∗‘𝐴)
· (𝐷 + 𝐴))))) |
67 | 59 | subid1d 11632 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
68 | 35, 16 | cjsubd 32747 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴))) |
69 | 68 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴))) |
70 | 40 | cjcld 15241 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ∈ ℂ) |
71 | 35, 16 | addcld 11305 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ) |
72 | 70, 71 | mulcomd 11307 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 + 𝐴)) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))) |
73 | 35 | cjcld 15241 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘𝐷) ∈
ℂ) |
74 | 16 | cjcld 15241 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘𝐴) ∈
ℂ) |
75 | 73, 74, 71 | subdird 11743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝐷 + 𝐴)) = (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) |
76 | 69, 72, 75 | 3eqtr3rd 2783 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))) |
78 | 67, 77 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − 0) −
(((∗‘𝐷)
· (𝐷 + 𝐴)) −
((∗‘𝐴)
· (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
79 | 56, 66, 78 | 3eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
80 | 57, 61, 58 | subdird 11743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
81 | 61, 57 | negsubdi2d 11659 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = ((𝐷 − 𝐴) − (𝐷 + 𝐴))) |
82 | 36, 17, 17 | pnncand 11682 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (𝐴 + 𝐴)) |
83 | 17 | 2timesd 12532 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) = (𝐴 + 𝐴)) |
84 | 82, 83 | eqtr4d 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 + 𝐴) − (𝐷 − 𝐴)) = (2 · 𝐴)) |
85 | 84 | negeqd 11526 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((𝐷 + 𝐴) − (𝐷 − 𝐴)) = -(2 · 𝐴)) |
86 | 81, 85 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) − (𝐷 + 𝐴)) = -(2 · 𝐴)) |
87 | 86 | oveq1d 7460 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (-(2 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
88 | 79, 80, 87 | 3eqtr2rd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))))) |
89 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴))) |
90 | 88, 89 | oveq12d 7463 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))) |
91 | | 2cnd 12367 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 2 ∈ ℂ) |
92 | 91, 17 | mulcld 11306 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · 𝐴) ∈ ℂ) |
93 | 92 | negcld 11630 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · 𝐴) ∈ ℂ) |
94 | | constrrtcc.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≠ 𝐷) |
95 | 94 | necomd 2998 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ≠ 𝐴) |
96 | 35, 16, 95 | subne0d 11652 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0) |
97 | 40, 96 | cjne0d 15248 |
. . . . . . . . . . 11
⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0) |
98 | 97 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (∗‘(𝐷 − 𝐴)) ≠ 0) |
99 | 93, 58, 98 | divcan4d 12072 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(2 · 𝐴) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐴)) |
100 | 2, 90, 99 | 3eqtr2d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑀 = -(2 · 𝐴)) |
101 | 100 | oveq1d 7460 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = (-(2 · 𝐴) · 𝑋)) |
102 | 92, 14 | mulneg1d 11739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(2 · 𝐴) · 𝑋) = -((2 · 𝐴) · 𝑋)) |
103 | 91, 17, 14 | mulassd 11309 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝐴 · 𝑋))) |
104 | 17, 14 | mulcomd 11307 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴 · 𝑋) = (𝑋 · 𝐴)) |
105 | 104 | oveq2d 7461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝐴 · 𝑋)) = (2 · (𝑋 · 𝐴))) |
106 | 103, 105 | eqtrd 2774 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((2 · 𝐴) · 𝑋) = (2 · (𝑋 · 𝐴))) |
107 | 106 | negeqd 11526 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -((2 · 𝐴) · 𝑋) = -(2 · (𝑋 · 𝐴))) |
108 | 101, 102,
107 | 3eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐴))) |
109 | | constrrtcc.n |
. . . . . . 7
⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) |
110 | 17 | sqcld 14190 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) ∈ ℂ) |
111 | 54 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = (0 · 𝐷)) |
112 | 36 | mul02d 11484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (0 · 𝐷) = 0) |
113 | 111, 112 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑃 · 𝐷) = 0) |
114 | 113 | oveq2d 7461 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − 0)) |
115 | 36, 17 | mulcld 11306 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐷 · 𝐴) ∈ ℂ) |
116 | 64, 115 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ) |
117 | 116 | subid1d 11632 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐴) · (𝐷 · 𝐴))) |
118 | 114, 117 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = ((∗‘𝐴) · (𝐷 · 𝐴))) |
119 | 43 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑄 · 𝐴) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) |
120 | 119 | oveq2d 7461 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))) |
121 | 118, 120 | oveq12d 7463 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)))) |
122 | 60, 115 | mulcld 11306 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ) |
123 | 59, 17 | mulcld 11306 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) ∈ ℂ) |
124 | 116, 122,
123 | subsubd 11671 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴))) |
125 | 68 | negeqd 11526 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -(∗‘(𝐷 − 𝐴)) = -((∗‘𝐷) − (∗‘𝐴))) |
126 | 73, 74 | negsubdi2d 11659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -((∗‘𝐷) − (∗‘𝐴)) = ((∗‘𝐴) − (∗‘𝐷))) |
127 | 125, 126 | eqtr2d 2775 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∗‘𝐴) − (∗‘𝐷)) = -(∗‘(𝐷 − 𝐴))) |
128 | 127 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴))) |
129 | 35, 16 | mulcld 11306 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ) |
130 | 74, 73, 129 | subdird 11743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐷)) · (𝐷 · 𝐴)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴)))) |
131 | 70, 129 | mulcomd 11307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = ((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
132 | 131 | negeqd 11526 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
133 | 70, 129 | mulneg1d 11739 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = -((∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴))) |
134 | 129, 70 | mulneg1d 11739 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
135 | 132, 133,
134 | 3eqtr4d 2784 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (-(∗‘(𝐷 − 𝐴)) · (𝐷 · 𝐴)) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
136 | 128, 130,
135 | 3eqtr3d 2782 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
137 | 136 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
138 | 57, 58, 17 | mul32d 11496 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
139 | 36, 17, 17 | subdird 11743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴 · 𝐴))) |
140 | 17 | sqvald 14189 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐴↑2) = (𝐴 · 𝐴)) |
141 | 140 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) = ((𝐷 · 𝐴) − (𝐴 · 𝐴))) |
142 | 139, 141 | eqtr4d 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 − 𝐴) · 𝐴) = ((𝐷 · 𝐴) − (𝐴↑2))) |
143 | 142 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · 𝐴) · (∗‘(𝐷 − 𝐴))) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))) |
144 | 138, 143 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴) = (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴)))) |
145 | 137, 144 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))) |
146 | 115 | negcld 11630 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐷 · 𝐴) ∈ ℂ) |
147 | 115, 110 | subcld 11643 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐴↑2)) ∈ ℂ) |
148 | 146, 147,
58 | adddird 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) + (((𝐷 · 𝐴) − (𝐴↑2)) · (∗‘(𝐷 − 𝐴))))) |
149 | 115 | subidd 11631 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0) |
150 | 149 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2)) = (0 − (𝐴↑2))) |
151 | 146, 147 | addcomd 11488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴))) |
152 | 147, 115 | negsubd 11649 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) + -(𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴))) |
153 | 115, 110,
115 | sub32d 11675 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝐷 · 𝐴) − (𝐴↑2)) − (𝐷 · 𝐴)) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2))) |
154 | 151, 152,
153 | 3eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = (((𝐷 · 𝐴) − (𝐷 · 𝐴)) − (𝐴↑2))) |
155 | | df-neg 11519 |
. . . . . . . . . . . . . . 15
⊢ -(𝐴↑2) = (0 − (𝐴↑2)) |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (0 − (𝐴↑2))) |
157 | 150, 154,
156 | 3eqtr4d 2784 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) = -(𝐴↑2)) |
158 | 157 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐷 · 𝐴) + ((𝐷 · 𝐴) − (𝐴↑2))) · (∗‘(𝐷 − 𝐴))) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴)))) |
159 | 145, 148,
158 | 3eqtr2d 2780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) + (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐴)) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴)))) |
160 | 121, 124,
159 | 3eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐴↑2) · (∗‘(𝐷 − 𝐴)))) |
161 | 89 | eqcomd 2740 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴))) |
162 | 160, 161 | oveq12d 7463 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴)))) |
163 | 110 | negcld 11630 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) ∈ ℂ) |
164 | 163, 58, 98 | divcan4d 12072 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((-(𝐴↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐴↑2)) |
165 | 162, 164 | eqtr2d 2775 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(𝐴↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))) |
166 | 110, 165 | negcon1ad 11638 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐴↑2)) |
167 | 109, 166 | eqtrid 2786 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑁 = (𝐴↑2)) |
168 | 108, 167 | oveq12d 7463 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐴)) + (𝐴↑2))) |
169 | 168 | oveq2d 7461 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2)))) |
170 | 14 | sqcld 14190 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋↑2) ∈ ℂ) |
171 | 14, 17 | mulcld 11306 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝑋 · 𝐴) ∈ ℂ) |
172 | 91, 171 | mulcld 11306 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (2 · (𝑋 · 𝐴)) ∈ ℂ) |
173 | 172 | negcld 11630 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → -(2 · (𝑋 · 𝐴)) ∈ ℂ) |
174 | 170, 173,
110 | addassd 11308 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐴)) + (𝐴↑2)))) |
175 | 170, 172 | negsubd 11649 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + -(2 · (𝑋 · 𝐴))) = ((𝑋↑2) − (2 · (𝑋 · 𝐴)))) |
176 | 175 | oveq1d 7460 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (((𝑋↑2) + -(2 · (𝑋 · 𝐴))) + (𝐴↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2))) |
177 | 169, 174,
176 | 3eqtr2d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2))) |
178 | | binom2sub 14265 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2))) |
179 | 14, 17, 178 | syl2anc 583 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐴))) + (𝐴↑2))) |
180 | 29 | sq0id 14239 |
. . 3
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋 − 𝐴)↑2) = 0) |
181 | 177, 179,
180 | 3eqtr2d 2780 |
. 2
⊢ ((𝜑 ∧ 𝐵 = 𝐶) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) |
182 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))) |
183 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 ∈ ℂ) |
184 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐸 = 𝐹) |
185 | 183, 184 | subeq0bd 11712 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐸 − 𝐹) = 0) |
186 | 185 | oveq1d 7460 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = (0 · (∗‘(𝐸 − 𝐹)))) |
187 | 9 | cjcld 15241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ) |
188 | 187 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐸 − 𝐹)) ∈ ℂ) |
189 | 188 | mul02d 11484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · (∗‘(𝐸 − 𝐹))) = 0) |
190 | 186, 189 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) = 0) |
191 | 3, 190 | eqtrid 2786 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑄 = 0) |
192 | 191 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) = (0 − ((∗‘𝐷) · (𝐷 + 𝐴)))) |
193 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐵 − 𝐶) ∈ ℂ) |
194 | 193 | absvalsqd 15487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))) |
195 | 45, 194 | eqtr4id 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((abs‘(𝐵 − 𝐶))↑2)) |
196 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) |
197 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 ∈ ℂ) |
198 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐷 ∈ ℂ) |
199 | 13, 35 | subcld 11643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ) |
200 | 199 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) ∈ ℂ) |
201 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) |
202 | 185 | abs00bd 15336 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐸 − 𝐹)) = 0) |
203 | 201, 202 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐷)) = 0) |
204 | 200, 203 | abs00d 15491 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 − 𝐷) = 0) |
205 | 197, 198,
204 | subeq0d 11651 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑋 = 𝐷) |
206 | 205 | fvoveq1d 7467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐷 − 𝐴))) |
207 | 196, 206 | eqtr3d 2776 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐷 − 𝐴))) |
208 | 207 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐵 − 𝐶))↑2) = ((abs‘(𝐷 − 𝐴))↑2)) |
209 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((abs‘(𝐷 − 𝐴))↑2) = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
210 | 195, 208,
209 | 3eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑃 = ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
211 | 210 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))) |
212 | 192, 211 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴))))) |
213 | | 0cnd 11279 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 0 ∈ ℂ) |
214 | 198 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐷) ∈ ℂ) |
215 | 16 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝐴 ∈ ℂ) |
216 | 198, 215 | addcld 11305 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 + 𝐴) ∈ ℂ) |
217 | 214, 216 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ) |
218 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 − 𝐴) ∈ ℂ) |
219 | 218 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ∈ ℂ) |
220 | 218, 219 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) ∈ ℂ) |
221 | 215 | cjcld 15241 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘𝐴) ∈ ℂ) |
222 | 221, 216 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ) |
223 | 213, 217,
220, 222 | sub4d 11692 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))))) |
224 | 218, 219 | mulneg1d 11739 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
225 | 198, 215 | negsubdi2d 11659 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 − 𝐴) = (𝐴 − 𝐷)) |
226 | 225 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴)))) |
227 | | df-neg 11519 |
. . . . . . . . . . . . . . 15
⊢ -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) = (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))))) |
229 | 224, 226,
228 | 3eqtr3rd 2783 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) = ((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴)))) |
230 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴))) = ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴)))) |
231 | 229, 230 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((0 − ((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴)))) − (((∗‘𝐷) · (𝐷 + 𝐴)) − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
232 | 212, 223,
231 | 3eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
233 | 215, 198 | subcld 11643 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 − 𝐷) ∈ ℂ) |
234 | 233, 216,
219 | subdird 11743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (((𝐴 − 𝐷) · (∗‘(𝐷 − 𝐴))) − ((𝐷 + 𝐴) · (∗‘(𝐷 − 𝐴))))) |
235 | 216, 233 | negsubdi2d 11659 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = ((𝐴 − 𝐷) − (𝐷 + 𝐴))) |
236 | 198 | 2timesd 12532 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) = (𝐷 + 𝐷)) |
237 | 215, 198,
198 | pnncand 11682 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = (𝐷 + 𝐷)) |
238 | 215, 198 | addcomd 11488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐴 + 𝐷) = (𝐷 + 𝐴)) |
239 | 238 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 + 𝐷) − (𝐴 − 𝐷)) = ((𝐷 + 𝐴) − (𝐴 − 𝐷))) |
240 | 236, 237,
239 | 3eqtr2rd 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 + 𝐴) − (𝐴 − 𝐷)) = (2 · 𝐷)) |
241 | 240 | negeqd 11526 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((𝐷 + 𝐴) − (𝐴 − 𝐷)) = -(2 · 𝐷)) |
242 | 235, 241 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐴 − 𝐷) − (𝐷 + 𝐴)) = -(2 · 𝐷)) |
243 | 242 | oveq1d 7460 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐴 − 𝐷) − (𝐷 + 𝐴)) · (∗‘(𝐷 − 𝐴))) = (-(2 · 𝐷) · (∗‘(𝐷 − 𝐴)))) |
244 | 232, 234,
243 | 3eqtr2rd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) = ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))))) |
245 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴))) |
246 | 244, 245 | oveq12d 7463 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))) |
247 | | 2cnd 12367 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 2 ∈ ℂ) |
248 | 247, 198 | mulcld 11306 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · 𝐷) ∈ ℂ) |
249 | 248 | negcld 11630 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · 𝐷) ∈ ℂ) |
250 | 97 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (∗‘(𝐷 − 𝐴)) ≠ 0) |
251 | 249, 219,
250 | divcan4d 12072 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(2 · 𝐷) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(2 · 𝐷)) |
252 | 182, 246,
251 | 3eqtr2d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑀 = -(2 · 𝐷)) |
253 | 252 | oveq1d 7460 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = (-(2 · 𝐷) · 𝑋)) |
254 | 248, 197 | mulneg1d 11739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(2 · 𝐷) · 𝑋) = -((2 · 𝐷) · 𝑋)) |
255 | 247, 198,
197 | mulassd 11309 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝐷 · 𝑋))) |
256 | 198, 197 | mulcomd 11307 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝑋) = (𝑋 · 𝐷)) |
257 | 256 | oveq2d 7461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝐷 · 𝑋)) = (2 · (𝑋 · 𝐷))) |
258 | 255, 257 | eqtrd 2774 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((2 · 𝐷) · 𝑋) = (2 · (𝑋 · 𝐷))) |
259 | 258 | negeqd 11526 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -((2 · 𝐷) · 𝑋) = -(2 · (𝑋 · 𝐷))) |
260 | 253, 254,
259 | 3eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑀 · 𝑋) = -(2 · (𝑋 · 𝐷))) |
261 | 198 | sqcld 14190 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) ∈ ℂ) |
262 | 210 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑃 · 𝐷) = (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) |
263 | 262 | oveq2d 7461 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) = (((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷))) |
264 | 191 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = (0 · 𝐴)) |
265 | 215 | mul02d 11484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (0 · 𝐴) = 0) |
266 | 264, 265 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑄 · 𝐴) = 0) |
267 | 266 | oveq2d 7461 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = (((∗‘𝐷) · (𝐷 · 𝐴)) − 0)) |
268 | 198, 215 | mulcld 11306 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) ∈ ℂ) |
269 | 214, 268 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ) |
270 | 269 | subid1d 11632 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − 0) = ((∗‘𝐷) · (𝐷 · 𝐴))) |
271 | 267, 270 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) = ((∗‘𝐷) · (𝐷 · 𝐴))) |
272 | 263, 271 | oveq12d 7463 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴)))) |
273 | 221, 268 | mulcld 11306 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ) |
274 | 220, 198 | mulcld 11306 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) ∈ ℂ) |
275 | 273, 274,
269 | sub32d 11675 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷))) |
276 | 136 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) = (-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴)))) |
277 | 218, 219,
198 | mul32d 11496 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴)))) |
278 | 198, 215,
198 | subdird 11743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷 · 𝐷) − (𝐴 · 𝐷))) |
279 | 198 | sqvald 14189 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷↑2) = (𝐷 · 𝐷)) |
280 | 198, 215 | mulcomd 11307 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝐷 · 𝐴) = (𝐴 · 𝐷)) |
281 | 279, 280 | oveq12d 7463 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) = ((𝐷 · 𝐷) − (𝐴 · 𝐷))) |
282 | 278, 281 | eqtr4d 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 − 𝐴) · 𝐷) = ((𝐷↑2) − (𝐷 · 𝐴))) |
283 | 282 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · 𝐷) · (∗‘(𝐷 − 𝐴))) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))) |
284 | 277, 283 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷) = (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴)))) |
285 | 276, 284 | oveq12d 7463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))) |
286 | 268 | negcld 11630 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷 · 𝐴) ∈ ℂ) |
287 | 261, 268 | subcld 11643 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷↑2) − (𝐷 · 𝐴)) ∈ ℂ) |
288 | 286, 287,
219 | subdird 11743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = ((-(𝐷 · 𝐴) · (∗‘(𝐷 − 𝐴))) − (((𝐷↑2) − (𝐷 · 𝐴)) · (∗‘(𝐷 − 𝐴))))) |
289 | 286, 268 | addcomd 11488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = ((𝐷 · 𝐴) + -(𝐷 · 𝐴))) |
290 | 268, 268 | negsubd 11649 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) + -(𝐷 · 𝐴)) = ((𝐷 · 𝐴) − (𝐷 · 𝐴))) |
291 | 268 | subidd 11631 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝐷 · 𝐴) − (𝐷 · 𝐴)) = 0) |
292 | 289, 290,
291 | 3eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) + (𝐷 · 𝐴)) = 0) |
293 | 292 | oveq1d 7460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2)) = (0 − (𝐷↑2))) |
294 | 286, 261,
268 | subsub3d 11673 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = ((-(𝐷 · 𝐴) + (𝐷 · 𝐴)) − (𝐷↑2))) |
295 | | df-neg 11519 |
. . . . . . . . . . . . . . 15
⊢ -(𝐷↑2) = (0 − (𝐷↑2)) |
296 | 295 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (0 − (𝐷↑2))) |
297 | 293, 294,
296 | 3eqtr4d 2784 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) = -(𝐷↑2)) |
298 | 297 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷 · 𝐴) − ((𝐷↑2) − (𝐷 · 𝐴))) · (∗‘(𝐷 − 𝐴))) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴)))) |
299 | 285, 288,
298 | 3eqtr2d 2780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − ((∗‘𝐷) · (𝐷 · 𝐴))) − (((𝐷 − 𝐴) · (∗‘(𝐷 − 𝐴))) · 𝐷)) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴)))) |
300 | 272, 275,
299 | 3eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = (-(𝐷↑2) · (∗‘(𝐷 − 𝐴)))) |
301 | 245 | eqcomd 2740 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((∗‘𝐷) − (∗‘𝐴)) = (∗‘(𝐷 − 𝐴))) |
302 | 300, 301 | oveq12d 7463 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = ((-(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴)))) |
303 | 261 | negcld 11630 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) ∈ ℂ) |
304 | 303, 219,
250 | divcan4d 12072 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((-(𝐷↑2) · (∗‘(𝐷 − 𝐴))) / (∗‘(𝐷 − 𝐴))) = -(𝐷↑2)) |
305 | 302, 304 | eqtr2d 2775 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(𝐷↑2) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))) |
306 | 261, 305 | negcon1ad 11638 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = (𝐷↑2)) |
307 | 109, 306 | eqtrid 2786 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝑁 = (𝐷↑2)) |
308 | 260, 307 | oveq12d 7463 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑀 · 𝑋) + 𝑁) = (-(2 · (𝑋 · 𝐷)) + (𝐷↑2))) |
309 | 308 | oveq2d 7461 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2)))) |
310 | 197 | sqcld 14190 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋↑2) ∈ ℂ) |
311 | 197, 198 | mulcld 11306 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (𝑋 · 𝐷) ∈ ℂ) |
312 | 247, 311 | mulcld 11306 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (2 · (𝑋 · 𝐷)) ∈ ℂ) |
313 | 312 | negcld 11630 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → -(2 · (𝑋 · 𝐷)) ∈ ℂ) |
314 | 310, 313,
261 | addassd 11308 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = ((𝑋↑2) + (-(2 · (𝑋 · 𝐷)) + (𝐷↑2)))) |
315 | 310, 312 | negsubd 11649 |
. . . . 5
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + -(2 · (𝑋 · 𝐷))) = ((𝑋↑2) − (2 · (𝑋 · 𝐷)))) |
316 | 315 | oveq1d 7460 |
. . . 4
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → (((𝑋↑2) + -(2 · (𝑋 · 𝐷))) + (𝐷↑2)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2))) |
317 | 309, 314,
316 | 3eqtr2d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2))) |
318 | | binom2sub 14265 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2))) |
319 | 197, 198,
318 | syl2anc 583 |
. . 3
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = (((𝑋↑2) − (2 · (𝑋 · 𝐷))) + (𝐷↑2))) |
320 | 204 | sq0id 14239 |
. . 3
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋 − 𝐷)↑2) = 0) |
321 | 317, 319,
320 | 3eqtr2d 2780 |
. 2
⊢ ((𝜑 ∧ 𝐸 = 𝐹) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) |
322 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑆 ⊆ ℂ) |
323 | 15 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ∈ 𝑆) |
324 | 22 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ∈ 𝑆) |
325 | 47 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐶 ∈ 𝑆) |
326 | 34 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐷 ∈ 𝑆) |
327 | 5 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ∈ 𝑆) |
328 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐹 ∈ 𝑆) |
329 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝑋 ∈ ℂ) |
330 | 94 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐴 ≠ 𝐷) |
331 | 20 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) |
332 | 32 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) |
333 | | simprl 770 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐵 ≠ 𝐶) |
334 | | simprr 772 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → 𝐸 ≠ 𝐹) |
335 | 322, 323,
324, 325, 326, 327, 328, 329, 330, 331, 332, 45, 3, 1, 109, 333, 334 | constrrtcclem 33717 |
. 2
⊢ ((𝜑 ∧ (𝐵 ≠ 𝐶 ∧ 𝐸 ≠ 𝐹)) → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) |
336 | 181, 321,
335 | pm2.61da2ne 3032 |
1
⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) |