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	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
	dcubic.d	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
	dcubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	dcubic.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
	dcubic.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( 𝐺 − 𝑁 ) )
	dcubic.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
	dcubic.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
	dcubic.m	⊢ ( 𝜑 → 𝑀 = ( 𝑃 / 3 ) )
	dcubic.n	⊢ ( 𝜑 → 𝑁 = ( 𝑄 / 2 ) )
	dcubic.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
	dcubic2.u	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
	dcubic2.z	⊢ ( 𝜑 → 𝑈 ≠ 0 )
	dcubic2.2	⊢ ( 𝜑 → 𝑋 = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
Assertion	dcubic1lem	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		dcubic.c	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
2		dcubic.d	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
3		dcubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4		dcubic.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
5		dcubic.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( 𝐺 − 𝑁 ) )
6		dcubic.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
7		dcubic.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
8		dcubic.m	⊢ ( 𝜑 → 𝑀 = ( 𝑃 / 3 ) )
9		dcubic.n	⊢ ( 𝜑 → 𝑁 = ( 𝑄 / 2 ) )
10		dcubic.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
11		dcubic2.u	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
12		dcubic2.z	⊢ ( 𝜑 → 𝑈 ≠ 0 )
13		dcubic2.2	⊢ ( 𝜑 → 𝑋 = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
14		3nn0	⊢ 3 ∈ ℕ₀
15		expcl	⊢ ( ( 𝑈 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑈 ↑ 3 ) ∈ ℂ )
16	11 14 15	sylancl	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℂ )
17	16	sqvald	⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) ↑ 2 ) = ( ( 𝑈 ↑ 3 ) · ( 𝑈 ↑ 3 ) ) )
18	17	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) / ( 𝑈 ↑ 3 ) ) = ( ( ( 𝑈 ↑ 3 ) · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) )
19		3z	⊢ 3 ∈ ℤ
20	19	a1i	⊢ ( 𝜑 → 3 ∈ ℤ )
21	11 12 20	expne0d	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ≠ 0 )
22	16 16 21	divcan4d	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) = ( 𝑈 ↑ 3 ) )
23	18 22	eqtr2d	⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) = ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) / ( 𝑈 ↑ 3 ) ) )
24		3cn	⊢ 3 ∈ ℂ
25	24	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
26		3ne0	⊢ 3 ≠ 0
27	26	a1i	⊢ ( 𝜑 → 3 ≠ 0 )
28	1 25 27	divcld	⊢ ( 𝜑 → ( 𝑃 / 3 ) ∈ ℂ )
29	8 28	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
30		expcl	⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
31	29 14 30	sylancl	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
32	31 16 21	divcld	⊢ ( 𝜑 → ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ∈ ℂ )
33	2 32	negsubd	⊢ ( 𝜑 → ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( 𝑄 − ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
34	2 16 21	divcan4d	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) = 𝑄 )
35	34	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) − ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( 𝑄 − ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
36	33 35	eqtr4d	⊢ ( 𝜑 → ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) − ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
37	1 3	mulcld	⊢ ( 𝜑 → ( 𝑃 · 𝑋 ) ∈ ℂ )
38	37	negcld	⊢ ( 𝜑 → - ( 𝑃 · 𝑋 ) ∈ ℂ )
39	32	negcld	⊢ ( 𝜑 → - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ∈ ℂ )
40	38 39 37 2	add42d	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑋 ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( - ( 𝑃 · 𝑋 ) + ( 𝑃 · 𝑋 ) ) + ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
41	1 3	mulneg2d	⊢ ( 𝜑 → ( 𝑃 · - 𝑋 ) = - ( 𝑃 · 𝑋 ) )
42	13	negeqd	⊢ ( 𝜑 → - 𝑋 = - ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
43	29 11 12	divcld	⊢ ( 𝜑 → ( 𝑀 / 𝑈 ) ∈ ℂ )
44	11 43	negsubdid	⊢ ( 𝜑 → - ( 𝑈 − ( 𝑀 / 𝑈 ) ) = ( - 𝑈 + ( 𝑀 / 𝑈 ) ) )
45	42 44	eqtrd	⊢ ( 𝜑 → - 𝑋 = ( - 𝑈 + ( 𝑀 / 𝑈 ) ) )
46	45	oveq2d	⊢ ( 𝜑 → ( 𝑃 · - 𝑋 ) = ( 𝑃 · ( - 𝑈 + ( 𝑀 / 𝑈 ) ) ) )
47	41 46	eqtr3d	⊢ ( 𝜑 → - ( 𝑃 · 𝑋 ) = ( 𝑃 · ( - 𝑈 + ( 𝑀 / 𝑈 ) ) ) )
48	11	negcld	⊢ ( 𝜑 → - 𝑈 ∈ ℂ )
49	1 48 43	adddid	⊢ ( 𝜑 → ( 𝑃 · ( - 𝑈 + ( 𝑀 / 𝑈 ) ) ) = ( ( 𝑃 · - 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) )
50	1 11	mulneg2d	⊢ ( 𝜑 → ( 𝑃 · - 𝑈 ) = - ( 𝑃 · 𝑈 ) )
51	50	oveq1d	⊢ ( 𝜑 → ( ( 𝑃 · - 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) = ( - ( 𝑃 · 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) )
52	47 49 51	3eqtrd	⊢ ( 𝜑 → - ( 𝑃 · 𝑋 ) = ( - ( 𝑃 · 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) )
53	52	oveq1d	⊢ ( 𝜑 → ( - ( 𝑃 · 𝑋 ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( ( - ( 𝑃 · 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
54	1 11	mulcld	⊢ ( 𝜑 → ( 𝑃 · 𝑈 ) ∈ ℂ )
55	54	negcld	⊢ ( 𝜑 → - ( 𝑃 · 𝑈 ) ∈ ℂ )
56	1 43	mulcld	⊢ ( 𝜑 → ( 𝑃 · ( 𝑀 / 𝑈 ) ) ∈ ℂ )
57	55 56 39	addassd	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑈 ) + ( 𝑃 · ( 𝑀 / 𝑈 ) ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
58	53 57	eqtrd	⊢ ( 𝜑 → ( - ( 𝑃 · 𝑋 ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) = ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
59	58	oveq1d	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑋 ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) )
60	38 37	addcomd	⊢ ( 𝜑 → ( - ( 𝑃 · 𝑋 ) + ( 𝑃 · 𝑋 ) ) = ( ( 𝑃 · 𝑋 ) + - ( 𝑃 · 𝑋 ) ) )
61	37	negidd	⊢ ( 𝜑 → ( ( 𝑃 · 𝑋 ) + - ( 𝑃 · 𝑋 ) ) = 0 )
62	60 61	eqtrd	⊢ ( 𝜑 → ( - ( 𝑃 · 𝑋 ) + ( 𝑃 · 𝑋 ) ) = 0 )
63	62	oveq1d	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑋 ) + ( 𝑃 · 𝑋 ) ) + ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) = ( 0 + ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
64	2 39	addcld	⊢ ( 𝜑 → ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ∈ ℂ )
65	64	addlidd	⊢ ( 𝜑 → ( 0 + ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) = ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
66	63 65	eqtrd	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑋 ) + ( 𝑃 · 𝑋 ) ) + ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) = ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
67	40 59 66	3eqtr3d	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( 𝑄 + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
68	2 16	mulcld	⊢ ( 𝜑 → ( 𝑄 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
69	68 31 16 21	divsubdird	⊢ ( 𝜑 → ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) = ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) − ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
70	36 67 69	3eqtr4d	⊢ ( 𝜑 → ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) )
71	23 70	oveq12d	⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) + ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) ) = ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) / ( 𝑈 ↑ 3 ) ) + ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) ) )
72	11 43	negsubd	⊢ ( 𝜑 → ( 𝑈 + - ( 𝑀 / 𝑈 ) ) = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
73	13 72	eqtr4d	⊢ ( 𝜑 → 𝑋 = ( 𝑈 + - ( 𝑀 / 𝑈 ) ) )
74	73	oveq1d	⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) = ( ( 𝑈 + - ( 𝑀 / 𝑈 ) ) ↑ 3 ) )
75	43	negcld	⊢ ( 𝜑 → - ( 𝑀 / 𝑈 ) ∈ ℂ )
76		binom3	⊢ ( ( 𝑈 ∈ ℂ ∧ - ( 𝑀 / 𝑈 ) ∈ ℂ ) → ( ( 𝑈 + - ( 𝑀 / 𝑈 ) ) ↑ 3 ) = ( ( ( 𝑈 ↑ 3 ) + ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) ) + ( ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) + ( - ( 𝑀 / 𝑈 ) ↑ 3 ) ) ) )
77	11 75 76	syl2anc	⊢ ( 𝜑 → ( ( 𝑈 + - ( 𝑀 / 𝑈 ) ) ↑ 3 ) = ( ( ( 𝑈 ↑ 3 ) + ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) ) + ( ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) + ( - ( 𝑀 / 𝑈 ) ↑ 3 ) ) ) )
78	11	sqcld	⊢ ( 𝜑 → ( 𝑈 ↑ 2 ) ∈ ℂ )
79	78 43	mulneg2d	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) = - ( ( 𝑈 ↑ 2 ) · ( 𝑀 / 𝑈 ) ) )
80	78 29 11 12	div12d	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) · ( 𝑀 / 𝑈 ) ) = ( 𝑀 · ( ( 𝑈 ↑ 2 ) / 𝑈 ) ) )
81	11	sqvald	⊢ ( 𝜑 → ( 𝑈 ↑ 2 ) = ( 𝑈 · 𝑈 ) )
82	81	oveq1d	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) / 𝑈 ) = ( ( 𝑈 · 𝑈 ) / 𝑈 ) )
83	11 11 12	divcan4d	⊢ ( 𝜑 → ( ( 𝑈 · 𝑈 ) / 𝑈 ) = 𝑈 )
84	82 83	eqtrd	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) / 𝑈 ) = 𝑈 )
85	84	oveq2d	⊢ ( 𝜑 → ( 𝑀 · ( ( 𝑈 ↑ 2 ) / 𝑈 ) ) = ( 𝑀 · 𝑈 ) )
86	80 85	eqtrd	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) · ( 𝑀 / 𝑈 ) ) = ( 𝑀 · 𝑈 ) )
87	86	negeqd	⊢ ( 𝜑 → - ( ( 𝑈 ↑ 2 ) · ( 𝑀 / 𝑈 ) ) = - ( 𝑀 · 𝑈 ) )
88	79 87	eqtrd	⊢ ( 𝜑 → ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) = - ( 𝑀 · 𝑈 ) )
89	88	oveq2d	⊢ ( 𝜑 → ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) = ( 3 · - ( 𝑀 · 𝑈 ) ) )
90	29 11	mulcld	⊢ ( 𝜑 → ( 𝑀 · 𝑈 ) ∈ ℂ )
91	25 90	mulneg2d	⊢ ( 𝜑 → ( 3 · - ( 𝑀 · 𝑈 ) ) = - ( 3 · ( 𝑀 · 𝑈 ) ) )
92	25 29 11	mulassd	⊢ ( 𝜑 → ( ( 3 · 𝑀 ) · 𝑈 ) = ( 3 · ( 𝑀 · 𝑈 ) ) )
93	8	oveq2d	⊢ ( 𝜑 → ( 3 · 𝑀 ) = ( 3 · ( 𝑃 / 3 ) ) )
94	1 25 27	divcan2d	⊢ ( 𝜑 → ( 3 · ( 𝑃 / 3 ) ) = 𝑃 )
95	93 94	eqtrd	⊢ ( 𝜑 → ( 3 · 𝑀 ) = 𝑃 )
96	95	oveq1d	⊢ ( 𝜑 → ( ( 3 · 𝑀 ) · 𝑈 ) = ( 𝑃 · 𝑈 ) )
97	92 96	eqtr3d	⊢ ( 𝜑 → ( 3 · ( 𝑀 · 𝑈 ) ) = ( 𝑃 · 𝑈 ) )
98	97	negeqd	⊢ ( 𝜑 → - ( 3 · ( 𝑀 · 𝑈 ) ) = - ( 𝑃 · 𝑈 ) )
99	89 91 98	3eqtrd	⊢ ( 𝜑 → ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) = - ( 𝑃 · 𝑈 ) )
100	99	oveq2d	⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) + ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) ) = ( ( 𝑈 ↑ 3 ) + - ( 𝑃 · 𝑈 ) ) )
101		sqneg	⊢ ( ( 𝑀 / 𝑈 ) ∈ ℂ → ( - ( 𝑀 / 𝑈 ) ↑ 2 ) = ( ( 𝑀 / 𝑈 ) ↑ 2 ) )
102	43 101	syl	⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 2 ) = ( ( 𝑀 / 𝑈 ) ↑ 2 ) )
103	43	sqvald	⊢ ( 𝜑 → ( ( 𝑀 / 𝑈 ) ↑ 2 ) = ( ( 𝑀 / 𝑈 ) · ( 𝑀 / 𝑈 ) ) )
104	102 103	eqtrd	⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 2 ) = ( ( 𝑀 / 𝑈 ) · ( 𝑀 / 𝑈 ) ) )
105	104	oveq2d	⊢ ( 𝜑 → ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) = ( 𝑈 · ( ( 𝑀 / 𝑈 ) · ( 𝑀 / 𝑈 ) ) ) )
106	11 43 43	mulassd	⊢ ( 𝜑 → ( ( 𝑈 · ( 𝑀 / 𝑈 ) ) · ( 𝑀 / 𝑈 ) ) = ( 𝑈 · ( ( 𝑀 / 𝑈 ) · ( 𝑀 / 𝑈 ) ) ) )
107	29 11 12	divcan2d	⊢ ( 𝜑 → ( 𝑈 · ( 𝑀 / 𝑈 ) ) = 𝑀 )
108	107	oveq1d	⊢ ( 𝜑 → ( ( 𝑈 · ( 𝑀 / 𝑈 ) ) · ( 𝑀 / 𝑈 ) ) = ( 𝑀 · ( 𝑀 / 𝑈 ) ) )
109	105 106 108	3eqtr2d	⊢ ( 𝜑 → ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) = ( 𝑀 · ( 𝑀 / 𝑈 ) ) )
110	109	oveq2d	⊢ ( 𝜑 → ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) = ( 3 · ( 𝑀 · ( 𝑀 / 𝑈 ) ) ) )
111	25 29 43	mulassd	⊢ ( 𝜑 → ( ( 3 · 𝑀 ) · ( 𝑀 / 𝑈 ) ) = ( 3 · ( 𝑀 · ( 𝑀 / 𝑈 ) ) ) )
112	95	oveq1d	⊢ ( 𝜑 → ( ( 3 · 𝑀 ) · ( 𝑀 / 𝑈 ) ) = ( 𝑃 · ( 𝑀 / 𝑈 ) ) )
113	110 111 112	3eqtr2d	⊢ ( 𝜑 → ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) = ( 𝑃 · ( 𝑀 / 𝑈 ) ) )
114		3nn	⊢ 3 ∈ ℕ
115	114	a1i	⊢ ( 𝜑 → 3 ∈ ℕ )
116		n2dvds3	⊢ ¬ 2 ∥ 3
117	116	a1i	⊢ ( 𝜑 → ¬ 2 ∥ 3 )
118		oexpneg	⊢ ( ( ( 𝑀 / 𝑈 ) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - ( 𝑀 / 𝑈 ) ↑ 3 ) = - ( ( 𝑀 / 𝑈 ) ↑ 3 ) )
119	43 115 117 118	syl3anc	⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 3 ) = - ( ( 𝑀 / 𝑈 ) ↑ 3 ) )
120	14	a1i	⊢ ( 𝜑 → 3 ∈ ℕ₀ )
121	29 11 12 120	expdivd	⊢ ( 𝜑 → ( ( 𝑀 / 𝑈 ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
122	121	negeqd	⊢ ( 𝜑 → - ( ( 𝑀 / 𝑈 ) ↑ 3 ) = - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
123	119 122	eqtrd	⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 3 ) = - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
124	113 123	oveq12d	⊢ ( 𝜑 → ( ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) + ( - ( 𝑀 / 𝑈 ) ↑ 3 ) ) = ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) )
125	100 124	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) + ( 3 · ( ( 𝑈 ↑ 2 ) · - ( 𝑀 / 𝑈 ) ) ) ) + ( ( 3 · ( 𝑈 · ( - ( 𝑀 / 𝑈 ) ↑ 2 ) ) ) + ( - ( 𝑀 / 𝑈 ) ↑ 3 ) ) ) = ( ( ( 𝑈 ↑ 3 ) + - ( 𝑃 · 𝑈 ) ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
126	74 77 125	3eqtrd	⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) = ( ( ( 𝑈 ↑ 3 ) + - ( 𝑃 · 𝑈 ) ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) )
127	56 39	addcld	⊢ ( 𝜑 → ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ∈ ℂ )
128	16 55 127	addassd	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) + - ( 𝑃 · 𝑈 ) ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) = ( ( 𝑈 ↑ 3 ) + ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) ) )
129	126 128	eqtrd	⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) = ( ( 𝑈 ↑ 3 ) + ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) ) )
130	129	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( ( 𝑈 ↑ 3 ) + ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) )
131	55 127	addcld	⊢ ( 𝜑 → ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) ∈ ℂ )
132	37 2	addcld	⊢ ( 𝜑 → ( ( 𝑃 · 𝑋 ) + 𝑄 ) ∈ ℂ )
133	16 131 132	addassd	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) + ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( 𝑈 ↑ 3 ) + ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) ) )
134	130 133	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( 𝑈 ↑ 3 ) + ( ( - ( 𝑃 · 𝑈 ) + ( ( 𝑃 · ( 𝑀 / 𝑈 ) ) + - ( ( 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) ) ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) ) )
135	16	sqcld	⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) ↑ 2 ) ∈ ℂ )
136	68 31	subcld	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ∈ ℂ )
137	135 136 16 21	divdird	⊢ ( 𝜑 → ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) / ( 𝑈 ↑ 3 ) ) = ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) / ( 𝑈 ↑ 3 ) ) + ( ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) ) )
138	71 134 137	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) / ( 𝑈 ↑ 3 ) ) )
139	138	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) / ( 𝑈 ↑ 3 ) ) = 0 ) )
140	135 136	addcld	⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) ∈ ℂ )
141	140 16 21	diveq0ad	⊢ ( 𝜑 → ( ( ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) / ( 𝑈 ↑ 3 ) ) = 0 ↔ ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 ) )
142	139 141	bitrd	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 ) )

Metamath Proof Explorer

Theorem dcubic1lem

Proof