mcubic

Description: Solutions to a monic cubic equation, a special case of cubic . (Contributed by Mario Carneiro, 24-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mcubic.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
2		mcubic.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3		mcubic.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
4		mcubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5		mcubic.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
6		mcubic.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑁 + 𝐺 ) / 2 ) )
7		mcubic.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
8		mcubic.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
9		mcubic.m	⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) )
10		mcubic.n	⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) )
11		mcubic.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
12	1	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
13		3cn	⊢ 3 ∈ ℂ
14		mulcl	⊢ ( ( 3 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 3 · 𝐶 ) ∈ ℂ )
15	13 2 14	sylancr	⊢ ( 𝜑 → ( 3 · 𝐶 ) ∈ ℂ )
16	12 15	subcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) ∈ ℂ )
17	9 16	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
18	13	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
19		3ne0	⊢ 3 ≠ 0
20	19	a1i	⊢ ( 𝜑 → 3 ≠ 0 )
21	17 18 20	divcld	⊢ ( 𝜑 → ( 𝑀 / 3 ) ∈ ℂ )
22	21	negcld	⊢ ( 𝜑 → - ( 𝑀 / 3 ) ∈ ℂ )
23		2cn	⊢ 2 ∈ ℂ
24		3nn0	⊢ 3 ∈ ℕ₀
25		expcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝐵 ↑ 3 ) ∈ ℂ )
26	1 24 25	sylancl	⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) ∈ ℂ )
27		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
28	23 26 27	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
29		9cn	⊢ 9 ∈ ℂ
30	1 2	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
31		mulcl	⊢ ( ( 9 ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 9 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
32	29 30 31	sylancr	⊢ ( 𝜑 → ( 9 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
33	28 32	subcld	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
34		2nn0	⊢ 2 ∈ ℕ₀
35		7nn	⊢ 7 ∈ ℕ
36	34 35	decnncl	⊢ ; 2 7 ∈ ℕ
37	36	nncni	⊢ ; 2 7 ∈ ℂ
38		mulcl	⊢ ( ( ; 2 7 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ; 2 7 · 𝐷 ) ∈ ℂ )
39	37 3 38	sylancr	⊢ ( 𝜑 → ( ; 2 7 · 𝐷 ) ∈ ℂ )
40	33 39	addcld	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) ∈ ℂ )
41	10 40	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
42	37	a1i	⊢ ( 𝜑 → ; 2 7 ∈ ℂ )
43	36	nnne0i	⊢ ; 2 7 ≠ 0
44	43	a1i	⊢ ( 𝜑 → ; 2 7 ≠ 0 )
45	41 42 44	divcld	⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) ∈ ℂ )
46	1 18 20	divcld	⊢ ( 𝜑 → ( 𝐵 / 3 ) ∈ ℂ )
47	4 46	addcld	⊢ ( 𝜑 → ( 𝑋 + ( 𝐵 / 3 ) ) ∈ ℂ )
48	5 18 20	divcld	⊢ ( 𝜑 → ( 𝑇 / 3 ) ∈ ℂ )
49	48	negcld	⊢ ( 𝜑 → - ( 𝑇 / 3 ) ∈ ℂ )
50		3nn	⊢ 3 ∈ ℕ
51	50	a1i	⊢ ( 𝜑 → 3 ∈ ℕ )
52		n2dvds3	⊢ ¬ 2 ∥ 3
53	52	a1i	⊢ ( 𝜑 → ¬ 2 ∥ 3 )
54		oexpneg	⊢ ( ( ( 𝑇 / 3 ) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - ( 𝑇 / 3 ) ↑ 3 ) = - ( ( 𝑇 / 3 ) ↑ 3 ) )
55	48 51 53 54	syl3anc	⊢ ( 𝜑 → ( - ( 𝑇 / 3 ) ↑ 3 ) = - ( ( 𝑇 / 3 ) ↑ 3 ) )
56	24	a1i	⊢ ( 𝜑 → 3 ∈ ℕ₀ )
57	5 18 20 56	expdivd	⊢ ( 𝜑 → ( ( 𝑇 / 3 ) ↑ 3 ) = ( ( 𝑇 ↑ 3 ) / ( 3 ↑ 3 ) ) )
58		3exp3	⊢ ( 3 ↑ 3 ) = ; 2 7
59	58	a1i	⊢ ( 𝜑 → ( 3 ↑ 3 ) = ; 2 7 )
60	6 59	oveq12d	⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) )
61	41 7	addcld	⊢ ( 𝜑 → ( 𝑁 + 𝐺 ) ∈ ℂ )
62		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
63		2ne0	⊢ 2 ≠ 0
64	63	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
65	61 62 42 64 44	divdiv32d	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) = ( ( ( 𝑁 + 𝐺 ) / ; 2 7 ) / 2 ) )
66	41 7	addcomd	⊢ ( 𝜑 → ( 𝑁 + 𝐺 ) = ( 𝐺 + 𝑁 ) )
67	66	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 + 𝐺 ) / ; 2 7 ) = ( ( 𝐺 + 𝑁 ) / ; 2 7 ) )
68	7 41 42 44	divdird	⊢ ( 𝜑 → ( ( 𝐺 + 𝑁 ) / ; 2 7 ) = ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) )
69	67 68	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 + 𝐺 ) / ; 2 7 ) = ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) )
70	69	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / ; 2 7 ) / 2 ) = ( ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) / 2 ) )
71	7 42 44	divcld	⊢ ( 𝜑 → ( 𝐺 / ; 2 7 ) ∈ ℂ )
72	71 45 62 64	divdird	⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) + ( 𝑁 / ; 2 7 ) ) / 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
73	65 70 72	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑁 + 𝐺 ) / 2 ) / ; 2 7 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
74	57 60 73	3eqtrd	⊢ ( 𝜑 → ( ( 𝑇 / 3 ) ↑ 3 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
75	74	negeqd	⊢ ( 𝜑 → - ( ( 𝑇 / 3 ) ↑ 3 ) = - ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
76	71	halfcld	⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ )
77	45	halfcld	⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) / 2 ) ∈ ℂ )
78	76 77	negdi2d	⊢ ( 𝜑 → - ( ( ( 𝐺 / ; 2 7 ) / 2 ) + ( ( 𝑁 / ; 2 7 ) / 2 ) ) = ( - ( ( 𝐺 / ; 2 7 ) / 2 ) − ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
79	55 75 78	3eqtrd	⊢ ( 𝜑 → ( - ( 𝑇 / 3 ) ↑ 3 ) = ( - ( ( 𝐺 / ; 2 7 ) / 2 ) − ( ( 𝑁 / ; 2 7 ) / 2 ) ) )
80	76	negcld	⊢ ( 𝜑 → - ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ )
81		sqneg	⊢ ( ( ( 𝐺 / ; 2 7 ) / 2 ) ∈ ℂ → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) )
82	76 81	syl	⊢ ( 𝜑 → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) )
83	71 62 64	sqdivd	⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
84	45 62 64	sqdivd	⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( 𝑁 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
85	41 42 44	sqdivd	⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) ↑ 2 ) = ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) )
86	85	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) )
87	84 86	eqtr2d	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) )
88		4cn	⊢ 4 ∈ ℂ
89	88	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
90		expcl	⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
91	17 24 90	sylancl	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
92	37	sqcli	⊢ ( ; 2 7 ↑ 2 ) ∈ ℂ
93	92	a1i	⊢ ( 𝜑 → ( ; 2 7 ↑ 2 ) ∈ ℂ )
94		sqne0	⊢ ( ; 2 7 ∈ ℂ → ( ( ; 2 7 ↑ 2 ) ≠ 0 ↔ ; 2 7 ≠ 0 ) )
95	42 94	syl	⊢ ( 𝜑 → ( ( ; 2 7 ↑ 2 ) ≠ 0 ↔ ; 2 7 ≠ 0 ) )
96	44 95	mpbird	⊢ ( 𝜑 → ( ; 2 7 ↑ 2 ) ≠ 0 )
97	89 91 93 96	divassd	⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) ) )
98	29	a1i	⊢ ( 𝜑 → 9 ∈ ℂ )
99		9nn	⊢ 9 ∈ ℕ
100	99	nnne0i	⊢ 9 ≠ 0
101	100	a1i	⊢ ( 𝜑 → 9 ≠ 0 )
102	17 98 101 56	expdivd	⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( 9 ↑ 3 ) ) )
103	23 13	mulcomi	⊢ ( 2 · 3 ) = ( 3 · 2 )
104	103	oveq2i	⊢ ( 3 ↑ ( 2 · 3 ) ) = ( 3 ↑ ( 3 · 2 ) )
105		expmul	⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ) → ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 ) )
106	13 34 24 105	mp3an	⊢ ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 )
107		expmul	⊢ ( ( 3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ) → ( 3 ↑ ( 3 · 2 ) ) = ( ( 3 ↑ 3 ) ↑ 2 ) )
108	13 24 34 107	mp3an	⊢ ( 3 ↑ ( 3 · 2 ) ) = ( ( 3 ↑ 3 ) ↑ 2 )
109	104 106 108	3eqtr3i	⊢ ( ( 3 ↑ 2 ) ↑ 3 ) = ( ( 3 ↑ 3 ) ↑ 2 )
110		sq3	⊢ ( 3 ↑ 2 ) = 9
111	110	oveq1i	⊢ ( ( 3 ↑ 2 ) ↑ 3 ) = ( 9 ↑ 3 )
112	58	oveq1i	⊢ ( ( 3 ↑ 3 ) ↑ 2 ) = ( ; 2 7 ↑ 2 )
113	109 111 112	3eqtr3i	⊢ ( 9 ↑ 3 ) = ( ; 2 7 ↑ 2 )
114	113	oveq2i	⊢ ( ( 𝑀 ↑ 3 ) / ( 9 ↑ 3 ) ) = ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) )
115	102 114	eqtrdi	⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) = ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) )
116	115	oveq2d	⊢ ( 𝜑 → ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) = ( 4 · ( ( 𝑀 ↑ 3 ) / ( ; 2 7 ↑ 2 ) ) ) )
117	97 116	eqtr4d	⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) = ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) )
118	117	oveq1d	⊢ ( 𝜑 → ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) )
119		sq2	⊢ ( 2 ↑ 2 ) = 4
120	119	oveq2i	⊢ ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) = ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / 4 )
121	17 98 101	divcld	⊢ ( 𝜑 → ( 𝑀 / 9 ) ∈ ℂ )
122		expcl	⊢ ( ( ( 𝑀 / 9 ) ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( ( 𝑀 / 9 ) ↑ 3 ) ∈ ℂ )
123	121 24 122	sylancl	⊢ ( 𝜑 → ( ( 𝑀 / 9 ) ↑ 3 ) ∈ ℂ )
124		4ne0	⊢ 4 ≠ 0
125	124	a1i	⊢ ( 𝜑 → 4 ≠ 0 )
126	123 89 125	divcan3d	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / 4 ) = ( ( 𝑀 / 9 ) ↑ 3 ) )
127	120 126	syl5eq	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑀 / 9 ) ↑ 3 ) ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 / 9 ) ↑ 3 ) )
128	118 127	eqtrd	⊢ ( 𝜑 → ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 / 9 ) ↑ 3 ) )
129	87 128	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) − ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) − ( ( 𝑀 / 9 ) ↑ 3 ) ) )
130	41	sqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
131	130 93 96	divcld	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) ∈ ℂ )
132		mulcl	⊢ ( ( 4 ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
133	88 91 132	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
134	133 93 96	divcld	⊢ ( 𝜑 → ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ∈ ℂ )
135	23	sqcli	⊢ ( 2 ↑ 2 ) ∈ ℂ
136	135	a1i	⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℂ )
137	119 124	eqnetri	⊢ ( 2 ↑ 2 ) ≠ 0
138	137	a1i	⊢ ( 𝜑 → ( 2 ↑ 2 ) ≠ 0 )
139	131 134 136 138	divsubdird	⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) − ( ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) / ( 2 ↑ 2 ) ) ) )
140	77	sqcld	⊢ ( 𝜑 → ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) ∈ ℂ )
141	140 123	negsubd	⊢ ( 𝜑 → ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) − ( ( 𝑀 / 9 ) ↑ 3 ) ) )
142	129 139 141	3eqtr4d	⊢ ( 𝜑 → ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) )
143	7 42 44	sqdivd	⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) ↑ 2 ) = ( ( 𝐺 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) )
144	8	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ; 2 7 ↑ 2 ) ) )
145	130 133 93 96	divsubdird	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) / ( ; 2 7 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) )
146	143 144 145	3eqtrd	⊢ ( 𝜑 → ( ( 𝐺 / ; 2 7 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) )
147	146	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 ↑ 2 ) / ( ; 2 7 ↑ 2 ) ) − ( ( 4 · ( 𝑀 ↑ 3 ) ) / ( ; 2 7 ↑ 2 ) ) ) / ( 2 ↑ 2 ) ) )
148		oexpneg	⊢ ( ( ( 𝑀 / 9 ) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - ( 𝑀 / 9 ) ↑ 3 ) = - ( ( 𝑀 / 9 ) ↑ 3 ) )
149	121 51 53 148	syl3anc	⊢ ( 𝜑 → ( - ( 𝑀 / 9 ) ↑ 3 ) = - ( ( 𝑀 / 9 ) ↑ 3 ) )
150	149	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + - ( ( 𝑀 / 9 ) ↑ 3 ) ) )
151	142 147 150	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐺 / ; 2 7 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) )
152	82 83 151	3eqtrd	⊢ ( 𝜑 → ( - ( ( 𝐺 / ; 2 7 ) / 2 ) ↑ 2 ) = ( ( ( ( 𝑁 / ; 2 7 ) / 2 ) ↑ 2 ) + ( - ( 𝑀 / 9 ) ↑ 3 ) ) )
153	17 18 18 20 20	divdiv1d	⊢ ( 𝜑 → ( ( 𝑀 / 3 ) / 3 ) = ( 𝑀 / ( 3 · 3 ) ) )
154		3t3e9	⊢ ( 3 · 3 ) = 9
155	154	oveq2i	⊢ ( 𝑀 / ( 3 · 3 ) ) = ( 𝑀 / 9 )
156	153 155	eqtrdi	⊢ ( 𝜑 → ( ( 𝑀 / 3 ) / 3 ) = ( 𝑀 / 9 ) )
157	156	negeqd	⊢ ( 𝜑 → - ( ( 𝑀 / 3 ) / 3 ) = - ( 𝑀 / 9 ) )
158	21 18 20	divnegd	⊢ ( 𝜑 → - ( ( 𝑀 / 3 ) / 3 ) = ( - ( 𝑀 / 3 ) / 3 ) )
159	157 158	eqtr3d	⊢ ( 𝜑 → - ( 𝑀 / 9 ) = ( - ( 𝑀 / 3 ) / 3 ) )
160		eqidd	⊢ ( 𝜑 → ( ( 𝑁 / ; 2 7 ) / 2 ) = ( ( 𝑁 / ; 2 7 ) / 2 ) )
161	5 18 11 20	divne0d	⊢ ( 𝜑 → ( 𝑇 / 3 ) ≠ 0 )
162	48 161	negne0d	⊢ ( 𝜑 → - ( 𝑇 / 3 ) ≠ 0 )
163	22 45 47 49 79 80 152 159 160 162	dcubic	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ) )
164		binom3	⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝐵 / 3 ) ∈ ℂ ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
165	4 46 164	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
166	4	sqcld	⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
167	18 166 46	mul12d	⊢ ( 𝜑 → ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) = ( ( 𝑋 ↑ 2 ) · ( 3 · ( 𝐵 / 3 ) ) ) )
168	1 18 20	divcan2d	⊢ ( 𝜑 → ( 3 · ( 𝐵 / 3 ) ) = 𝐵 )
169	168	oveq2d	⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · ( 3 · ( 𝐵 / 3 ) ) ) = ( ( 𝑋 ↑ 2 ) · 𝐵 ) )
170	166 1	mulcomd	⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · 𝐵 ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) )
171	167 169 170	3eqtrd	⊢ ( 𝜑 → ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) = ( 𝐵 · ( 𝑋 ↑ 2 ) ) )
172	171	oveq2d	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) = ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) )
173	172	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( 3 · ( ( 𝑋 ↑ 2 ) · ( 𝐵 / 3 ) ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
174	165 173	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
175	174	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) )
176		expcl	⊢ ( ( 𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( 𝑋 ↑ 3 ) ∈ ℂ )
177	4 24 176	sylancl	⊢ ( 𝜑 → ( 𝑋 ↑ 3 ) ∈ ℂ )
178	1 166	mulcld	⊢ ( 𝜑 → ( 𝐵 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
179	177 178	addcld	⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
180	46	sqcld	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) ∈ ℂ )
181	4 180	mulcld	⊢ ( 𝜑 → ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ∈ ℂ )
182	18 181	mulcld	⊢ ( 𝜑 → ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ∈ ℂ )
183		expcl	⊢ ( ( ( 𝐵 / 3 ) ∈ ℂ ∧ 3 ∈ ℕ₀ ) → ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ )
184	46 24 183	sylancl	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ )
185	182 184	addcld	⊢ ( 𝜑 → ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ∈ ℂ )
186	22 47	mulcld	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) ∈ ℂ )
187	186 45	addcld	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ∈ ℂ )
188	179 185 187	addassd	⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) ) )
189	22 4 46	adddid	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) = ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) )
190	189	oveq1d	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) )
191	22 4	mulcld	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) ∈ ℂ )
192	22 46	mulcld	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ∈ ℂ )
193	191 192 45	addassd	⊢ ( 𝜑 → ( ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) ) )
194	9	oveq1d	⊢ ( 𝜑 → ( 𝑀 / 3 ) = ( ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) / 3 ) )
195	12 15 18 20	divsubdird	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) − ( 3 · 𝐶 ) ) / 3 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − ( ( 3 · 𝐶 ) / 3 ) ) )
196	2 18 20	divcan3d	⊢ ( 𝜑 → ( ( 3 · 𝐶 ) / 3 ) = 𝐶 )
197	196	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) − ( ( 3 · 𝐶 ) / 3 ) ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) )
198	194 195 197	3eqtrd	⊢ ( 𝜑 → ( 𝑀 / 3 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) )
199	198	negeqd	⊢ ( 𝜑 → - ( 𝑀 / 3 ) = - ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) )
200	12 18 20	divcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) / 3 ) ∈ ℂ )
201	200 2	negsubdi2d	⊢ ( 𝜑 → - ( ( ( 𝐵 ↑ 2 ) / 3 ) − 𝐶 ) = ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) )
202	199 201	eqtrd	⊢ ( 𝜑 → - ( 𝑀 / 3 ) = ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) )
203	202	oveq1d	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) = ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · 𝑋 ) )
204	2 200 4	subdird	⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · 𝑋 ) = ( ( 𝐶 · 𝑋 ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) ) )
205	200 4	mulcomd	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) = ( 𝑋 · ( ( 𝐵 ↑ 2 ) / 3 ) ) )
206	13	sqvali	⊢ ( 3 ↑ 2 ) = ( 3 · 3 )
207	206	oveq2i	⊢ ( ( 𝐵 ↑ 2 ) / ( 3 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) / ( 3 · 3 ) )
208	1 18 20	sqdivd	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( 3 ↑ 2 ) ) )
209	12 18 18 20 20	divdiv1d	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) = ( ( 𝐵 ↑ 2 ) / ( 3 · 3 ) ) )
210	207 208 209	3eqtr4a	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) )
211	210	oveq2d	⊢ ( 𝜑 → ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) = ( 3 · ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) ) )
212	200 18 20	divcan2d	⊢ ( 𝜑 → ( 3 · ( ( ( 𝐵 ↑ 2 ) / 3 ) / 3 ) ) = ( ( 𝐵 ↑ 2 ) / 3 ) )
213	211 212	eqtrd	⊢ ( 𝜑 → ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) / 3 ) )
214	213	oveq2d	⊢ ( 𝜑 → ( 𝑋 · ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) = ( 𝑋 · ( ( 𝐵 ↑ 2 ) / 3 ) ) )
215	4 18 180	mul12d	⊢ ( 𝜑 → ( 𝑋 · ( 3 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) = ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) )
216	205 214 215	3eqtr2d	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) = ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) )
217	216	oveq2d	⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · 𝑋 ) ) = ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) )
218	203 204 217	3eqtrd	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · 𝑋 ) = ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) )
219	202	oveq1d	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) = ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · ( 𝐵 / 3 ) ) )
220	2 200 46	subdird	⊢ ( 𝜑 → ( ( 𝐶 − ( ( 𝐵 ↑ 2 ) / 3 ) ) · ( 𝐵 / 3 ) ) = ( ( 𝐶 · ( 𝐵 / 3 ) ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) ) )
221	2 1 18 20	divassd	⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) / 3 ) = ( 𝐶 · ( 𝐵 / 3 ) ) )
222	2 1	mulcomd	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
223	222	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) / 3 ) = ( ( 𝐵 · 𝐶 ) / 3 ) )
224	221 223	eqtr3d	⊢ ( 𝜑 → ( 𝐶 · ( 𝐵 / 3 ) ) = ( ( 𝐵 · 𝐶 ) / 3 ) )
225	12 18 1 18 20 20	divmuldivd	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) = ( ( ( 𝐵 ↑ 2 ) · 𝐵 ) / ( 3 · 3 ) ) )
226		df-3	⊢ 3 = ( 2 + 1 )
227	226	oveq2i	⊢ ( 𝐵 ↑ 3 ) = ( 𝐵 ↑ ( 2 + 1 ) )
228		expp1	⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀ ) → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) )
229	1 34 228	sylancl	⊢ ( 𝜑 → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) )
230	227 229	eqtr2id	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · 𝐵 ) = ( 𝐵 ↑ 3 ) )
231	154	a1i	⊢ ( 𝜑 → ( 3 · 3 ) = 9 )
232	230 231	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) · 𝐵 ) / ( 3 · 3 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) )
233	225 232	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) )
234	224 233	oveq12d	⊢ ( 𝜑 → ( ( 𝐶 · ( 𝐵 / 3 ) ) − ( ( ( 𝐵 ↑ 2 ) / 3 ) · ( 𝐵 / 3 ) ) ) = ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) )
235	219 220 234	3eqtrd	⊢ ( 𝜑 → ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) = ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) )
236	10	oveq1d	⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) / ; 2 7 ) )
237	33 39 42 44	divdird	⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · 𝐷 ) ) / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) + ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) ) )
238	28 32 42 44	divsubdird	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) ) )
239		9t3e27	⊢ ( 9 · 3 ) = ; 2 7
240	239	oveq2i	⊢ ( ( 9 · ( 𝐵 · 𝐶 ) ) / ( 9 · 3 ) ) = ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 )
241	30 18 98 20 101	divcan5d	⊢ ( 𝜑 → ( ( 9 · ( 𝐵 · 𝐶 ) ) / ( 9 · 3 ) ) = ( ( 𝐵 · 𝐶 ) / 3 ) )
242	240 241	eqtr3id	⊢ ( 𝜑 → ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) = ( ( 𝐵 · 𝐶 ) / 3 ) )
243	242	oveq2d	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 9 · ( 𝐵 · 𝐶 ) ) / ; 2 7 ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) )
244	238 243	eqtrd	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) )
245	3 42 44	divcan3d	⊢ ( 𝜑 → ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) = 𝐷 )
246	244 245	oveq12d	⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( 9 · ( 𝐵 · 𝐶 ) ) ) / ; 2 7 ) + ( ( ; 2 7 · 𝐷 ) / ; 2 7 ) ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) )
247	236 237 246	3eqtrd	⊢ ( 𝜑 → ( 𝑁 / ; 2 7 ) = ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) )
248	235 247	oveq12d	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) )
249	26 98 101	divcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / 9 ) ∈ ℂ )
250	28 42 44	divcld	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ∈ ℂ )
251	249 250	negsubdi2d	⊢ ( 𝜑 → - ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) )
252	1 18 20 56	expdivd	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) )
253	58	oveq2i	⊢ ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( 𝐵 ↑ 3 ) / ; 2 7 )
254		ax-1cn	⊢ 1 ∈ ℂ
255		2p1e3	⊢ ( 2 + 1 ) = 3
256	13 23 254 255	subaddrii	⊢ ( 3 − 2 ) = 1
257	256	oveq1i	⊢ ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( 1 · ( 𝐵 ↑ 3 ) )
258	26	mulid2d	⊢ ( 𝜑 → ( 1 · ( 𝐵 ↑ 3 ) ) = ( 𝐵 ↑ 3 ) )
259	257 258	syl5eq	⊢ ( 𝜑 → ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( 𝐵 ↑ 3 ) )
260	18 62 26	subdird	⊢ ( 𝜑 → ( ( 3 − 2 ) · ( 𝐵 ↑ 3 ) ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) )
261	259 260	eqtr3d	⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) )
262	261	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) / ; 2 7 ) )
263		mulcl	⊢ ( ( 3 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 3 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
264	13 26 263	sylancr	⊢ ( 𝜑 → ( 3 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
265	264 28 42 44	divsubdird	⊢ ( 𝜑 → ( ( ( 3 · ( 𝐵 ↑ 3 ) ) − ( 2 · ( 𝐵 ↑ 3 ) ) ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
266	262 265	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ; 2 7 ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
267	253 266	syl5eq	⊢ ( 𝜑 → ( ( 𝐵 ↑ 3 ) / ( 3 ↑ 3 ) ) = ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
268	29 13 239	mulcomli	⊢ ( 3 · 9 ) = ; 2 7
269	268	oveq2i	⊢ ( ( 3 · ( 𝐵 ↑ 3 ) ) / ( 3 · 9 ) ) = ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 )
270	26 98 18 101 20	divcan5d	⊢ ( 𝜑 → ( ( 3 · ( 𝐵 ↑ 3 ) ) / ( 3 · 9 ) ) = ( ( 𝐵 ↑ 3 ) / 9 ) )
271	269 270	eqtr3id	⊢ ( 𝜑 → ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) = ( ( 𝐵 ↑ 3 ) / 9 ) )
272	271	oveq1d	⊢ ( 𝜑 → ( ( ( 3 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) = ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
273	252 267 272	3eqtrd	⊢ ( 𝜑 → ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
274	273	negeqd	⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) = - ( ( ( 𝐵 ↑ 3 ) / 9 ) − ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) ) )
275	30 18 20	divcld	⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) / 3 ) ∈ ℂ )
276	275 249 250	npncan3d	⊢ ( 𝜑 → ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) )
277	251 274 276	3eqtr4d	⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) )
278	277	oveq1d	⊢ ( 𝜑 → ( - ( ( 𝐵 / 3 ) ↑ 3 ) + 𝐷 ) = ( ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) + 𝐷 ) )
279	184	negcld	⊢ ( 𝜑 → - ( ( 𝐵 / 3 ) ↑ 3 ) ∈ ℂ )
280	279 3	addcomd	⊢ ( 𝜑 → ( - ( ( 𝐵 / 3 ) ↑ 3 ) + 𝐷 ) = ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) )
281	235 192	eqeltrrd	⊢ ( 𝜑 → ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) ∈ ℂ )
282	250 275	subcld	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ∈ ℂ )
283	281 282 3	addassd	⊢ ( 𝜑 → ( ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) ) + 𝐷 ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) )
284	278 280 283	3eqtr3d	⊢ ( 𝜑 → ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) = ( ( ( ( 𝐵 · 𝐶 ) / 3 ) − ( ( 𝐵 ↑ 3 ) / 9 ) ) + ( ( ( ( 2 · ( 𝐵 ↑ 3 ) ) / ; 2 7 ) − ( ( 𝐵 · 𝐶 ) / 3 ) ) + 𝐷 ) ) )
285	3 184	negsubd	⊢ ( 𝜑 → ( 𝐷 + - ( ( 𝐵 / 3 ) ↑ 3 ) ) = ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) )
286	248 284 285	3eqtr2d	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) = ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) )
287	218 286	oveq12d	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · 𝑋 ) + ( ( - ( 𝑀 / 3 ) · ( 𝐵 / 3 ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
288	190 193 287	3eqtrd	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
289	2 4	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ℂ )
290	289 3 182 184	addsub4d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) = ( ( ( 𝐶 · 𝑋 ) − ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) ) + ( 𝐷 − ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
291	288 290	eqtr4d	⊢ ( 𝜑 → ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) = ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) )
292	291	oveq2d	⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) )
293	289 3	addcld	⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) + 𝐷 ) ∈ ℂ )
294	185 293	pncan3d	⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) − ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
295	292 294	eqtrd	⊢ ( 𝜑 → ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
296	295	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( ( 3 · ( 𝑋 · ( ( 𝐵 / 3 ) ↑ 2 ) ) ) + ( ( 𝐵 / 3 ) ↑ 3 ) ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
297	175 188 296	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
298	297	eqeq1d	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( 𝐵 / 3 ) ) ↑ 3 ) + ( ( - ( 𝑀 / 3 ) · ( 𝑋 + ( 𝐵 / 3 ) ) ) + ( 𝑁 / ; 2 7 ) ) ) = 0 ↔ ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ) )
299		oveq1	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = ( 0 ↑ 3 ) )
300		0exp	⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 )
301	50 300	ax-mp	⊢ ( 0 ↑ 3 ) = 0
302	299 301	eqtrdi	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = 0 )
303		0ne1	⊢ 0 ≠ 1
304	303	a1i	⊢ ( 𝑟 = 0 → 0 ≠ 1 )
305	302 304	eqnetrd	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) ≠ 1 )
306	305	necon2i	⊢ ( ( 𝑟 ↑ 3 ) = 1 → 𝑟 ≠ 0 )
307		eqcom	⊢ ( 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = 𝑋 )
308	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝐵 ∈ ℂ )
309		simprl	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ∈ ℂ )
310	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ∈ ℂ )
311	309 310	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ∈ ℂ )
312	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑀 ∈ ℂ )
313		simprr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑟 ≠ 0 )
314	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑇 ≠ 0 )
315	309 310 313 314	mulne0d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · 𝑇 ) ≠ 0 )
316	312 311 315	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / ( 𝑟 · 𝑇 ) ) ∈ ℂ )
317	311 316	addcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ∈ ℂ )
318	13	a1i	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ∈ ℂ )
319	19	a1i	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 3 ≠ 0 )
320	308 317 318 319	divdird	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) / 3 ) = ( ( 𝐵 / 3 ) + ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
321	308 311 316	addassd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) = ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
322	321	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝐵 + ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) / 3 ) )
323	46	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝐵 / 3 ) ∈ ℂ )
324	317 318 319	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ∈ ℂ )
325	323 324	subnegd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) = ( ( 𝐵 / 3 ) + ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
326	320 322 325	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
327	326	negeqd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = - ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
328	324	negcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ∈ ℂ )
329	323 328	negsubdi2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝐵 / 3 ) − - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) = ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) )
330	327 329	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) )
331	330	eqeq1d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = 𝑋 ↔ ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ) )
332	307 331	syl5bb	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ) )
333	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → 𝑋 ∈ ℂ )
334	328 323 333	subadd2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) − ( 𝐵 / 3 ) ) = 𝑋 ↔ ( 𝑋 + ( 𝐵 / 3 ) ) = - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
335	311 316 318 319	divdird	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) )
336	335	negeqd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = - ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) )
337	311 318 319	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) ∈ ℂ )
338	316 318 319	divcld	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ∈ ℂ )
339	337 338	negdi2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) / 3 ) + ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) = ( - ( ( 𝑟 · 𝑇 ) / 3 ) − ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) )
340	309 310 318 319	divassd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) = ( 𝑟 · ( 𝑇 / 3 ) ) )
341	340	negeqd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝑟 · 𝑇 ) / 3 ) = - ( 𝑟 · ( 𝑇 / 3 ) ) )
342	48	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑇 / 3 ) ∈ ℂ )
343	309 342	mulneg2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑟 · - ( 𝑇 / 3 ) ) = - ( 𝑟 · ( 𝑇 / 3 ) ) )
344	341 343	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( 𝑟 · 𝑇 ) / 3 ) = ( 𝑟 · - ( 𝑇 / 3 ) ) )
345	312 311 318 315 319	divdiv32d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( ( 𝑀 / 3 ) / ( 𝑟 · 𝑇 ) ) )
346	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / 3 ) ∈ ℂ )
347	346 311 318 315 319	divcan7d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 3 ) / ( 𝑟 · 𝑇 ) ) )
348	156	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) )
349	348	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( ( 𝑀 / 3 ) / 3 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) )
350	345 347 349	3eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) )
351	121	adantr	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( 𝑀 / 9 ) ∈ ℂ )
352	311 318 315 319	divne0d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑟 · 𝑇 ) / 3 ) ≠ 0 )
353	351 337 352	div2negd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( 𝑀 / 9 ) / - ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( ( 𝑀 / 9 ) / ( ( 𝑟 · 𝑇 ) / 3 ) ) )
354	344	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( 𝑀 / 9 ) / - ( ( 𝑟 · 𝑇 ) / 3 ) ) = ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) )
355	350 353 354	3eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) = ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) )
356	344 355	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( - ( ( 𝑟 · 𝑇 ) / 3 ) − ( ( 𝑀 / ( 𝑟 · 𝑇 ) ) / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) )
357	336 339 356	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) )
358	357	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = - ( ( ( 𝑟 · 𝑇 ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ↔ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) )
359	332 334 358	3bitrrd	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℂ ∧ 𝑟 ≠ 0 ) ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
360	359	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ 𝑟 ≠ 0 ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
361	306 360	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( 𝑟 ↑ 3 ) = 1 ) → ( ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ↔ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) )
362	361	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → ( ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ↔ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) )
363	362	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ ( 𝑋 + ( 𝐵 / 3 ) ) = ( ( 𝑟 · - ( 𝑇 / 3 ) ) − ( - ( 𝑀 / 9 ) / ( 𝑟 · - ( 𝑇 / 3 ) ) ) ) ) ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) )
364	163 298 363	3bitr3d	⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 3 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / 3 ) ) ) )

Metamath Proof Explorer

Theorem mcubic

Proof