Metamath Proof Explorer

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 )