Metamath Proof Explorer


Theorem cubic

Description: The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp to convert the existential quantifier to a triple disjunction. This is Metamath 100 proof #37. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses cubic.r R = 1 - 1 + i 3 2 - 1 - i 3 2
cubic.a φ A
cubic.z φ A 0
cubic.b φ B
cubic.c φ C
cubic.d φ D
cubic.x φ X
cubic.t φ T = N + G 2 1 3
cubic.g φ G = N 2 4 M 3
cubic.m φ M = B 2 3 A C
cubic.n φ N = 2 B 3 - 9 A B C + 27 A 2 D
cubic.0 φ M 0
Assertion cubic φ A X 3 + B X 2 + C X + D = 0 r R X = B + r T + M r T 3 A

Proof

Step Hyp Ref Expression
1 cubic.r R = 1 - 1 + i 3 2 - 1 - i 3 2
2 cubic.a φ A
3 cubic.z φ A 0
4 cubic.b φ B
5 cubic.c φ C
6 cubic.d φ D
7 cubic.x φ X
8 cubic.t φ T = N + G 2 1 3
9 cubic.g φ G = N 2 4 M 3
10 cubic.m φ M = B 2 3 A C
11 cubic.n φ N = 2 B 3 - 9 A B C + 27 A 2 D
12 cubic.0 φ M 0
13 2cn 2
14 3nn0 3 0
15 expcl B 3 0 B 3
16 4 14 15 sylancl φ B 3
17 mulcl 2 B 3 2 B 3
18 13 16 17 sylancr φ 2 B 3
19 9cn 9
20 mulcl 9 A 9 A
21 19 2 20 sylancr φ 9 A
22 4 5 mulcld φ B C
23 21 22 mulcld φ 9 A B C
24 18 23 subcld φ 2 B 3 9 A B C
25 2nn0 2 0
26 7nn 7
27 25 26 decnncl 27
28 27 nncni 27
29 2 sqcld φ A 2
30 29 6 mulcld φ A 2 D
31 mulcl 27 A 2 D 27 A 2 D
32 28 30 31 sylancr φ 27 A 2 D
33 24 32 addcld φ 2 B 3 - 9 A B C + 27 A 2 D
34 11 33 eqeltrd φ N
35 34 sqcld φ N 2
36 4cn 4
37 4 sqcld φ B 2
38 3cn 3
39 2 5 mulcld φ A C
40 mulcl 3 A C 3 A C
41 38 39 40 sylancr φ 3 A C
42 37 41 subcld φ B 2 3 A C
43 10 42 eqeltrd φ M
44 expcl M 3 0 M 3
45 43 14 44 sylancl φ M 3
46 mulcl 4 M 3 4 M 3
47 36 45 46 sylancr φ 4 M 3
48 35 47 subcld φ N 2 4 M 3
49 9 48 eqeltrd φ G
50 49 sqrtcld φ G
51 34 50 addcld φ N + G
52 51 halfcld φ N + G 2
53 3ne0 3 0
54 38 53 reccli 1 3
55 cxpcl N + G 2 1 3 N + G 2 1 3
56 52 54 55 sylancl φ N + G 2 1 3
57 8 56 eqeltrd φ T
58 8 oveq1d φ T 3 = N + G 2 1 3 3
59 3nn 3
60 cxproot N + G 2 3 N + G 2 1 3 3 = N + G 2
61 52 59 60 sylancl φ N + G 2 1 3 3 = N + G 2
62 58 61 eqtrd φ T 3 = N + G 2
63 49 sqsqrtd φ G 2 = G
64 63 9 eqtrd φ G 2 = N 2 4 M 3
65 13 a1i φ 2
66 36 a1i φ 4
67 4ne0 4 0
68 67 a1i φ 4 0
69 3z 3
70 69 a1i φ 3
71 43 12 70 expne0d φ M 3 0
72 66 45 68 71 mulne0d φ 4 M 3 0
73 64 oveq2d φ N 2 G 2 = N 2 N 2 4 M 3
74 subsq N G N 2 G 2 = N + G N G
75 34 50 74 syl2anc φ N 2 G 2 = N + G N G
76 35 47 nncand φ N 2 N 2 4 M 3 = 4 M 3
77 73 75 76 3eqtr3d φ N + G N G = 4 M 3
78 34 50 subcld φ N G
79 78 mul02d φ 0 N G = 0
80 72 77 79 3netr4d φ N + G N G 0 N G
81 oveq1 N + G = 0 N + G N G = 0 N G
82 81 necon3i N + G N G 0 N G N + G 0
83 80 82 syl φ N + G 0
84 2ne0 2 0
85 84 a1i φ 2 0
86 51 65 83 85 divne0d φ N + G 2 0
87 54 a1i φ 1 3
88 52 86 87 cxpne0d φ N + G 2 1 3 0
89 8 88 eqnetrd φ T 0
90 2 3 4 5 6 7 57 62 50 64 10 11 89 cubic2 φ A X 3 + B X 2 + C X + D = 0 r r 3 = 1 X = B + r T + M r T 3 A
91 1 1cubr r R r r 3 = 1
92 91 anbi1i r R X = B + r T + M r T 3 A r r 3 = 1 X = B + r T + M r T 3 A
93 anass r r 3 = 1 X = B + r T + M r T 3 A r r 3 = 1 X = B + r T + M r T 3 A
94 92 93 bitri r R X = B + r T + M r T 3 A r r 3 = 1 X = B + r T + M r T 3 A
95 94 rexbii2 r R X = B + r T + M r T 3 A r r 3 = 1 X = B + r T + M r T 3 A
96 90 95 bitr4di φ A X 3 + B X 2 + C X + D = 0 r R X = B + r T + M r T 3 A