cubic2

Description: The solution to the general cubic equation, for arbitrary choices G and T of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	cubic2.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	cubic2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	cubic2.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	cubic2.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	cubic2.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	cubic2.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	cubic2.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
	cubic2.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑁 + 𝐺 ) / 2 ) )
	cubic2.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
	cubic2.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
	cubic2.m	⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) )
	cubic2.n	⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
	cubic2.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
Assertion	cubic2	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cubic2.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		cubic2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		cubic2.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4		cubic2.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		cubic2.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
6		cubic2.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
7		cubic2.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
8		cubic2.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑁 + 𝐺 ) / 2 ) )
9		cubic2.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
10		cubic2.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
11		cubic2.m	⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) )
12		cubic2.n	⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
13		cubic2.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
14		3nn0	⊢ 3 ∈ ℕ₀
15		expcl	⊢ ( ( 𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑋 ↑ 3 ) ∈ ℂ )
16	6 14 15	sylancl	⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) ∈ ℂ )
17	1 16	mulcld	⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ↑ 3 ) ) ∈ ℂ )
18	6	sqcld	⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
19	3 18	mulcld	⊢ ( 𝜑 → ( 𝐵 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
20	17 19	addcld	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
21	4 6	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ℂ )
22	21 5	addcld	⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) + 𝐷 ) ∈ ℂ )
23	20 22	addcld	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ∈ ℂ )
24	23 1 2	diveq0ad	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) / 𝐴 ) = 0 ↔ ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ) )
25	20 22 1 2	divdird	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) / 𝐴 ) = ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) / 𝐴 ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) / 𝐴 ) ) )
26	17 19 1 2	divdird	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) / 𝐴 ) = ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) / 𝐴 ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) ) )
27	16 1 2	divcan3d	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) / 𝐴 ) = ( 𝑋 ↑ 3 ) )
28	3 18 1 2	div23d	⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) = ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) )
29	27 28	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) / 𝐴 ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) ) = ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) )
30	26 29	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) / 𝐴 ) = ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) )
31	21 5 1 2	divdird	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) / 𝐴 ) = ( ( ( 𝐶 · 𝑋 ) / 𝐴 ) + ( 𝐷 / 𝐴 ) ) )
32	4 6 1 2	div23d	⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) / 𝐴 ) = ( ( 𝐶 / 𝐴 ) · 𝑋 ) )
33	32	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) / 𝐴 ) + ( 𝐷 / 𝐴 ) ) = ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) )
34	31 33	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) / 𝐴 ) = ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) )
35	30 34	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) / 𝐴 ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) / 𝐴 ) ) = ( ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) ) )
36	25 35	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) / 𝐴 ) = ( ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) ) )
37	36	eqeq1d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) / 𝐴 ) = 0 ↔ ( ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) ) = 0 ) )
38	24 37	bitr3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ( ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) ) = 0 ) )
39	3 1 2	divcld	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℂ )
40	4 1 2	divcld	⊢ ( 𝜑 → ( 𝐶 / 𝐴 ) ∈ ℂ )
41	5 1 2	divcld	⊢ ( 𝜑 → ( 𝐷 / 𝐴 ) ∈ ℂ )
42	7 1 2	divcld	⊢ ( 𝜑 → ( 𝑇 / 𝐴 ) ∈ ℂ )
43	14	a1i	⊢ ( 𝜑 → 3 ∈ ℕ₀ )
44	7 1 2 43	expdivd	⊢ ( 𝜑 → ( ( 𝑇 / 𝐴 ) ↑ 3 ) = ( ( 𝑇 ↑ 3 ) / ( 𝐴 ↑ 3 ) ) )
45	8	oveq1d	⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) / ( 𝐴 ↑ 3 ) ) = ( ( ( 𝑁 + 𝐺 ) / 2 ) / ( 𝐴 ↑ 3 ) ) )
46		2cn	⊢ 2 ∈ ℂ
47		expcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝐵 ↑ 3 ) ∈ ℂ )
48	3 14 47	sylancl	⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) ∈ ℂ )
49		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
50	46 48 49	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
51		9cn	⊢ 9 ∈ ℂ
52		mulcl	⊢ ( ( 9 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 9 · 𝐴 ) ∈ ℂ )
53	51 1 52	sylancr	⊢ ( 𝜑 → ( 9 · 𝐴 ) ∈ ℂ )
54	3 4	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
55	53 54	mulcld	⊢ ( 𝜑 → ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
56	50 55	subcld	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
57		2nn0	⊢ 2 ∈ ℕ₀
58		7nn	⊢ 7 ∈ ℕ
59	57 58	decnncl	⊢ ; 2 7 ∈ ℕ
60	59	nncni	⊢ ; 2 7 ∈ ℂ
61	1	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
62	61 5	mulcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ )
63		mulcl	⊢ ( ( ; 2 7 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ ) → ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
64	60 62 63	sylancr	⊢ ( 𝜑 → ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
65	56 64	addcld	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) ∈ ℂ )
66	12 65	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
67	66 9	addcld	⊢ ( 𝜑 → ( 𝑁 + 𝐺 ) ∈ ℂ )
68		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
69		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
70	1 14 69	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) ∈ ℂ )
71		2ne0	⊢ 2 ≠ 0
72	71	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
73		3z	⊢ 3 ∈ ℤ
74	73	a1i	⊢ ( 𝜑 → 3 ∈ ℤ )
75	1 2 74	expne0d	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) ≠ 0 )
76	67 68 70 72 75	divdiv32d	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ( 𝐴 ↑ 3 ) ) = ( ( ( 𝑁 + 𝐺 ) / ( 𝐴 ↑ 3 ) ) / 2 ) )
77	66 9 70 75	divdird	⊢ ( 𝜑 → ( ( 𝑁 + 𝐺 ) / ( 𝐴 ↑ 3 ) ) = ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) + ( 𝐺 / ( 𝐴 ↑ 3 ) ) ) )
78	77	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / ( 𝐴 ↑ 3 ) ) / 2 ) = ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) + ( 𝐺 / ( 𝐴 ↑ 3 ) ) ) / 2 ) )
79	76 78	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ( 𝐴 ↑ 3 ) ) = ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) + ( 𝐺 / ( 𝐴 ↑ 3 ) ) ) / 2 ) )
80	44 45 79	3eqtrd	⊢ ( 𝜑 → ( ( 𝑇 / 𝐴 ) ↑ 3 ) = ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) + ( 𝐺 / ( 𝐴 ↑ 3 ) ) ) / 2 ) )
81	9 70 75	divcld	⊢ ( 𝜑 → ( 𝐺 / ( 𝐴 ↑ 3 ) ) ∈ ℂ )
82	9 70 75	sqdivd	⊢ ( 𝜑 → ( ( 𝐺 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) = ( ( 𝐺 ↑ 2 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
83	10	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
84	66	sqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
85		4cn	⊢ 4 ∈ ℂ
86	3	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
87		3cn	⊢ 3 ∈ ℂ
88	1 4	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
89		mulcl	⊢ ( ( 3 ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ∈ ℂ ) → ( 3 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
90	87 88 89	sylancr	⊢ ( 𝜑 → ( 3 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
91	86 90	subcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
92	11 91	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
93		expcl	⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
94	92 14 93	sylancl	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
95		mulcl	⊢ ( ( 4 ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
96	85 94 95	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
97	70	sqcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 3 ) ↑ 2 ) ∈ ℂ )
98		sqne0	⊢ ( ( 𝐴 ↑ 3 ) ∈ ℂ → ( ( ( 𝐴 ↑ 3 ) ↑ 2 ) ≠ 0 ↔ ( 𝐴 ↑ 3 ) ≠ 0 ) )
99	70 98	syl	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 3 ) ↑ 2 ) ≠ 0 ↔ ( 𝐴 ↑ 3 ) ≠ 0 ) )
100	75 99	mpbird	⊢ ( 𝜑 → ( ( 𝐴 ↑ 3 ) ↑ 2 ) ≠ 0 )
101	84 96 97 100	divsubdird	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) ) )
102	66 70 75	sqdivd	⊢ ( 𝜑 → ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) = ( ( 𝑁 ↑ 2 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
103		2z	⊢ 2 ∈ ℤ
104	103	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
105	1 2 104	expne0d	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ≠ 0 )
106	92 61 105 43	expdivd	⊢ ( 𝜑 → ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 2 ) ↑ 3 ) ) )
107	46 87	mulcomi	⊢ ( 2 · 3 ) = ( 3 · 2 )
108	107	oveq2i	⊢ ( 𝐴 ↑ ( 2 · 3 ) ) = ( 𝐴 ↑ ( 3 · 2 ) )
109	57	a1i	⊢ ( 𝜑 → 2 ∈ ℕ₀ )
110	1 43 109	expmuld	⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 · 3 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 3 ) )
111	1 109 43	expmuld	⊢ ( 𝜑 → ( 𝐴 ↑ ( 3 · 2 ) ) = ( ( 𝐴 ↑ 3 ) ↑ 2 ) )
112	108 110 111	3eqtr3a	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) ↑ 3 ) = ( ( 𝐴 ↑ 3 ) ↑ 2 ) )
113	112	oveq2d	⊢ ( 𝜑 → ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 2 ) ↑ 3 ) ) = ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
114	106 113	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
115	114	oveq2d	⊢ ( 𝜑 → ( 4 · ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) ) )
116	85	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
117	116 94 97 100	divassd	⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) ) )
118	115 117	eqtr4d	⊢ ( 𝜑 → ( 4 · ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) ) = ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) )
119	102 118	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) − ( 4 · ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) ) )
120	101 119	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ( 𝐴 ↑ 3 ) ↑ 2 ) ) = ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) − ( 4 · ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) ) ) )
121	82 83 120	3eqtrd	⊢ ( 𝜑 → ( ( 𝐺 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) = ( ( ( 𝑁 / ( 𝐴 ↑ 3 ) ) ↑ 2 ) − ( 4 · ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) ↑ 3 ) ) ) )
122	86 90 61 105	divsubdird	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) − ( ( 3 · ( 𝐴 · 𝐶 ) ) / ( 𝐴 ↑ 2 ) ) ) )
123	11	oveq1d	⊢ ( 𝜑 → ( 𝑀 / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) / ( 𝐴 ↑ 2 ) ) )
124	3 1 2	sqdivd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) )
125	1	sqvald	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
126	125	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 · 𝐶 ) / ( 𝐴 · 𝐴 ) ) )
127	4 1 1 2 2	divcan5d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) / ( 𝐴 · 𝐴 ) ) = ( 𝐶 / 𝐴 ) )
128	126 127	eqtr2d	⊢ ( 𝜑 → ( 𝐶 / 𝐴 ) = ( ( 𝐴 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) )
129	128	oveq2d	⊢ ( 𝜑 → ( 3 · ( 𝐶 / 𝐴 ) ) = ( 3 · ( ( 𝐴 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) ) )
130	87	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
131	130 88 61 105	divassd	⊢ ( 𝜑 → ( ( 3 · ( 𝐴 · 𝐶 ) ) / ( 𝐴 ↑ 2 ) ) = ( 3 · ( ( 𝐴 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) ) )
132	129 131	eqtr4d	⊢ ( 𝜑 → ( 3 · ( 𝐶 / 𝐴 ) ) = ( ( 3 · ( 𝐴 · 𝐶 ) ) / ( 𝐴 ↑ 2 ) ) )
133	124 132	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐵 / 𝐴 ) ↑ 2 ) − ( 3 · ( 𝐶 / 𝐴 ) ) ) = ( ( ( 𝐵 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) − ( ( 3 · ( 𝐴 · 𝐶 ) ) / ( 𝐴 ↑ 2 ) ) ) )
134	122 123 133	3eqtr4d	⊢ ( 𝜑 → ( 𝑀 / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐵 / 𝐴 ) ↑ 2 ) − ( 3 · ( 𝐶 / 𝐴 ) ) ) )
135	56 64 70 75	divdird	⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝐴 ↑ 3 ) ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) + ( ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝐴 ↑ 3 ) ) ) )
136	12	oveq1d	⊢ ( 𝜑 → ( 𝑁 / ( 𝐴 ↑ 3 ) ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) / ( 𝐴 ↑ 3 ) ) )
137	3 1 2 43	expdivd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) ↑ 3 ) = ( ( 𝐵 ↑ 3 ) / ( 𝐴 ↑ 3 ) ) )
138	137	oveq2d	⊢ ( 𝜑 → ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) = ( 2 · ( ( 𝐵 ↑ 3 ) / ( 𝐴 ↑ 3 ) ) ) )
139	68 48 70 75	divassd	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) / ( 𝐴 ↑ 3 ) ) = ( 2 · ( ( 𝐵 ↑ 3 ) / ( 𝐴 ↑ 3 ) ) ) )
140	138 139	eqtr4d	⊢ ( 𝜑 → ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) = ( ( 2 · ( 𝐵 ↑ 3 ) ) / ( 𝐴 ↑ 3 ) ) )
141	51	a1i	⊢ ( 𝜑 → 9 ∈ ℂ )
142	1 54	mulcld	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
143	141 142 70 75	divassd	⊢ ( 𝜑 → ( ( 9 · ( 𝐴 · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) = ( 9 · ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) ) )
144	141 1 54	mulassd	⊢ ( 𝜑 → ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) = ( 9 · ( 𝐴 · ( 𝐵 · 𝐶 ) ) ) )
145	144	oveq1d	⊢ ( 𝜑 → ( ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) = ( ( 9 · ( 𝐴 · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) )
146	54 61 1 105 2	divcan5d	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 · ( 𝐴 ↑ 2 ) ) ) = ( ( 𝐵 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) )
147		df-3	⊢ 3 = ( 2 + 1 )
148	147	oveq2i	⊢ ( 𝐴 ↑ 3 ) = ( 𝐴 ↑ ( 2 + 1 ) )
149		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀ ) → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
150	1 57 149	sylancl	⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
151	148 150	eqtrid	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
152	61 1	mulcomd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 ↑ 2 ) ) )
153	151 152	eqtrd	⊢ ( 𝜑 → ( 𝐴 ↑ 3 ) = ( 𝐴 · ( 𝐴 ↑ 2 ) ) )
154	153	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) = ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 · ( 𝐴 ↑ 2 ) ) ) )
155	3 1 4 1 2 2	divmuldivd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) = ( ( 𝐵 · 𝐶 ) / ( 𝐴 · 𝐴 ) ) )
156	125	oveq2d	⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 · 𝐶 ) / ( 𝐴 · 𝐴 ) ) )
157	155 156	eqtr4d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) = ( ( 𝐵 · 𝐶 ) / ( 𝐴 ↑ 2 ) ) )
158	146 154 157	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) = ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) )
159	158	oveq2d	⊢ ( 𝜑 → ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) = ( 9 · ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) ) )
160	143 145 159	3eqtr4rd	⊢ ( 𝜑 → ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) = ( ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) )
161	140 160	oveq12d	⊢ ( 𝜑 → ( ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) − ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ( 𝐴 ↑ 3 ) ) − ( ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) ) )
162	50 55 70 75	divsubdird	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ( 𝐴 ↑ 3 ) ) − ( ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) / ( 𝐴 ↑ 3 ) ) ) )
163	161 162	eqtr4d	⊢ ( 𝜑 → ( ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) − ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) )
164	151	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( 𝐴 ↑ 3 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( ( 𝐴 ↑ 2 ) · 𝐴 ) ) )
165	5 1 61 2 105	divcan5d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( ( 𝐴 ↑ 2 ) · 𝐴 ) ) = ( 𝐷 / 𝐴 ) )
166	164 165	eqtr2d	⊢ ( 𝜑 → ( 𝐷 / 𝐴 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( 𝐴 ↑ 3 ) ) )
167	166	oveq2d	⊢ ( 𝜑 → ( ; 2 7 · ( 𝐷 / 𝐴 ) ) = ( ; 2 7 · ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( 𝐴 ↑ 3 ) ) ) )
168	60	a1i	⊢ ( 𝜑 → ; 2 7 ∈ ℂ )
169	168 62 70 75	divassd	⊢ ( 𝜑 → ( ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝐴 ↑ 3 ) ) = ( ; 2 7 · ( ( ( 𝐴 ↑ 2 ) · 𝐷 ) / ( 𝐴 ↑ 3 ) ) ) )
170	167 169	eqtr4d	⊢ ( 𝜑 → ( ; 2 7 · ( 𝐷 / 𝐴 ) ) = ( ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝐴 ↑ 3 ) ) )
171	163 170	oveq12d	⊢ ( 𝜑 → ( ( ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) − ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) ) + ( ; 2 7 · ( 𝐷 / 𝐴 ) ) ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) / ( 𝐴 ↑ 3 ) ) + ( ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) / ( 𝐴 ↑ 3 ) ) ) )
172	135 136 171	3eqtr4d	⊢ ( 𝜑 → ( 𝑁 / ( 𝐴 ↑ 3 ) ) = ( ( ( 2 · ( ( 𝐵 / 𝐴 ) ↑ 3 ) ) − ( 9 · ( ( 𝐵 / 𝐴 ) · ( 𝐶 / 𝐴 ) ) ) ) + ( ; 2 7 · ( 𝐷 / 𝐴 ) ) ) )
173	7 1 13 2	divne0d	⊢ ( 𝜑 → ( 𝑇 / 𝐴 ) ≠ 0 )
174	39 40 41 6 42 80 81 121 134 172 173	mcubic	⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 3 ) + ( ( 𝐵 / 𝐴 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 𝐶 / 𝐴 ) · 𝑋 ) + ( 𝐷 / 𝐴 ) ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ) ) )
175		oveq1	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = ( 0 ↑ 3 ) )
176		3nn	⊢ 3 ∈ ℕ
177		0exp	⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 )
178	176 177	ax-mp	⊢ ( 0 ↑ 3 ) = 0
179	175 178	eqtrdi	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = 0 )
180		0ne1	⊢ 0 ≠ 1
181	180	a1i	⊢ ( 𝑟 = 0 → 0 ≠ 1 )
182	179 181	eqnetrd	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) ≠ 1 )
183	182	necon2i	⊢ ( ( 𝑟 ↑ 3 ) = 1 → 𝑟 ≠ 0 )
184		simprl	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ∈ ℂ )
185	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ∈ ℂ )
186	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝐴 ∈ ℂ )
187	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝐴 ≠ 0 )
188	184 185 186 187	divassd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 𝐴 ) = ( 𝑟 · ( 𝑇 / 𝐴 ) ) )
189	188	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · ( 𝑇 / 𝐴 ) ) = ( ( 𝑟 · 𝑇 ) / 𝐴 ) )
190	189	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) = ( ( 𝐵 / 𝐴 ) + ( ( 𝑟 · 𝑇 ) / 𝐴 ) ) )
191	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝐵 ∈ ℂ )
192	184 185	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ∈ ℂ )
193	191 192 186 187	divdird	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) / 𝐴 ) = ( ( 𝐵 / 𝐴 ) + ( ( 𝑟 · 𝑇 ) / 𝐴 ) ) )
194	190 193	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) = ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) / 𝐴 ) )
195	92	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑀 ∈ ℂ )
196	195 186 187	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / 𝐴 ) ∈ ℂ )
197		simprr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ≠ 0 )
198	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ≠ 0 )
199	184 185 197 198	mulne0d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ≠ 0 )
200	196 192 186 199 187	divcan7d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 𝐴 ) / 𝐴 ) / ( ( 𝑟 · 𝑇 ) / 𝐴 ) ) = ( ( 𝑀 / 𝐴 ) / ( 𝑟 · 𝑇 ) ) )
201	195 186 186 187 187	divdiv1d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / 𝐴 ) / 𝐴 ) = ( 𝑀 / ( 𝐴 · 𝐴 ) ) )
202	186	sqvald	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
203	202	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / ( 𝐴 ↑ 2 ) ) = ( 𝑀 / ( 𝐴 · 𝐴 ) ) )
204	201 203	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / 𝐴 ) / 𝐴 ) = ( 𝑀 / ( 𝐴 ↑ 2 ) ) )
205	204 188	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 𝐴 ) / 𝐴 ) / ( ( 𝑟 · 𝑇 ) / 𝐴 ) ) = ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) )
206	195 186 192 187 199	divdiv32d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / 𝐴 ) / ( 𝑟 · 𝑇 ) ) = ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 𝐴 ) )
207	200 205 206	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) = ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 𝐴 ) )
208	194 207	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) / 𝐴 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 𝐴 ) ) )
209	191 192	addcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝐵 + ( 𝑟 · 𝑇 ) ) ∈ ℂ )
210	195 192 199	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / ( 𝑟 · 𝑇 ) ) ∈ ℂ )
211	209 210 186 187	divdird	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 𝐴 ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) / 𝐴 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 𝐴 ) ) )
212	208 211	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 𝐴 ) )
213	212	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) = ( ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 𝐴 ) / 3 ) )
214	209 210	addcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ∈ ℂ )
215	87	a1i	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ∈ ℂ )
216		3ne0	⊢ 3 ≠ 0
217	216	a1i	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ≠ 0 )
218	214 186 215 187 217	divdiv1d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 𝐴 ) / 3 ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 𝐴 · 3 ) ) )
219		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℂ ) → ( 𝐴 · 3 ) = ( 3 · 𝐴 ) )
220	186 87 219	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝐴 · 3 ) = ( 3 · 𝐴 ) )
221	220	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 𝐴 · 3 ) ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) )
222	213 218 221	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) = ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) )
223	222	negeqd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) )
224	223	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )
225	224	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ 𝑟 ≠ 0 ) → ( 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )
226	183 225	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( 𝑟 ↑ 3 ) = 1 ) → ( 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )
227	226	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → ( ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ) ↔ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )
228	227	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( ( 𝐵 / 𝐴 ) + ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) + ( ( 𝑀 / ( 𝐴 ↑ 2 ) ) / ( 𝑟 · ( 𝑇 / 𝐴 ) ) ) ) / 3 ) ) ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )
229	38 174 228	3bitrd	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )

Metamath Proof Explorer

Theorem cubic2

Proof