dcubic

Description: Solutions to the depressed cubic, a special case of cubic . (The definitions of M , N , G , T here differ from mcubic by scale factors of -u 9 , 5 4 , 5 4 and -u 2 7 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	dcubic.c	$⊢ φ \to P \in ℂ$
	dcubic.d	$⊢ φ \to Q \in ℂ$
	dcubic.x	$⊢ φ \to X \in ℂ$
	dcubic.t	$⊢ φ \to T \in ℂ$
	dcubic.3	$⊢ φ \to T^{3} = G - N$
	dcubic.g	$⊢ φ \to G \in ℂ$
	dcubic.2	$⊢ φ \to G^{2} = N^{2} + M^{3}$
	dcubic.m	$⊢ φ \to M = \frac{P}{3}$
	dcubic.n	$⊢ φ \to N = \frac{Q}{2}$
	dcubic.0	$⊢ φ \to T \neq 0$
Assertion	dcubic	$⊢ φ \to (X^{3} + P X + Q = 0 \leftrightarrow \exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T})))$

Proof

Step	Hyp	Ref	Expression
1		dcubic.c	$⊢ φ \to P \in ℂ$
2		dcubic.d	$⊢ φ \to Q \in ℂ$
3		dcubic.x	$⊢ φ \to X \in ℂ$
4		dcubic.t	$⊢ φ \to T \in ℂ$
5		dcubic.3	$⊢ φ \to T^{3} = G - N$
6		dcubic.g	$⊢ φ \to G \in ℂ$
7		dcubic.2	$⊢ φ \to G^{2} = N^{2} + M^{3}$
8		dcubic.m	$⊢ φ \to M = \frac{P}{3}$
9		dcubic.n	$⊢ φ \to N = \frac{Q}{2}$
10		dcubic.0	$⊢ φ \to T \neq 0$
11	10	adantr	$⊢ (φ \land X^{3} + P X + Q = 0) \to T \neq 0$
12	4	adantr	$⊢ (φ \land X^{3} + P X + Q = 0) \to T \in ℂ$
13		3z	$⊢ 3 \in ℤ$
14		expne0i	$⊢ (T \in ℂ \land T \neq 0 \land 3 \in ℤ) \to T^{3} \neq 0$
15	13 14	mp3an3	$⊢ (T \in ℂ \land T \neq 0) \to T^{3} \neq 0$
16	15	ex	$⊢ T \in ℂ \to (T \neq 0 \to T^{3} \neq 0)$
17	12 16	syl	$⊢ (φ \land X^{3} + P X + Q = 0) \to (T \neq 0 \to T^{3} \neq 0)$
18	5	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to T^{3} = G - N$
19	6	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G \in ℂ$
20	7	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G^{2} = N^{2} + M^{3}$
21	9	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to N = \frac{Q}{2}$
22		simprl	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X = 0$
23	22	oveq2d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X = P \cdot 0$
24	1	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P \in ℂ$
25	24	mul01d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P \cdot 0 = 0$
26	23 25	eqtrd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X = 0$
27	26	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X + Q = 0 + Q$
28	22	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{3} = 0^{3}$
29		3nn	$⊢ 3 \in ℕ$
30		0exp	$⊢ 3 \in ℕ \to 0^{3} = 0$
31	29 30	ax-mp	$⊢ 0^{3} = 0$
32	28 31	eqtrdi	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{3} = 0$
33	32	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{3} + P X + Q = 0 + P X + Q$
34		simplr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{3} + P X + Q = 0$
35		0cnd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 0 \in ℂ$
36	26 35	eqeltrd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X \in ℂ$
37	2	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to Q \in ℂ$
38	36 37	addcld	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X + Q \in ℂ$
39	38	addlidd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 0 + P X + Q = P X + Q$
40	33 34 39	3eqtr3rd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to P X + Q = 0$
41	37	addlidd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 0 + Q = Q$
42	27 40 41	3eqtr3rd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to Q = 0$
43	42	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to \frac{Q}{2} = \frac{0}{2}$
44		2cn	$⊢ 2 \in ℂ$
45		2ne0	$⊢ 2 \neq 0$
46	44 45	div0i	$⊢ \frac{0}{2} = 0$
47	43 46	eqtrdi	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to \frac{Q}{2} = 0$
48	21 47	eqtrd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to N = 0$
49	48	sq0id	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to N^{2} = 0$
50		3cn	$⊢ 3 \in ℂ$
51	50	a1i	$⊢ φ \to 3 \in ℂ$
52		3ne0	$⊢ 3 \neq 0$
53	52	a1i	$⊢ φ \to 3 \neq 0$
54	1 51 53	divcld	$⊢ φ \to \frac{P}{3} \in ℂ$
55	8 54	eqeltrd	$⊢ φ \to M \in ℂ$
56	55	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to M \in ℂ$
57		4cn	$⊢ 4 \in ℂ$
58	57	a1i	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 4 \in ℂ$
59		4ne0	$⊢ 4 \neq 0$
60	59	a1i	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 4 \neq 0$
61	22	sq0id	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{2} = 0$
62	61	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{2} + 4 \cdot M = 0 + 4 \cdot M$
63	3	sqcld	$⊢ φ \to X^{2} \in ℂ$
64		mulcl	$⊢ (4 \in ℂ \land M \in ℂ) \to 4 \cdot M \in ℂ$
65	57 55 64	sylancr	$⊢ φ \to 4 \cdot M \in ℂ$
66	63 65	addcld	$⊢ φ \to X^{2} + 4 \cdot M \in ℂ$
67	66	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{2} + 4 \cdot M \in ℂ$
68		simprr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to \sqrt{X^{2} + 4 \cdot M} = 0$
69	67 68	sqr00d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to X^{2} + 4 \cdot M = 0$
70	65	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 4 \cdot M \in ℂ$
71	70	addlidd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 0 + 4 \cdot M = 4 \cdot M$
72	62 69 71	3eqtr3rd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 4 \cdot M = 0$
73	57	mul01i	$⊢ 4 \cdot 0 = 0$
74	72 73	eqtr4di	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to 4 \cdot M = 4 \cdot 0$
75	56 35 58 60 74	mulcanad	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to M = 0$
76	75	oveq1d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to M^{3} = 0^{3}$
77	76 31	eqtrdi	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to M^{3} = 0$
78	49 77	oveq12d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to N^{2} + M^{3} = 0 + 0$
79		00id	$⊢ 0 + 0 = 0$
80	78 79	eqtrdi	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to N^{2} + M^{3} = 0$
81	20 80	eqtrd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G^{2} = 0$
82	19 81	sqeq0d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G = 0$
83	82 48	oveq12d	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G - N = 0 - 0$
84		0m0e0	$⊢ 0 - 0 = 0$
85	83 84	eqtrdi	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to G - N = 0$
86	18 85	eqtrd	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to T^{3} = 0$
87	86	ex	$⊢ (φ \land X^{3} + P X + Q = 0) \to ((X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0) \to T^{3} = 0)$
88	87	necon3ad	$⊢ (φ \land X^{3} + P X + Q = 0) \to (T^{3} \neq 0 \to \neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0))$
89	17 88	syld	$⊢ (φ \land X^{3} + P X + Q = 0) \to (T \neq 0 \to \neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0))$
90	11 89	mpd	$⊢ (φ \land X^{3} + P X + Q = 0) \to \neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)$
91		oveq12	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 + 0$
92	91 79	eqtrdi	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0$
93		oveq12	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 - 0$
94	93 84	eqtrdi	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0$
95	92 94	jca	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 \land (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0)$
96	66	sqrtcld	$⊢ φ \to \sqrt{X^{2} + 4 \cdot M} \in ℂ$
97		halfaddsub	$⊢ (X \in ℂ \land \sqrt{X^{2} + 4 \cdot M} \in ℂ) \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = X \land (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = \sqrt{X^{2} + 4 \cdot M})$
98	3 96 97	syl2anc	$⊢ φ \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = X \land (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = \sqrt{X^{2} + 4 \cdot M})$
99	98	simpld	$⊢ φ \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = X$
100	99	eqeq1d	$⊢ φ \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 \leftrightarrow X = 0)$
101	98	simprd	$⊢ φ \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = \sqrt{X^{2} + 4 \cdot M}$
102	101	eqeq1d	$⊢ φ \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 \leftrightarrow \sqrt{X^{2} + 4 \cdot M} = 0)$
103	100 102	anbi12d	$⊢ φ \to (((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) + (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0 \land (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}) - (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) = 0) \leftrightarrow (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0))$
104	95 103	imbitrid	$⊢ φ \to ((\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0) \to (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0))$
105	104	con3d	$⊢ φ \to (\neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0) \to \neg (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0))$
106		eldifi	$⊢ u \in (ℂ ∖ \{0\}) \to u \in ℂ$
107	106	adantl	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to u \in ℂ$
108	55	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to M \in ℂ$
109		eldifsni	$⊢ u \in (ℂ ∖ \{0\}) \to u \neq 0$
110	109	adantl	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to u \neq 0$
111	108 107 110	divcld	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to \frac{M}{u} \in ℂ$
112	3	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X \in ℂ$
113	107 111 112	subaddd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u - (\frac{M}{u}) = X \leftrightarrow (\frac{M}{u}) + X = u)$
114		eqcom	$⊢ X = u - (\frac{M}{u}) \leftrightarrow u - (\frac{M}{u}) = X$
115		eqcom	$⊢ u = (\frac{M}{u}) + X \leftrightarrow (\frac{M}{u}) + X = u$
116	113 114 115	3bitr4g	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (X = u - (\frac{M}{u}) \leftrightarrow u = (\frac{M}{u}) + X)$
117	107	sqcld	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to u^{2} \in ℂ$
118	112 107	mulcld	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X u \in ℂ$
119	118 108	addcld	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X u + M \in ℂ$
120	117 119	subeq0ad	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u^{2} - (X u + M) = 0 \leftrightarrow u^{2} = X u + M)$
121	107	sqvald	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to u^{2} = u u$
122	111 112 107	adddird	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to ((\frac{M}{u}) + X) u = (\frac{M}{u}) u + X u$
123	108 107 110	divcan1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (\frac{M}{u}) u = M$
124	123	oveq1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (\frac{M}{u}) u + X u = M + X u$
125	108 118	addcomd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to M + X u = X u + M$
126	122 124 125	3eqtrrd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X u + M = ((\frac{M}{u}) + X) u$
127	121 126	eqeq12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u^{2} = X u + M \leftrightarrow u u = ((\frac{M}{u}) + X) u)$
128	111 112	addcld	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (\frac{M}{u}) + X \in ℂ$
129	107 128 107 110	mulcan2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u u = ((\frac{M}{u}) + X) u \leftrightarrow u = (\frac{M}{u}) + X)$
130	120 127 129	3bitrd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u^{2} - (X u + M) = 0 \leftrightarrow u = (\frac{M}{u}) + X)$
131		1cnd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 \in ℂ$
132		ax-1ne0	$⊢ 1 \neq 0$
133	132	a1i	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 \neq 0$
134	3	negcld	$⊢ φ \to - X \in ℂ$
135	134	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - X \in ℂ$
136	55	negcld	$⊢ φ \to - M \in ℂ$
137	136	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - M \in ℂ$
138		sqneg	$⊢ X \in ℂ \to {(- X)}^{2} = X^{2}$
139	112 138	syl	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to {(- X)}^{2} = X^{2}$
140	137	mullidd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 -M = - M$
141	140	oveq2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 4 1 -M = 4 -M$
142		mulneg2	$⊢ (4 \in ℂ \land M \in ℂ) \to 4 -M = - 4 \cdot M$
143	57 108 142	sylancr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 4 -M = - 4 \cdot M$
144	141 143	eqtrd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 4 1 -M = - 4 \cdot M$
145	139 144	oveq12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to {(- X)}^{2} - 4 1 -M = X^{2} - (- 4 \cdot M)$
146	63	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X^{2} \in ℂ$
147	65	adantr	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 4 \cdot M \in ℂ$
148	146 147	subnegd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X^{2} - (- 4 \cdot M) = X^{2} + 4 \cdot M$
149	145 148	eqtr2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to X^{2} + 4 \cdot M = {(- X)}^{2} - 4 1 -M$
150	131 133 135 137 107 149	quad	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (1 u^{2} + (- X) u + -M = 0 \leftrightarrow (u = \frac{- (- X) + \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} \lor u = \frac{- (- X) - \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1}))$
151	117	mullidd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 u^{2} = u^{2}$
152	112 107	mulneg1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (- X) u = - X u$
153	152	oveq1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (- X) u + -M = - X u + -M$
154	118 108	negdid	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - (X u + M) = - X u + -M$
155	153 154	eqtr4d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (- X) u + -M = - (X u + M)$
156	151 155	oveq12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 u^{2} + (- X) u + -M = u^{2} + (- (X u + M))$
157	117 119	negsubd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to u^{2} + (- (X u + M)) = u^{2} - (X u + M)$
158	156 157	eqtrd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 1 u^{2} + (- X) u + -M = u^{2} - (X u + M)$
159	158	eqeq1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (1 u^{2} + (- X) u + -M = 0 \leftrightarrow u^{2} - (X u + M) = 0)$
160	112	negnegd	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - (- X) = X$
161	160	oveq1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - (- X) + \sqrt{X^{2} + 4 \cdot M} = X + \sqrt{X^{2} + 4 \cdot M}$
162		2t1e2	$⊢ 2 \cdot 1 = 2$
163	162	a1i	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to 2 \cdot 1 = 2$
164	161 163	oveq12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to \frac{- (- X) + \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}$
165	164	eqeq2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u = \frac{- (- X) + \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} \leftrightarrow u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2})$
166	160	oveq1d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to - (- X) - \sqrt{X^{2} + 4 \cdot M} = X - \sqrt{X^{2} + 4 \cdot M}$
167	166 163	oveq12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to \frac{- (- X) - \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}$
168	167	eqeq2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u = \frac{- (- X) - \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} \leftrightarrow u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2})$
169	165 168	orbi12d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to ((u = \frac{- (- X) + \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1} \lor u = \frac{- (- X) - \sqrt{X^{2} + 4 \cdot M}}{2 \cdot 1}) \leftrightarrow (u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}))$
170	150 159 169	3bitr3d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (u^{2} - (X u + M) = 0 \leftrightarrow (u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}))$
171	116 130 170	3bitr2d	$⊢ (φ \land u \in (ℂ ∖ \{0\})) \to (X = u - (\frac{M}{u}) \leftrightarrow (u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}))$
172	171	rexbidva	$⊢ φ \to (\exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u}) \leftrightarrow \exists u \in (ℂ ∖ \{0\}) (u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}))$
173		r19.43	$⊢ \exists u \in (ℂ ∖ \{0\}) (u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) \leftrightarrow (\exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor \exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2})$
174	172 173	bitrdi	$⊢ φ \to (\exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u}) \leftrightarrow (\exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor \exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}))$
175		risset	$⊢ \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2}$
176	3 96	addcld	$⊢ φ \to X + \sqrt{X^{2} + 4 \cdot M} \in ℂ$
177	176	halfcld	$⊢ φ \to \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ$
178		eldifsn	$⊢ \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ \land \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
179	178	baib	$⊢ \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
180	177 179	syl	$⊢ φ \to (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
181	175 180	bitr3id	$⊢ φ \to (\exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \leftrightarrow \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
182		risset	$⊢ \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}$
183	3 96	subcld	$⊢ φ \to X - \sqrt{X^{2} + 4 \cdot M} \in ℂ$
184	183	halfcld	$⊢ φ \to \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ$
185		eldifsn	$⊢ \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
186	185	baib	$⊢ \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in ℂ \to (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
187	184 186	syl	$⊢ φ \to (\frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \in (ℂ ∖ \{0\}) \leftrightarrow \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
188	182 187	bitr3id	$⊢ φ \to (\exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \leftrightarrow \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0)$
189	181 188	orbi12d	$⊢ φ \to ((\exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor \exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) \leftrightarrow (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0 \lor \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0))$
190		neorian	$⊢ (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0 \lor \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} \neq 0) \leftrightarrow \neg (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0)$
191	189 190	bitrdi	$⊢ φ \to ((\exists u \in (ℂ ∖ \{0\}) u = \frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} \lor \exists u \in (ℂ ∖ \{0\}) u = \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2}) \leftrightarrow \neg (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0))$
192	174 191	bitrd	$⊢ φ \to (\exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u}) \leftrightarrow \neg (\frac{X + \sqrt{X^{2} + 4 \cdot M}}{2} = 0 \land \frac{X - \sqrt{X^{2} + 4 \cdot M}}{2} = 0))$
193	105 192	sylibrd	$⊢ φ \to (\neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0) \to \exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u}))$
194	193	imp	$⊢ (φ \land \neg (X = 0 \land \sqrt{X^{2} + 4 \cdot M} = 0)) \to \exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u})$
195	90 194	syldan	$⊢ (φ \land X^{3} + P X + Q = 0) \to \exists u \in (ℂ ∖ \{0\}) X = u - (\frac{M}{u})$
196	1	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to P \in ℂ$
197	2	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to Q \in ℂ$
198	3	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to X \in ℂ$
199	4	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to T \in ℂ$
200	5	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to T^{3} = G - N$
201	6	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to G \in ℂ$
202	7	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to G^{2} = N^{2} + M^{3}$
203	8	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to M = \frac{P}{3}$
204	9	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to N = \frac{Q}{2}$
205	10	ad2antrr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to T \neq 0$
206	106	ad2antrl	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to u \in ℂ$
207	109	ad2antrl	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to u \neq 0$
208		simprr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to X = u - (\frac{M}{u})$
209		simplr	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to X^{3} + P X + Q = 0$
210	196 197 198 199 200 201 202 203 204 205 206 207 208 209	dcubic2	$⊢ ((φ \land X^{3} + P X + Q = 0) \land (u \in (ℂ ∖ \{0\}) \land X = u - (\frac{M}{u}))) \to \exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T}))$
211	195 210	rexlimddv	$⊢ (φ \land X^{3} + P X + Q = 0) \to \exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T}))$
212	211	ex	$⊢ φ \to (X^{3} + P X + Q = 0 \to \exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T})))$
213	1	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to P \in ℂ$
214	2	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to Q \in ℂ$
215	3	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to X \in ℂ$
216		simplr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r \in ℂ$
217	4	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to T \in ℂ$
218	216 217	mulcld	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r T \in ℂ$
219		3nn0	$⊢ 3 \in ℕ_{0}$
220	219	a1i	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to 3 \in ℕ_{0}$
221	216 217 220	mulexpd	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to {r T}^{3} = r^{3} T^{3}$
222		simprl	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r^{3} = 1$
223	222	oveq1d	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r^{3} T^{3} = 1 T^{3}$
224		expcl	$⊢ (T \in ℂ \land 3 \in ℕ_{0}) \to T^{3} \in ℂ$
225	4 219 224	sylancl	$⊢ φ \to T^{3} \in ℂ$
226	225	mullidd	$⊢ φ \to 1 T^{3} = T^{3}$
227	226 5	eqtrd	$⊢ φ \to 1 T^{3} = G - N$
228	227	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to 1 T^{3} = G - N$
229	221 223 228	3eqtrd	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to {r T}^{3} = G - N$
230	6	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to G \in ℂ$
231	7	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to G^{2} = N^{2} + M^{3}$
232	8	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to M = \frac{P}{3}$
233	9	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to N = \frac{Q}{2}$
234	132	a1i	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to 1 \neq 0$
235	222 234	eqnetrd	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r^{3} \neq 0$
236		oveq1	$⊢ r = 0 \to r^{3} = 0^{3}$
237	236 31	eqtrdi	$⊢ r = 0 \to r^{3} = 0$
238	237	necon3i	$⊢ r^{3} \neq 0 \to r \neq 0$
239	235 238	syl	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r \neq 0$
240	10	ad2antrr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to T \neq 0$
241	216 217 239 240	mulne0d	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to r T \neq 0$
242		simprr	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to X = r T - (\frac{M}{r T})$
243	213 214 215 218 229 230 231 232 233 241 242	dcubic1	$⊢ ((φ \land r \in ℂ) \land (r^{3} = 1 \land X = r T - (\frac{M}{r T}))) \to X^{3} + P X + Q = 0$
244	243	rexlimdva2	$⊢ φ \to (\exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T})) \to X^{3} + P X + Q = 0)$
245	212 244	impbid	$⊢ φ \to (X^{3} + P X + Q = 0 \leftrightarrow \exists r \in ℂ (r^{3} = 1 \land X = r T - (\frac{M}{r T})))$

Metamath Proof Explorer

Theorem dcubic

Proof