Step | Hyp | Ref
| Expression |
1 | | dcubic.0 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ≠ 0) |
2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ≠ 0) |
3 | | dcubic.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℂ) |
4 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ∈ ℂ) |
5 | | 3z 12336 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
6 | | expne0i 13796 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ)
→ (𝑇↑3) ≠
0) |
7 | 5, 6 | mp3an3 1448 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) → (𝑇↑3) ≠
0) |
8 | 7 | ex 412 |
. . . . . . . 8
⊢ (𝑇 ∈ ℂ → (𝑇 ≠ 0 → (𝑇↑3) ≠
0)) |
9 | 4, 8 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0)) |
10 | | dcubic.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁)) |
11 | 10 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁)) |
12 | | dcubic.g |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ ℂ) |
13 | 12 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈
ℂ) |
14 | | dcubic.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3))) |
15 | 14 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3))) |
16 | | dcubic.n |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 = (𝑄 / 2)) |
17 | 16 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2)) |
18 | | simprl 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0) |
19 | 18 | oveq2d 7284 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0)) |
20 | | dcubic.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑃 ∈ ℂ) |
21 | 20 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈
ℂ) |
22 | 21 | mul01d 11157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 0) =
0) |
23 | 19, 22 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = 0) |
24 | 23 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄)) |
25 | 18 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) =
(0↑3)) |
26 | | 3nn 12035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 ∈
ℕ |
27 | | 0exp 13799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 ∈
ℕ → (0↑3) = 0) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0↑3) = 0 |
29 | 25, 28 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0) |
30 | 29 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄))) |
31 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) |
32 | | 0cnd 10952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 0 ∈
ℂ) |
33 | 23, 32 | eqeltrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) ∈ ℂ) |
34 | | dcubic.d |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑄 ∈ ℂ) |
35 | 34 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈
ℂ) |
36 | 33, 35 | addcld 10978 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ) |
37 | 36 | addid2d 11159 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + ((𝑃 · 𝑋) + 𝑄)) = ((𝑃 · 𝑋) + 𝑄)) |
38 | 30, 31, 37 | 3eqtr3rd 2788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = 0) |
39 | 35 | addid2d 11159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + 𝑄) = 𝑄) |
40 | 24, 38, 39 | 3eqtr3rd 2788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 = 0) |
41 | 40 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 /
2)) |
42 | | 2cn 12031 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ |
43 | | 2ne0 12060 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
44 | 42, 43 | div0i 11692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 / 2) =
0 |
45 | 41, 44 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = 0) |
46 | 17, 45 | eqtrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = 0) |
47 | 46 | sq0id 13892 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑁↑2) = 0) |
48 | | dcubic.m |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 = (𝑃 / 3)) |
49 | | 3cn 12037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℂ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 3 ∈
ℂ) |
51 | | 3ne0 12062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ≠
0 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 3 ≠ 0) |
53 | 20, 50, 52 | divcld 11734 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃 / 3) ∈ ℂ) |
54 | 48, 53 | eqeltrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
55 | 54 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 ∈
ℂ) |
56 | | 4cn 12041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 4 ∈
ℂ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ∈
ℂ) |
58 | | 4ne0 12064 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 4 ≠
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠
0) |
60 | 18 | sq0id 13892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0) |
61 | 60 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀))) |
62 | | dcubic.x |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋 ∈ ℂ) |
63 | 62 | sqcld 13843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑋↑2) ∈ ℂ) |
64 | | mulcl 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((4
∈ ℂ ∧ 𝑀
∈ ℂ) → (4 · 𝑀) ∈ ℂ) |
65 | 56, 54, 64 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (4 · 𝑀) ∈
ℂ) |
66 | 63, 65 | addcld 10978 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ) |
67 | 66 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈
ℂ) |
68 | | simprr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) →
(√‘((𝑋↑2)
+ (4 · 𝑀))) =
0) |
69 | 67, 68 | sqr00d 15134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0) |
70 | 65 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 ·
𝑀) ∈
ℂ) |
71 | 70 | addid2d 11159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + (4
· 𝑀)) = (4 ·
𝑀)) |
72 | 61, 69, 71 | 3eqtr3rd 2788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 ·
𝑀) = 0) |
73 | 56 | mul01i 11148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (4
· 0) = 0 |
74 | 72, 73 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 ·
𝑀) = (4 ·
0)) |
75 | 55, 32, 57, 59, 74 | mulcanad 11593 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0) |
76 | 75 | oveq1d 7283 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) =
(0↑3)) |
77 | 76, 28 | eqtrdi 2795 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0) |
78 | 47, 77 | oveq12d 7286 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0)) |
79 | | 00id 11133 |
. . . . . . . . . . . . . . 15
⊢ (0 + 0) =
0 |
80 | 78, 79 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = 0) |
81 | 15, 80 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = 0) |
82 | 13, 81 | sqeq0d 13844 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0) |
83 | 82, 46 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0)) |
84 | | 0m0e0 12076 |
. . . . . . . . . . 11
⊢ (0
− 0) = 0 |
85 | 83, 84 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = 0) |
86 | 11, 85 | eqtrd 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = 0) |
87 | 86 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → (𝑇↑3) = 0)) |
88 | 87 | necon3ad 2957 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑇↑3) ≠ 0 → ¬ (𝑋 = 0 ∧
(√‘((𝑋↑2)
+ (4 · 𝑀))) =
0))) |
89 | 9, 88 | syld 47 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))) |
90 | 2, 89 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) |
91 | | oveq12 7277 |
. . . . . . . . . . 11
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0)) |
92 | 91, 79 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) |
93 | | oveq12 7277 |
. . . . . . . . . . 11
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 −
0)) |
94 | 93, 84 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) |
95 | 92, 94 | jca 511 |
. . . . . . . . 9
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)) |
96 | 66 | sqrtcld 15130 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈
ℂ) |
97 | | halfaddsub 12189 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧
(√‘((𝑋↑2)
+ (4 · 𝑀))) ∈
ℂ) → ((((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2) +
((𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)) =
𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) =
(√‘((𝑋↑2)
+ (4 · 𝑀))))) |
98 | 62, 96, 97 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀))))) |
99 | 98 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋) |
100 | 99 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ 𝑋 = 0)) |
101 | 98 | simprd 495 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))) |
102 | 101 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) |
103 | 100, 102 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝜑 → (((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) ↔ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))) |
104 | 95, 103 | syl5ib 243 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))) |
105 | 104 | con3d 152 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) =
0))) |
106 | | eldifi 4065 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (ℂ ∖ {0})
→ 𝑢 ∈
ℂ) |
107 | 106 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈
ℂ) |
108 | 54 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈
ℂ) |
109 | | eldifsni 4728 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (ℂ ∖ {0})
→ 𝑢 ≠
0) |
110 | 109 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0) |
111 | 108, 107,
110 | divcld 11734 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ) |
112 | 62 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈
ℂ) |
113 | 107, 111,
112 | subaddd 11333 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)) |
114 | | eqcom 2746 |
. . . . . . . . . . . 12
⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋) |
115 | | eqcom 2746 |
. . . . . . . . . . . 12
⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢) |
116 | 113, 114,
115 | 3bitr4g 313 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋))) |
117 | 107 | sqcld 13843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈
ℂ) |
118 | 112, 107 | mulcld 10979 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ) |
119 | 118, 108 | addcld 10978 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ) |
120 | 117, 119 | subeq0ad 11325 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(((𝑢↑2) −
((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀))) |
121 | 107 | sqvald 13842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢)) |
122 | 111, 112,
107 | adddird 10984 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢))) |
123 | 108, 107,
110 | divcan1d 11735 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀) |
124 | 123 | oveq1d 7283 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢))) |
125 | 108, 118 | addcomd 11160 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀)) |
126 | 122, 124,
125 | 3eqtrrd 2784 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)) |
127 | 121, 126 | eqeq12d 2755 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))) |
128 | 111, 112 | addcld 10978 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ) |
129 | 107, 128,
107, 110 | mulcan2d 11592 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋))) |
130 | 120, 127,
129 | 3bitrd 304 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(((𝑢↑2) −
((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋))) |
131 | | 1cnd 10954 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1
∈ ℂ) |
132 | | ax-1ne0 10924 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
0 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠
0) |
134 | 62 | negcld 11302 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -𝑋 ∈ ℂ) |
135 | 134 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈
ℂ) |
136 | 54 | negcld 11302 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -𝑀 ∈ ℂ) |
137 | 136 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈
ℂ) |
138 | | sqneg 13817 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2)) |
139 | 112, 138 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2)) |
140 | 137 | mulid2d 10977 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1
· -𝑀) = -𝑀) |
141 | 140 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4
· (1 · -𝑀)) =
(4 · -𝑀)) |
142 | | mulneg2 11395 |
. . . . . . . . . . . . . . . . 17
⊢ ((4
∈ ℂ ∧ 𝑀
∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀)) |
143 | 56, 108, 142 | sylancr 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4
· -𝑀) = -(4 ·
𝑀)) |
144 | 141, 143 | eqtrd 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4
· (1 · -𝑀)) =
-(4 · 𝑀)) |
145 | 139, 144 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
((-𝑋↑2) − (4
· (1 · -𝑀)))
= ((𝑋↑2) − -(4
· 𝑀))) |
146 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋↑2) ∈
ℂ) |
147 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4
· 𝑀) ∈
ℂ) |
148 | 146, 147 | subnegd 11322 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) − -(4 ·
𝑀)) = ((𝑋↑2) + (4 · 𝑀))) |
149 | 145, 148 | eqtr2d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) + (4 · 𝑀)) = ((-𝑋↑2) − (4 · (1 ·
-𝑀)))) |
150 | 131, 133,
135, 137, 107, 149 | quad 25971 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1
· (𝑢↑2)) +
((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))))) |
151 | 117 | mulid2d 10977 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1
· (𝑢↑2)) =
(𝑢↑2)) |
152 | 112, 107 | mulneg1d 11411 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢)) |
153 | 152 | oveq1d 7283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀)) |
154 | 118, 108 | negdid 11328 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
-((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀)) |
155 | 153, 154 | eqtr4d 2782 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀)) |
156 | 151, 155 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1
· (𝑢↑2)) +
((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀))) |
157 | 117, 119 | negsubd 11321 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀))) |
158 | 156, 157 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1
· (𝑢↑2)) +
((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀))) |
159 | 158 | eqeq1d 2741 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1
· (𝑢↑2)) +
((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0)) |
160 | 112 | negnegd 11306 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋) |
161 | 160 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(--𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) =
(𝑋 + (√‘((𝑋↑2) + (4 · 𝑀))))) |
162 | | 2t1e2 12119 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 1) = 2 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2
· 1) = 2) |
164 | 161, 163 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
((--𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / (2
· 1)) = ((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) /
2)) |
165 | 164 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))) |
166 | 160 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(--𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) =
(𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀))))) |
167 | 166, 163 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
((--𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / (2
· 1)) = ((𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) /
2)) |
168 | 167 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))) |
169 | 165, 168 | orbi12d 915 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))) |
170 | 150, 159,
169 | 3bitr3d 308 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) →
(((𝑢↑2) −
((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))) |
171 | 116, 130,
170 | 3bitr2d 306 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))) |
172 | 171 | rexbidva 3226 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))) |
173 | | r19.43 3279 |
. . . . . . . . 9
⊢
(∃𝑢 ∈
(ℂ ∖ {0})(𝑢 =
((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (∃𝑢 ∈ (ℂ ∖
{0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))) |
174 | 172, 173 | bitrdi 286 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))) |
175 | | risset 3195 |
. . . . . . . . . . 11
⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ
∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) |
176 | 62, 96 | addcld 10978 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ) |
177 | 176 | halfcld 12201 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ) |
178 | | eldifsn 4725 |
. . . . . . . . . . . . 13
⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ
∖ {0}) ↔ (((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
∈ ℂ ∧ ((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
≠ 0)) |
179 | 178 | baib 535 |
. . . . . . . . . . . 12
⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ →
(((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
∈ (ℂ ∖ {0}) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)) |
180 | 177, 179 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0})
↔ ((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
≠ 0)) |
181 | 175, 180 | bitr3id 284 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)) |
182 | | risset 3195 |
. . . . . . . . . . 11
⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ
∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) |
183 | 62, 96 | subcld 11315 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ) |
184 | 183 | halfcld 12201 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ) |
185 | | eldifsn 4725 |
. . . . . . . . . . . . 13
⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ
∖ {0}) ↔ (((𝑋
− (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠
0)) |
186 | 185 | baib 535 |
. . . . . . . . . . . 12
⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ →
(((𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
∈ (ℂ ∖ {0}) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)) |
187 | 184, 186 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0})
↔ ((𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2)
≠ 0)) |
188 | 182, 187 | bitr3id 284 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)) |
189 | 181, 188 | orbi12d 915 |
. . . . . . . . 9
⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖
{0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))) |
190 | | neorian 3040 |
. . . . . . . . 9
⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0) ↔ ¬
(((𝑋 +
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2) =
0 ∧ ((𝑋 −
(√‘((𝑋↑2)
+ (4 · 𝑀)))) / 2) =
0)) |
191 | 189, 190 | bitrdi 286 |
. . . . . . . 8
⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖
{0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))) |
192 | 174, 191 | bitrd 278 |
. . . . . . 7
⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))) |
193 | 105, 192 | sylibrd 258 |
. . . . . 6
⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ∃𝑢 ∈ (ℂ ∖
{0})𝑋 = (𝑢 − (𝑀 / 𝑢)))) |
194 | 193 | imp 406 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ∃𝑢 ∈ (ℂ ∖
{0})𝑋 = (𝑢 − (𝑀 / 𝑢))) |
195 | 90, 194 | syldan 590 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢))) |
196 | 20 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ) |
197 | 34 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ) |
198 | 62 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ) |
199 | 3 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ) |
200 | 10 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁)) |
201 | 12 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ) |
202 | 14 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3))) |
203 | 48 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3)) |
204 | 16 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2)) |
205 | 1 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0) |
206 | 106 | ad2antrl 724 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ) |
207 | 109 | ad2antrl 724 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0) |
208 | | simprr 769 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢))) |
209 | | simplr 765 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) |
210 | 196, 197,
198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209 | dcubic2 25975 |
. . . 4
⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) |
211 | 195, 210 | rexlimddv 3221 |
. . 3
⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) |
212 | 211 | ex 412 |
. 2
⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))) |
213 | 20 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ) |
214 | 34 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ) |
215 | 62 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ) |
216 | | simplr 765 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ) |
217 | 3 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ) |
218 | 216, 217 | mulcld 10979 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ) |
219 | | 3nn0 12234 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
220 | 219 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈
ℕ0) |
221 | 216, 217,
220 | mulexpd 13860 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3))) |
222 | | simprl 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1) |
223 | 222 | oveq1d 7283 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3))) |
224 | | expcl 13781 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑇↑3) ∈ ℂ) |
225 | 3, 219, 224 | sylancl 585 |
. . . . . . . 8
⊢ (𝜑 → (𝑇↑3) ∈ ℂ) |
226 | 225 | mulid2d 10977 |
. . . . . . 7
⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3)) |
227 | 226, 10 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁)) |
228 | 227 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁)) |
229 | 221, 223,
228 | 3eqtrd 2783 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁)) |
230 | 12 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ) |
231 | 14 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3))) |
232 | 48 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3)) |
233 | 16 | ad2antrr 722 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2)) |
234 | 132 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0) |
235 | 222, 234 | eqnetrd 3012 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0) |
236 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3)) |
237 | 236, 28 | eqtrdi 2795 |
. . . . . . 7
⊢ (𝑟 = 0 → (𝑟↑3) = 0) |
238 | 237 | necon3i 2977 |
. . . . . 6
⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0) |
239 | 235, 238 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0) |
240 | 1 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0) |
241 | 216, 217,
239, 240 | mulne0d 11610 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0) |
242 | | simprr 769 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))) |
243 | 213, 214,
215, 218, 229, 230, 231, 232, 233, 241, 242 | dcubic1 25976 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) |
244 | 243 | rexlimdva2 3217 |
. 2
⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)) |
245 | 212, 244 | impbid 211 |
1
⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))) |