dcubic1lem

Description: Lemma for dcubic1 and dcubic2 : simplify the cubic equation under the substitution X = U - M / U . (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$
	dcubic2.u	$⊢ φ \to U \in ℂ$
	dcubic2.z	$⊢ φ \to U \neq 0$
	dcubic2.2	$⊢ φ \to X = U - (\frac{M}{U})$
Assertion	dcubic1lem	$⊢ φ \to (X^{3} + P X + Q = 0 \leftrightarrow {(U^{3})}^{2} + Q U^{3} - M^{3} = 0)$

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		dcubic2.u	$⊢ φ \to U \in ℂ$
12		dcubic2.z	$⊢ φ \to U \neq 0$
13		dcubic2.2	$⊢ φ \to X = U - (\frac{M}{U})$
14		3nn0	$⊢ 3 \in ℕ_{0}$
15		expcl	$⊢ (U \in ℂ \land 3 \in ℕ_{0}) \to U^{3} \in ℂ$
16	11 14 15	sylancl	$⊢ φ \to U^{3} \in ℂ$
17	16	sqvald	$⊢ φ \to {(U^{3})}^{2} = U^{3} U^{3}$
18	17	oveq1d	$⊢ φ \to \frac{{(U^{3})}^{2}}{U^{3}} = \frac{U^{3} U^{3}}{U^{3}}$
19		3z	$⊢ 3 \in ℤ$
20	19	a1i	$⊢ φ \to 3 \in ℤ$
21	11 12 20	expne0d	$⊢ φ \to U^{3} \neq 0$
22	16 16 21	divcan4d	$⊢ φ \to \frac{U^{3} U^{3}}{U^{3}} = U^{3}$
23	18 22	eqtr2d	$⊢ φ \to U^{3} = \frac{{(U^{3})}^{2}}{U^{3}}$
24		3cn	$⊢ 3 \in ℂ$
25	24	a1i	$⊢ φ \to 3 \in ℂ$
26		3ne0	$⊢ 3 \neq 0$
27	26	a1i	$⊢ φ \to 3 \neq 0$
28	1 25 27	divcld	$⊢ φ \to \frac{P}{3} \in ℂ$
29	8 28	eqeltrd	$⊢ φ \to M \in ℂ$
30		expcl	$⊢ (M \in ℂ \land 3 \in ℕ_{0}) \to M^{3} \in ℂ$
31	29 14 30	sylancl	$⊢ φ \to M^{3} \in ℂ$
32	31 16 21	divcld	$⊢ φ \to \frac{M^{3}}{U^{3}} \in ℂ$
33	2 32	negsubd	$⊢ φ \to Q + (- \frac{M^{3}}{U^{3}}) = Q - (\frac{M^{3}}{U^{3}})$
34	2 16 21	divcan4d	$⊢ φ \to \frac{Q U^{3}}{U^{3}} = Q$
35	34	oveq1d	$⊢ φ \to (\frac{Q U^{3}}{U^{3}}) - (\frac{M^{3}}{U^{3}}) = Q - (\frac{M^{3}}{U^{3}})$
36	33 35	eqtr4d	$⊢ φ \to Q + (- \frac{M^{3}}{U^{3}}) = (\frac{Q U^{3}}{U^{3}}) - (\frac{M^{3}}{U^{3}})$
37	1 3	mulcld	$⊢ φ \to P X \in ℂ$
38	37	negcld	$⊢ φ \to - P X \in ℂ$
39	32	negcld	$⊢ φ \to - \frac{M^{3}}{U^{3}} \in ℂ$
40	38 39 37 2	add42d	$⊢ φ \to (- P X) + (- \frac{M^{3}}{U^{3}}) + P X + Q = (- P X) + P X + Q + (- \frac{M^{3}}{U^{3}})$
41	1 3	mulneg2d	$⊢ φ \to P (- X) = - P X$
42	13	negeqd	$⊢ φ \to - X = - (U - (\frac{M}{U}))$
43	29 11 12	divcld	$⊢ φ \to \frac{M}{U} \in ℂ$
44	11 43	negsubdid	$⊢ φ \to - (U - (\frac{M}{U})) = - U + (\frac{M}{U})$
45	42 44	eqtrd	$⊢ φ \to - X = - U + (\frac{M}{U})$
46	45	oveq2d	$⊢ φ \to P (- X) = P (- U + (\frac{M}{U}))$
47	41 46	eqtr3d	$⊢ φ \to - P X = P (- U + (\frac{M}{U}))$
48	11	negcld	$⊢ φ \to - U \in ℂ$
49	1 48 43	adddid	$⊢ φ \to P (- U + (\frac{M}{U})) = P (- U) + P (\frac{M}{U})$
50	1 11	mulneg2d	$⊢ φ \to P (- U) = - P U$
51	50	oveq1d	$⊢ φ \to P (- U) + P (\frac{M}{U}) = - P U + P (\frac{M}{U})$
52	47 49 51	3eqtrd	$⊢ φ \to - P X = - P U + P (\frac{M}{U})$
53	52	oveq1d	$⊢ φ \to - P X + (- \frac{M^{3}}{U^{3}}) = (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
54	1 11	mulcld	$⊢ φ \to P U \in ℂ$
55	54	negcld	$⊢ φ \to - P U \in ℂ$
56	1 43	mulcld	$⊢ φ \to P (\frac{M}{U}) \in ℂ$
57	55 56 39	addassd	$⊢ φ \to (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}) = (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
58	53 57	eqtrd	$⊢ φ \to - P X + (- \frac{M^{3}}{U^{3}}) = (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
59	58	oveq1d	$⊢ φ \to (- P X) + (- \frac{M^{3}}{U^{3}}) + P X + Q = (- P U) + (P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + P X + Q$
60	38 37	addcomd	$⊢ φ \to - P X + P X = P X + (- P X)$
61	37	negidd	$⊢ φ \to P X + (- P X) = 0$
62	60 61	eqtrd	$⊢ φ \to - P X + P X = 0$
63	62	oveq1d	$⊢ φ \to (- P X) + P X + Q + (- \frac{M^{3}}{U^{3}}) = 0 + Q + (- \frac{M^{3}}{U^{3}})$
64	2 39	addcld	$⊢ φ \to Q + (- \frac{M^{3}}{U^{3}}) \in ℂ$
65	64	addid2d	$⊢ φ \to 0 + Q + (- \frac{M^{3}}{U^{3}}) = Q + (- \frac{M^{3}}{U^{3}})$
66	63 65	eqtrd	$⊢ φ \to (- P X) + P X + Q + (- \frac{M^{3}}{U^{3}}) = Q + (- \frac{M^{3}}{U^{3}})$
67	40 59 66	3eqtr3d	$⊢ φ \to (- P U) + (P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + P X + Q = Q + (- \frac{M^{3}}{U^{3}})$
68	2 16	mulcld	$⊢ φ \to Q U^{3} \in ℂ$
69	68 31 16 21	divsubdird	$⊢ φ \to \frac{Q U^{3} - M^{3}}{U^{3}} = (\frac{Q U^{3}}{U^{3}}) - (\frac{M^{3}}{U^{3}})$
70	36 67 69	3eqtr4d	$⊢ φ \to (- P U) + (P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + P X + Q = \frac{Q U^{3} - M^{3}}{U^{3}}$
71	23 70	oveq12d	$⊢ φ \to U^{3} + ((- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + (P X + Q) = (\frac{{(U^{3})}^{2}}{U^{3}}) + (\frac{Q U^{3} - M^{3}}{U^{3}})$
72	11 43	negsubd	$⊢ φ \to U + (- \frac{M}{U}) = U - (\frac{M}{U})$
73	13 72	eqtr4d	$⊢ φ \to X = U + (- \frac{M}{U})$
74	73	oveq1d	$⊢ φ \to X^{3} = {(U + (- \frac{M}{U}))}^{3}$
75	43	negcld	$⊢ φ \to - \frac{M}{U} \in ℂ$
76		binom3	$⊢ (U \in ℂ \land - \frac{M}{U} \in ℂ) \to {(U + (- \frac{M}{U}))}^{3} = U^{3} + 3 U^{2} (- \frac{M}{U}) + 3 U {(- (\frac{M}{U}))}^{2} + {(- (\frac{M}{U}))}^{3}$
77	11 75 76	syl2anc	$⊢ φ \to {(U + (- \frac{M}{U}))}^{3} = U^{3} + 3 U^{2} (- \frac{M}{U}) + 3 U {(- (\frac{M}{U}))}^{2} + {(- (\frac{M}{U}))}^{3}$
78	11	sqcld	$⊢ φ \to U^{2} \in ℂ$
79	78 43	mulneg2d	$⊢ φ \to U^{2} (- \frac{M}{U}) = - U^{2} (\frac{M}{U})$
80	78 29 11 12	div12d	$⊢ φ \to U^{2} (\frac{M}{U}) = M (\frac{U^{2}}{U})$
81	11	sqvald	$⊢ φ \to U^{2} = U U$
82	81	oveq1d	$⊢ φ \to \frac{U^{2}}{U} = \frac{U U}{U}$
83	11 11 12	divcan4d	$⊢ φ \to \frac{U U}{U} = U$
84	82 83	eqtrd	$⊢ φ \to \frac{U^{2}}{U} = U$
85	84	oveq2d	$⊢ φ \to M (\frac{U^{2}}{U}) = M U$
86	80 85	eqtrd	$⊢ φ \to U^{2} (\frac{M}{U}) = M U$
87	86	negeqd	$⊢ φ \to - U^{2} (\frac{M}{U}) = - M U$
88	79 87	eqtrd	$⊢ φ \to U^{2} (- \frac{M}{U}) = - M U$
89	88	oveq2d	$⊢ φ \to 3 U^{2} (- \frac{M}{U}) = 3 (- M U)$
90	29 11	mulcld	$⊢ φ \to M U \in ℂ$
91	25 90	mulneg2d	$⊢ φ \to 3 (- M U) = - 3 M U$
92	25 29 11	mulassd	$⊢ φ \to 3 \cdot M U = 3 M U$
93	8	oveq2d	$⊢ φ \to 3 \cdot M = 3 (\frac{P}{3})$
94	1 25 27	divcan2d	$⊢ φ \to 3 (\frac{P}{3}) = P$
95	93 94	eqtrd	$⊢ φ \to 3 \cdot M = P$
96	95	oveq1d	$⊢ φ \to 3 \cdot M U = P U$
97	92 96	eqtr3d	$⊢ φ \to 3 M U = P U$
98	97	negeqd	$⊢ φ \to - 3 M U = - P U$
99	89 91 98	3eqtrd	$⊢ φ \to 3 U^{2} (- \frac{M}{U}) = - P U$
100	99	oveq2d	$⊢ φ \to U^{3} + 3 U^{2} (- \frac{M}{U}) = U^{3} + (- P U)$
101		sqneg	$⊢ \frac{M}{U} \in ℂ \to {(- (\frac{M}{U}))}^{2} = {(\frac{M}{U})}^{2}$
102	43 101	syl	$⊢ φ \to {(- (\frac{M}{U}))}^{2} = {(\frac{M}{U})}^{2}$
103	43	sqvald	$⊢ φ \to {(\frac{M}{U})}^{2} = (\frac{M}{U}) (\frac{M}{U})$
104	102 103	eqtrd	$⊢ φ \to {(- (\frac{M}{U}))}^{2} = (\frac{M}{U}) (\frac{M}{U})$
105	104	oveq2d	$⊢ φ \to U {(- (\frac{M}{U}))}^{2} = U (\frac{M}{U}) (\frac{M}{U})$
106	11 43 43	mulassd	$⊢ φ \to U (\frac{M}{U}) (\frac{M}{U}) = U (\frac{M}{U}) (\frac{M}{U})$
107	29 11 12	divcan2d	$⊢ φ \to U (\frac{M}{U}) = M$
108	107	oveq1d	$⊢ φ \to U (\frac{M}{U}) (\frac{M}{U}) = M (\frac{M}{U})$
109	105 106 108	3eqtr2d	$⊢ φ \to U {(- (\frac{M}{U}))}^{2} = M (\frac{M}{U})$
110	109	oveq2d	$⊢ φ \to 3 U {(- (\frac{M}{U}))}^{2} = 3 M (\frac{M}{U})$
111	25 29 43	mulassd	$⊢ φ \to 3 \cdot M (\frac{M}{U}) = 3 M (\frac{M}{U})$
112	95	oveq1d	$⊢ φ \to 3 \cdot M (\frac{M}{U}) = P (\frac{M}{U})$
113	110 111 112	3eqtr2d	$⊢ φ \to 3 U {(- (\frac{M}{U}))}^{2} = P (\frac{M}{U})$
114		3nn	$⊢ 3 \in ℕ$
115	114	a1i	$⊢ φ \to 3 \in ℕ$
116		n2dvds3	$⊢ \neg 2 ∥ 3$
117	116	a1i	$⊢ φ \to \neg 2 ∥ 3$
118		oexpneg	$⊢ (\frac{M}{U} \in ℂ \land 3 \in ℕ \land \neg 2 ∥ 3) \to {(- (\frac{M}{U}))}^{3} = - {(\frac{M}{U})}^{3}$
119	43 115 117 118	syl3anc	$⊢ φ \to {(- (\frac{M}{U}))}^{3} = - {(\frac{M}{U})}^{3}$
120	14	a1i	$⊢ φ \to 3 \in ℕ_{0}$
121	29 11 12 120	expdivd	$⊢ φ \to {(\frac{M}{U})}^{3} = \frac{M^{3}}{U^{3}}$
122	121	negeqd	$⊢ φ \to - {(\frac{M}{U})}^{3} = - \frac{M^{3}}{U^{3}}$
123	119 122	eqtrd	$⊢ φ \to {(- (\frac{M}{U}))}^{3} = - \frac{M^{3}}{U^{3}}$
124	113 123	oveq12d	$⊢ φ \to 3 U {(- (\frac{M}{U}))}^{2} + {(- (\frac{M}{U}))}^{3} = P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
125	100 124	oveq12d	$⊢ φ \to U^{3} + 3 U^{2} (- \frac{M}{U}) + 3 U {(- (\frac{M}{U}))}^{2} + {(- (\frac{M}{U}))}^{3} = U^{3} + (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
126	74 77 125	3eqtrd	$⊢ φ \to X^{3} = U^{3} + (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})$
127	56 39	addcld	$⊢ φ \to P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}) \in ℂ$
128	16 55 127	addassd	$⊢ φ \to U^{3} + (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}) = U^{3} + (- P U) + (P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}))$
129	126 128	eqtrd	$⊢ φ \to X^{3} = U^{3} + (- P U) + (P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}))$
130	129	oveq1d	$⊢ φ \to X^{3} + P X + Q = U^{3} + ((- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + P X + Q$
131	55 127	addcld	$⊢ φ \to (- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}}) \in ℂ$
132	37 2	addcld	$⊢ φ \to P X + Q \in ℂ$
133	16 131 132	addassd	$⊢ φ \to U^{3} + ((- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + P X + Q = U^{3} + ((- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + (P X + Q)$
134	130 133	eqtrd	$⊢ φ \to X^{3} + P X + Q = U^{3} + ((- P U) + P (\frac{M}{U}) + (- \frac{M^{3}}{U^{3}})) + (P X + Q)$
135	16	sqcld	$⊢ φ \to {(U^{3})}^{2} \in ℂ$
136	68 31	subcld	$⊢ φ \to Q U^{3} - M^{3} \in ℂ$
137	135 136 16 21	divdird	$⊢ φ \to \frac{{(U^{3})}^{2} + Q U^{3} - M^{3}}{U^{3}} = (\frac{{(U^{3})}^{2}}{U^{3}}) + (\frac{Q U^{3} - M^{3}}{U^{3}})$
138	71 134 137	3eqtr4d	$⊢ φ \to X^{3} + P X + Q = \frac{{(U^{3})}^{2} + Q U^{3} - M^{3}}{U^{3}}$
139	138	eqeq1d	$⊢ φ \to (X^{3} + P X + Q = 0 \leftrightarrow \frac{{(U^{3})}^{2} + Q U^{3} - M^{3}}{U^{3}} = 0)$
140	135 136	addcld	$⊢ φ \to {(U^{3})}^{2} + Q U^{3} - M^{3} \in ℂ$
141	140 16 21	diveq0ad	$⊢ φ \to (\frac{{(U^{3})}^{2} + Q U^{3} - M^{3}}{U^{3}} = 0 \leftrightarrow {(U^{3})}^{2} + Q U^{3} - M^{3} = 0)$
142	139 141	bitrd	$⊢ φ \to (X^{3} + P X + Q = 0 \leftrightarrow {(U^{3})}^{2} + Q U^{3} - M^{3} = 0)$

Metamath Proof Explorer

Theorem dcubic1lem

Proof