Theorem dcubic1

Description: Forward direction of dcubic : the claimed formula produces solutions to the cubic equation. (Contributed by Mario Carneiro, 25-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 )
	dcubic1.x	⊢ ( 𝜑 → 𝑋 = ( 𝑇 − ( 𝑀 / 𝑇 ) ) )
Assertion	dcubic1	⊢ ( 𝜑 → ( ( 𝑋 ↑ 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		dcubic1.x	⊢ ( 𝜑 → 𝑋 = ( 𝑇 − ( 𝑀 / 𝑇 ) ) )
12	5	oveq1d	⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) ↑ 2 ) = ( ( 𝐺 − 𝑁 ) ↑ 2 ) )
13	2	halfcld	⊢ ( 𝜑 → ( 𝑄 / 2 ) ∈ ℂ )
14	9 13	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
15		binom2sub	⊢ ( ( 𝐺 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐺 − 𝑁 ) ↑ 2 ) = ( ( ( 𝐺 ↑ 2 ) − ( 2 · ( 𝐺 · 𝑁 ) ) ) + ( 𝑁 ↑ 2 ) ) )
16	6 14 15	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 − 𝑁 ) ↑ 2 ) = ( ( ( 𝐺 ↑ 2 ) − ( 2 · ( 𝐺 · 𝑁 ) ) ) + ( 𝑁 ↑ 2 ) ) )
17		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
18	17 6 14	mul12d	⊢ ( 𝜑 → ( 2 · ( 𝐺 · 𝑁 ) ) = ( 𝐺 · ( 2 · 𝑁 ) ) )
19	9	oveq2d	⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 2 · ( 𝑄 / 2 ) ) )
20		2ne0	⊢ 2 ≠ 0
21	20	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
22	2 17 21	divcan2d	⊢ ( 𝜑 → ( 2 · ( 𝑄 / 2 ) ) = 𝑄 )
23	19 22	eqtrd	⊢ ( 𝜑 → ( 2 · 𝑁 ) = 𝑄 )
24	23	oveq2d	⊢ ( 𝜑 → ( 𝐺 · ( 2 · 𝑁 ) ) = ( 𝐺 · 𝑄 ) )
25	6 2	mulcomd	⊢ ( 𝜑 → ( 𝐺 · 𝑄 ) = ( 𝑄 · 𝐺 ) )
26	18 24 25	3eqtrd	⊢ ( 𝜑 → ( 2 · ( 𝐺 · 𝑁 ) ) = ( 𝑄 · 𝐺 ) )
27	7 26	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) − ( 2 · ( 𝐺 · 𝑁 ) ) ) = ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) )
28	27	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐺 ↑ 2 ) − ( 2 · ( 𝐺 · 𝑁 ) ) ) + ( 𝑁 ↑ 2 ) ) = ( ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( 𝑁 ↑ 2 ) ) )
29	12 16 28	3eqtrd	⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) ↑ 2 ) = ( ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( 𝑁 ↑ 2 ) ) )
30	14	sqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
31		3cn	⊢ 3 ∈ ℂ
32	31	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
33		3ne0	⊢ 3 ≠ 0
34	33	a1i	⊢ ( 𝜑 → 3 ≠ 0 )
35	1 32 34	divcld	⊢ ( 𝜑 → ( 𝑃 / 3 ) ∈ ℂ )
36	8 35	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
37		3nn0	⊢ 3 ∈ ℕ0
38		expcl	⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
39	36 37 38	sylancl	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
40	30 39	addcld	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) ∈ ℂ )
41	2 6	mulcld	⊢ ( 𝜑 → ( 𝑄 · 𝐺 ) ∈ ℂ )
42	40 30 41	addsubd	⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) + ( 𝑁 ↑ 2 ) ) − ( 𝑄 · 𝐺 ) ) = ( ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( 𝑁 ↑ 2 ) ) )
43	30 39 30	add32d	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) + ( 𝑁 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) )
44	30	2timesd	⊢ ( 𝜑 → ( 2 · ( 𝑁 ↑ 2 ) ) = ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
45	44	oveq1d	⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) = ( ( ( 𝑁 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) )
46	43 45	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) + ( 𝑁 ↑ 2 ) ) = ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) )
47	46	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) + ( 𝑁 ↑ 2 ) ) − ( 𝑄 · 𝐺 ) ) = ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) )
48	29 42 47	3eqtr2d	⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) ↑ 2 ) = ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) )
49	2 6 14	subdid	⊢ ( 𝜑 → ( 𝑄 · ( 𝐺 − 𝑁 ) ) = ( ( 𝑄 · 𝐺 ) − ( 𝑄 · 𝑁 ) ) )
50	5	oveq2d	⊢ ( 𝜑 → ( 𝑄 · ( 𝑇 ↑ 3 ) ) = ( 𝑄 · ( 𝐺 − 𝑁 ) ) )
51	14	sqvald	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
52	51	oveq2d	⊢ ( 𝜑 → ( 2 · ( 𝑁 ↑ 2 ) ) = ( 2 · ( 𝑁 · 𝑁 ) ) )
53	17 14 14	mulassd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · 𝑁 ) = ( 2 · ( 𝑁 · 𝑁 ) ) )
54	23	oveq1d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · 𝑁 ) = ( 𝑄 · 𝑁 ) )
55	52 53 54	3eqtr2d	⊢ ( 𝜑 → ( 2 · ( 𝑁 ↑ 2 ) ) = ( 𝑄 · 𝑁 ) )
56	55	oveq2d	⊢ ( 𝜑 → ( ( 𝑄 · 𝐺 ) − ( 2 · ( 𝑁 ↑ 2 ) ) ) = ( ( 𝑄 · 𝐺 ) − ( 𝑄 · 𝑁 ) ) )
57	49 50 56	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 · ( 𝑇 ↑ 3 ) ) = ( ( 𝑄 · 𝐺 ) − ( 2 · ( 𝑁 ↑ 2 ) ) ) )
58	57	oveq1d	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝑇 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) = ( ( ( 𝑄 · 𝐺 ) − ( 2 · ( 𝑁 ↑ 2 ) ) ) − ( 𝑀 ↑ 3 ) ) )
59		2cn	⊢ 2 ∈ ℂ
60		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ∈ ℂ ) → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
61	59 30 60	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
62	41 61 39	subsub4d	⊢ ( 𝜑 → ( ( ( 𝑄 · 𝐺 ) − ( 2 · ( 𝑁 ↑ 2 ) ) ) − ( 𝑀 ↑ 3 ) ) = ( ( 𝑄 · 𝐺 ) − ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ) )
63	58 62	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 · ( 𝑇 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) = ( ( 𝑄 · 𝐺 ) − ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ) )
64	48 63	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑇 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑇 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( ( 𝑄 · 𝐺 ) − ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ) ) )
65	61 39	addcld	⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ∈ ℂ )
66		npncan2	⊢ ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ∈ ℂ ∧ ( 𝑄 · 𝐺 ) ∈ ℂ ) → ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( ( 𝑄 · 𝐺 ) − ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ) ) = 0 )
67	65 41 66	syl2anc	⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) − ( 𝑄 · 𝐺 ) ) + ( ( 𝑄 · 𝐺 ) − ( ( 2 · ( 𝑁 ↑ 2 ) ) + ( 𝑀 ↑ 3 ) ) ) ) = 0 )
68	64 67	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑇 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑇 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 )
69	1 2 3 4 5 6 7 8 9 10 4 10 11	dcubic1lem	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ( ( ( 𝑇 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑇 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 ) )
70	68 69	mpbird	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )