Theorem mcubic 23304

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

Hypotheses

Ref	Expression
mcubic.b	|- ( ph -> B e. CC )
mcubic.c	|- ( ph -> C e. CC )
mcubic.d	|- ( ph -> D e. CC )
mcubic.x	|- ( ph -> X e. CC )
mcubic.t	|- ( ph -> T e. CC )
mcubic.3	|- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
mcubic.g	|- ( ph -> G e. CC )
mcubic.2	|- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
mcubic.m	|- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. C ) ) )
mcubic.n	|- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) )
mcubic.0	|- ( ph -> T =/= 0 )

Assertion

Ref	Expression
mcubic	|- ( ph -> ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )

Distinct variable groups:   B, r   M, r   N, r   ph, r   T, r   X, r

Allowed substitution hints:   C( r)   D( r)   G( r)

Proof of Theorem mcubic

Step	Hyp	Ref	Expression
1		mcubic.m	. . . . . 6 |- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. C ) ) )
2		mcubic.b	. . . . . . . 8 |- ( ph -> B e. CC )
3	2	sqcld 12311	. . . . . . 7 |- ( ph -> ( B ^ 2 ) e. CC )
4		3cn 10631	. . . . . . . 8 |- 3 e. CC
5		mcubic.c	. . . . . . . 8 |- ( ph -> C e. CC )
6		mulcl 9593	. . . . . . . 8 |- ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
7	4, 5, 6	sylancr 663	. . . . . . 7 |- ( ph -> ( 3 x. C ) e. CC )
8	3, 7	subcld 9950	. . . . . 6 |- ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
9	1, 8	eqeltrd 2545	. . . . 5 |- ( ph -> M e. CC )
10	4	a1i 11	. . . . 5 |- ( ph -> 3 e. CC )
11		3ne0 10651	. . . . . 6 |- 3 =/= 0
12	11	a1i 11	. . . . 5 |- ( ph -> 3 =/= 0 )
13	9, 10, 12	divcld 10341	. . . 4 |- ( ph -> ( M / 3 ) e. CC )
14	13	negcld 9937	. . 3 |- ( ph -> -u ( M / 3 ) e. CC )
15		mcubic.n	. . . . 5 |- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) )
16		2cn 10627	. . . . . . . 8 |- 2 e. CC
17		3nn0 10834	. . . . . . . . 9 |- 3 e. NN0
18		expcl 12187	. . . . . . . . 9 |- ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
19	2, 17, 18	sylancl 662	. . . . . . . 8 |- ( ph -> ( B ^ 3 ) e. CC )
20		mulcl 9593	. . . . . . . 8 |- ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
21	16, 19, 20	sylancr 663	. . . . . . 7 |- ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
22		9cn 10644	. . . . . . . 8 |- 9 e. CC
23	2, 5	mulcld 9633	. . . . . . . 8 |- ( ph -> ( B x. C ) e. CC )
24		mulcl 9593	. . . . . . . 8 |- ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
25	22, 23, 24	sylancr 663	. . . . . . 7 |- ( ph -> ( 9 x. ( B x. C ) ) e. CC )
26	21, 25	subcld 9950	. . . . . 6 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
27		2nn0 10833	. . . . . . . . 9 |- 2 e. NN0
28		7nn 10719	. . . . . . . . 9 |- 7 e. NN
29	27, 28	decnncl 11013	. . . . . . . 8 |- ; 2 7 e. NN
30	29	nncni 10566	. . . . . . 7 |- ; 2 7 e. CC
31		mcubic.d	. . . . . . 7 |- ( ph -> D e. CC )
32		mulcl 9593	. . . . . . 7 |- ( (; 2 7 e. CC /\ D e. CC ) -> (; 2 7 x. D ) e. CC )
33	30, 31, 32	sylancr 663	. . . . . 6 |- ( ph -> (; 2 7 x. D ) e. CC )
34	26, 33	addcld 9632	. . . . 5 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) e. CC )
35	15, 34	eqeltrd 2545	. . . 4 |- ( ph -> N e. CC )
36	30	a1i 11	. . . 4 |- ( ph -> ; 2 7 e. CC )
37	29	nnne0i 10591	. . . . 5 |- ; 2 7 =/= 0
38	37	a1i 11	. . . 4 |- ( ph -> ; 2 7 =/= 0 )
39	35, 36, 38	divcld 10341	. . 3 |- ( ph -> ( N / ; 2 7 ) e. CC )
40		mcubic.x	. . . 4 |- ( ph -> X e. CC )
41	2, 10, 12	divcld 10341	. . . 4 |- ( ph -> ( B / 3 ) e. CC )
42	40, 41	addcld 9632	. . 3 |- ( ph -> ( X + ( B / 3 ) ) e. CC )
43		mcubic.t	. . . . 5 |- ( ph -> T e. CC )
44	43, 10, 12	divcld 10341	. . . 4 |- ( ph -> ( T / 3 ) e. CC )
45	44	negcld 9937	. . 3 |- ( ph -> -u ( T / 3 ) e. CC )
46		3nn 10715	. . . . . 6 |- 3 e. NN
47	46	a1i 11	. . . . 5 |- ( ph -> 3 e. NN )
48		2nn 10714	. . . . . . 7 |- 2 e. NN
49		1nn0 10832	. . . . . . 7 |- 1 e. NN0
50		1nn 10567	. . . . . . 7 |- 1 e. NN
51		2t1e2 10705	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
52	51	oveq1i 6306	. . . . . . . 8 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
53		2p1e3 10680	. . . . . . . 8 |- ( 2 + 1 ) = 3
54	52, 53	eqtri 2486	. . . . . . 7 |- ( ( 2 x. 1 ) + 1 ) = 3
55		1lt2 10723	. . . . . . 7 |- 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 14080	. . . . . 6 |- -. 2 || 3
57	56	a1i 11	. . . . 5 |- ( ph -> -. 2 || 3 )
58		oexpneg 14061	. . . . 5 |- ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
59	44, 47, 57, 58	syl3anc 1228	. . . 4 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
60	17	a1i 11	. . . . . . 7 |- ( ph -> 3 e. NN0 )
61	43, 10, 12, 60	expdivd 12327	. . . . . 6 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
62		mcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
63		3exp3 14588	. . . . . . . 8 |- ( 3 ^ 3 ) = ; 2 7
64	63	a1i 11	. . . . . . 7 |- ( ph -> ( 3 ^ 3 ) = ; 2 7 )
65	62, 64	oveq12d 6314	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
66		mcubic.g	. . . . . . . . 9 |- ( ph -> G e. CC )
67	35, 66	addcld 9632	. . . . . . . 8 |- ( ph -> ( N + G ) e. CC )
68		2cnd 10629	. . . . . . . 8 |- ( ph -> 2 e. CC )
69		2ne0 10649	. . . . . . . . 9 |- 2 =/= 0
70	69	a1i 11	. . . . . . . 8 |- ( ph -> 2 =/= 0 )
71	67, 68, 36, 70, 38	divdiv32d 10366	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
72	35, 66	addcomd 9799	. . . . . . . . . 10 |- ( ph -> ( N + G ) = ( G + N ) )
73	72	oveq1d 6311	. . . . . . . . 9 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
74	66, 35, 36, 38	divdird 10379	. . . . . . . . 9 |- ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
75	73, 74	eqtrd 2498	. . . . . . . 8 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
76	75	oveq1d 6311	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
77	66, 36, 38	divcld 10341	. . . . . . . 8 |- ( ph -> ( G / ; 2 7 ) e. CC )
78	77, 39, 68, 70	divdird 10379	. . . . . . 7 |- ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
79	71, 76, 78	3eqtrd 2502	. . . . . 6 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
80	61, 65, 79	3eqtrd 2502	. . . . 5 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
81	80	negeqd 9833	. . . 4 |- ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
82	77	halfcld 10804	. . . . 5 |- ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
83	39	halfcld 10804	. . . . 5 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
84	82, 83	negdi2d 9964	. . . 4 |- ( ph -> -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
85	59, 81, 84	3eqtrd 2502	. . 3 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
86	82	negcld 9937	. . 3 |- ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
87		sqneg 12231	. . . . 5 |- ( ( ( G / ; 2 7 ) / 2 ) e. CC -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
88	82, 87	syl 16	. . . 4 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
89	77, 68, 70	sqdivd 12326	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
90	39, 68, 70	sqdivd 12326	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
91	35, 36, 38	sqdivd 12326	. . . . . . . . 9 |- ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) )
92	91	oveq1d 6311	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
93	90, 92	eqtr2d 2499	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
94		4cn 10634	. . . . . . . . . . . 12 |- 4 e. CC
95	94	a1i 11	. . . . . . . . . . 11 |- ( ph -> 4 e. CC )
96		expcl 12187	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
97	9, 17, 96	sylancl 662	. . . . . . . . . . 11 |- ( ph -> ( M ^ 3 ) e. CC )
98	30	sqcli 12251	. . . . . . . . . . . 12 |- (; 2 7 ^ 2 ) e. CC
99	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) e. CC )
100		sqne0 12237	. . . . . . . . . . . . 13 |- (; 2 7 e. CC -> ( (; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
101	36, 100	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( (; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
102	38, 101	mpbird 232	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) =/= 0 )
103	95, 97, 99, 102	divassd 10376	. . . . . . . . . 10 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
104	22	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 e. CC )
105		9nn 10721	. . . . . . . . . . . . . . 15 |- 9 e. NN
106	105	nnne0i 10591	. . . . . . . . . . . . . 14 |- 9 =/= 0
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 =/= 0 )
108	9, 104, 107, 60	expdivd 12327	. . . . . . . . . . . 12 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
109	16, 4	mulcomi 9619	. . . . . . . . . . . . . . . 16 |- ( 2 x. 3 ) = ( 3 x. 2 )
110	109	oveq2i 6307	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
111		expmul 12214	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
112	4, 27, 17, 111	mp3an 1324	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
113		expmul 12214	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
114	4, 17, 27, 113	mp3an 1324	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
115	110, 112, 114	3eqtr3i 2494	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
116		sq3 12268	. . . . . . . . . . . . . . 15 |- ( 3 ^ 2 ) = 9
117	116	oveq1i 6306	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
118	63	oveq1i 6306	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 3 ) ^ 2 ) = (; 2 7 ^ 2 )
119	115, 117, 118	3eqtr3i 2494	. . . . . . . . . . . . 13 |- ( 9 ^ 3 ) = (; 2 7 ^ 2 )
120	119	oveq2i 6307	. . . . . . . . . . . 12 |- ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) )
121	108, 120	syl6eq 2514	. . . . . . . . . . 11 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) )
122	121	oveq2d 6312	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
123	103, 122	eqtr4d 2501	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
124	123	oveq1d 6311	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
125		sq2 12267	. . . . . . . . . 10 |- ( 2 ^ 2 ) = 4
126	125	oveq2i 6307	. . . . . . . . 9 |- ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
127	9, 104, 107	divcld 10341	. . . . . . . . . . 11 |- ( ph -> ( M / 9 ) e. CC )
128		expcl 12187	. . . . . . . . . . 11 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
129	127, 17, 128	sylancl 662	. . . . . . . . . 10 |- ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
130		4ne0 10653	. . . . . . . . . . 11 |- 4 =/= 0
131	130	a1i 11	. . . . . . . . . 10 |- ( ph -> 4 =/= 0 )
132	129, 95, 131	divcan3d 10346	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
133	126, 132	syl5eq 2510	. . . . . . . 8 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
134	124, 133	eqtrd 2498	. . . . . . 7 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
135	93, 134	oveq12d 6314	. . . . . 6 |- ( ph -> ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) - ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
136	35	sqcld 12311	. . . . . . . 8 |- ( ph -> ( N ^ 2 ) e. CC )
137	136, 99, 102	divcld 10341	. . . . . . 7 |- ( ph -> ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) e. CC )
138		mulcl 9593	. . . . . . . . 9 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
139	94, 97, 138	sylancr 663	. . . . . . . 8 |- ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
140	139, 99, 102	divcld 10341	. . . . . . 7 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) e. CC )
141	16	sqcli 12251	. . . . . . . 8 |- ( 2 ^ 2 ) e. CC
142	141	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) e. CC )
143	125, 130	eqnetri 2753	. . . . . . . 8 |- ( 2 ^ 2 ) =/= 0
144	143	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) =/= 0 )
145	137, 140, 142, 144	divsubdird 10380	. . . . . 6 |- ( ph -> ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) - ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) ) )
146	83	sqcld 12311	. . . . . . 7 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
147	146, 129	negsubd 9956	. . . . . 6 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
148	135, 145, 147	3eqtr4d 2508	. . . . 5 |- ( ph -> ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) )
149	66, 36, 38	sqdivd 12326	. . . . . . 7 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) )
150		mcubic.2	. . . . . . . 8 |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
151	150	oveq1d 6311	. . . . . . 7 |- ( ph -> ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) )
152	136, 139, 99, 102	divsubdird 10380	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
153	149, 151, 152	3eqtrd 2502	. . . . . 6 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
154	153	oveq1d 6311	. . . . 5 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
155		oexpneg 14061	. . . . . . 7 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
156	127, 47, 57, 155	syl3anc 1228	. . . . . 6 |- ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
157	156	oveq2d 6312	. . . . 5 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) )
158	148, 154, 157	3eqtr4d 2508	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
159	88, 89, 158	3eqtrd 2502	. . 3 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
160	9, 10, 10, 12, 12	divdiv1d 10372	. . . . . 6 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
161		3t3e9 10709	. . . . . . 7 |- ( 3 x. 3 ) = 9
162	161	oveq2i 6307	. . . . . 6 |- ( M / ( 3 x. 3 ) ) = ( M / 9 )
163	160, 162	syl6eq 2514	. . . . 5 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
164	163	negeqd 9833	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
165	13, 10, 12	divnegd 10354	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
166	164, 165	eqtr3d 2500	. . 3 |- ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
167		eqidd 2458	. . 3 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
168		mcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
169	43, 10, 168, 12	divne0d 10357	. . . 4 |- ( ph -> ( T / 3 ) =/= 0 )
170	44, 169	negne0d 9948	. . 3 |- ( ph -> -u ( T / 3 ) =/= 0 )
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 23303	. 2 |- ( ph -> ( ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) ) )
172		binom3 12290	. . . . . . 7 |- ( ( X e. CC /\ ( B / 3 ) e. CC ) -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
173	40, 41, 172	syl2anc 661	. . . . . 6 |- ( ph -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
174	40	sqcld 12311	. . . . . . . . . 10 |- ( ph -> ( X ^ 2 ) e. CC )
175	10, 174, 41	mul12d 9806	. . . . . . . . 9 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
176	2, 10, 12	divcan2d 10343	. . . . . . . . . 10 |- ( ph -> ( 3 x. ( B / 3 ) ) = B )
177	176	oveq2d 6312	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
178	174, 2	mulcomd 9634	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
179	175, 177, 178	3eqtrd 2502	. . . . . . . 8 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
180	179	oveq2d 6312	. . . . . . 7 |- ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
181	180	oveq1d 6311	. . . . . 6 |- ( ph -> ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
182	173, 181	eqtrd 2498	. . . . 5 |- ( ph -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
183	182	oveq1d 6311	. . . 4 |- ( ph -> ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) )
184		expcl 12187	. . . . . . 7 |- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
185	40, 17, 184	sylancl 662	. . . . . 6 |- ( ph -> ( X ^ 3 ) e. CC )
186	2, 174	mulcld 9633	. . . . . 6 |- ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
187	185, 186	addcld 9632	. . . . 5 |- ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
188	41	sqcld 12311	. . . . . . . 8 |- ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
189	40, 188	mulcld 9633	. . . . . . 7 |- ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
190	10, 189	mulcld 9633	. . . . . 6 |- ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
191		expcl 12187	. . . . . . 7 |- ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
192	41, 17, 191	sylancl 662	. . . . . 6 |- ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
193	190, 192	addcld 9632	. . . . 5 |- ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
194	14, 42	mulcld 9633	. . . . . 6 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
195	194, 39	addcld 9632	. . . . 5 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
196	187, 193, 195	addassd 9635	. . . 4 |- ( ph -> ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) ) )
197	14, 40, 41	adddid 9637	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
198	197	oveq1d 6311	. . . . . . . . 9 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) + ( N / ; 2 7 ) ) )
199	14, 40	mulcld 9633	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
200	14, 41	mulcld 9633	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
201	199, 200, 39	addassd 9635	. . . . . . . . 9 |- ( ph -> ( ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( -u ( M / 3 ) x. X ) + ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) ) )
202	1	oveq1d 6311	. . . . . . . . . . . . . . 15 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
203	3, 7, 10, 12	divsubdird 10380	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
204	5, 10, 12	divcan3d 10346	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 3 x. C ) / 3 ) = C )
205	204	oveq2d 6312	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
206	202, 203, 205	3eqtrd 2502	. . . . . . . . . . . . . 14 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
207	206	negeqd 9833	. . . . . . . . . . . . 13 |- ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
208	3, 10, 12	divcld 10341	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
209	208, 5	negsubdi2d 9966	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
210	207, 209	eqtrd 2498	. . . . . . . . . . . 12 |- ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
211	210	oveq1d 6311	. . . . . . . . . . 11 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
212	5, 208, 40	subdird 10034	. . . . . . . . . . 11 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
213	208, 40	mulcomd 9634	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
214	4	sqvali 12250	. . . . . . . . . . . . . . . . . 18 |- ( 3 ^ 2 ) = ( 3 x. 3 )
215	214	oveq2i 6307	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
216	2, 10, 12	sqdivd 12326	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
217	3, 10, 10, 12, 12	divdiv1d 10372	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
218	215, 216, 217	3eqtr4a 2524	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
219	218	oveq2d 6312	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
220	208, 10, 12	divcan2d 10343	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
221	219, 220	eqtrd 2498	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
222	221	oveq2d 6312	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
223	40, 10, 188	mul12d 9806	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
224	213, 222, 223	3eqtr2d 2504	. . . . . . . . . . . 12 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
225	224	oveq2d 6312	. . . . . . . . . . 11 |- ( ph -> ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
226	211, 212, 225	3eqtrd 2502	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
227	210	oveq1d 6311	. . . . . . . . . . . . 13 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
228	5, 208, 41	subdird 10034	. . . . . . . . . . . . 13 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) = ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) )
229	5, 2, 10, 12	divassd 10376	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
230	5, 2	mulcomd 9634	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C x. B ) = ( B x. C ) )
231	230	oveq1d 6311	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
232	229, 231	eqtr3d 2500	. . . . . . . . . . . . . 14 |- ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
233	3, 10, 2, 10, 12, 12	divmuldivd 10382	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
234		df-3 10616	. . . . . . . . . . . . . . . . . 18 |- 3 = ( 2 + 1 )
235	234	oveq2i 6307	. . . . . . . . . . . . . . . . 17 |- ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
236		expp1 12176	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
237	2, 27, 236	sylancl 662	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
238	235, 237	syl5req 2511	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
239	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 x. 3 ) = 9 )
240	238, 239	oveq12d 6314	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
241	233, 240	eqtrd 2498	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
242	232, 241	oveq12d 6314	. . . . . . . . . . . . 13 |- ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
243	227, 228, 242	3eqtrd 2502	. . . . . . . . . . . 12 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
244	15	oveq1d 6311	. . . . . . . . . . . . 13 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) / ; 2 7 ) )
245	26, 33, 36, 38	divdird 10379	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) + ( (; 2 7 x. D ) / ; 2 7 ) ) )
246	21, 25, 36, 38	divsubdird 10380	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 9 x. ( B x. C ) ) / ; 2 7 ) ) )
247		9t3e27 11096	. . . . . . . . . . . . . . . . . 18 |- ( 9 x. 3 ) = ; 2 7
248	247	oveq2i 6307	. . . . . . . . . . . . . . . . 17 |- ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
249	23, 10, 104, 12, 107	divcan5d 10367	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
250	248, 249	syl5eqr 2512	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
251	250	oveq2d 6312	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 9 x. ( B x. C ) ) / ; 2 7 ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) )
252	246, 251	eqtrd 2498	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) )
253	31, 36, 38	divcan3d 10346	. . . . . . . . . . . . . 14 |- ( ph -> ( (; 2 7 x. D ) / ; 2 7 ) = D )
254	252, 253	oveq12d 6314	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) + ( (; 2 7 x. D ) / ; 2 7 ) ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
255	244, 245, 254	3eqtrd 2502	. . . . . . . . . . . 12 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
256	243, 255	oveq12d 6314	. . . . . . . . . . 11 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
257	19, 104, 107	divcld 10341	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
258	21, 36, 38	divcld 10341	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
259	257, 258	negsubdi2d 9966	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B ^ 3 ) / 9 ) ) )
260	2, 10, 12, 60	expdivd 12327	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
261	63	oveq2i 6307	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
262		ax-1cn 9567	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
263	4, 16, 262, 53	subaddrii 9928	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 - 2 ) = 1
264	263	oveq1i 6306	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
265	19	mulid2d 9631	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
266	264, 265	syl5eq 2510	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
267	10, 68, 19	subdird 10034	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
268	266, 267	eqtr3d 2500	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
269	268	oveq1d 6311	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
270		mulcl 9593	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
271	4, 19, 270	sylancr 663	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
272	271, 21, 36, 38	divsubdird 10380	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
273	269, 272	eqtrd 2498	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274	261, 273	syl5eq 2510	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275	22, 4, 247	mulcomli 9620	. . . . . . . . . . . . . . . . . . 19 |- ( 3 x. 9 ) = ; 2 7
276	275	oveq2i 6307	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
277	19, 104, 10, 107, 12	divcan5d 10367	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
278	276, 277	syl5eqr 2512	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
279	278	oveq1d 6311	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
280	260, 274, 279	3eqtrd 2502	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
281	280	negeqd 9833	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
282	23, 10, 12	divcld 10341	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B x. C ) / 3 ) e. CC )
283	282, 257, 258	npncan3d 9986	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B ^ 3 ) / 9 ) ) )
284	259, 281, 283	3eqtr4d 2508	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) )
285	284	oveq1d 6311	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) + D ) )
286	192	negcld 9937	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
287	286, 31	addcomd 9799	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
288	243, 200	eqeltrrd 2546	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
289	258, 282	subcld 9950	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
290	288, 289, 31	addassd 9635	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) + D ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
291	285, 287, 290	3eqtr3d 2506	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
292	31, 192	negsubd 9956	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
293	256, 291, 292	3eqtr2d 2504	. . . . . . . . . 10 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
294	226, 293	oveq12d 6314	. . . . . . . . 9 |- ( ph -> ( ( -u ( M / 3 ) x. X ) + ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
295	198, 201, 294	3eqtrd 2502	. . . . . . . 8 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
296	5, 40	mulcld 9633	. . . . . . . . 9 |- ( ph -> ( C x. X ) e. CC )
297	296, 31, 190, 192	addsub4d 9997	. . . . . . . 8 |- ( ph -> ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
298	295, 297	eqtr4d 2501	. . . . . . 7 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
299	298	oveq2d 6312	. . . . . 6 |- ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) ) )
300	296, 31	addcld 9632	. . . . . . 7 |- ( ph -> ( ( C x. X ) + D ) e. CC )
301	193, 300	pncan3d 9953	. . . . . 6 |- ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) ) = ( ( C x. X ) + D ) )
302	299, 301	eqtrd 2498	. . . . 5 |- ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( C x. X ) + D ) )
303	302	oveq2d 6312	. . . 4 |- ( ph -> ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) )
304	183, 196, 303	3eqtrd 2502	. . 3 |- ( ph -> ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) )
305	304	eqeq1d 2459	. 2 |- ( ph -> ( ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = 0 <-> ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 ) )
306		oveq1 6303	. . . . . . . 8 |- ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
307		0exp 12204	. . . . . . . . 9 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
308	46, 307	ax-mp 5	. . . . . . . 8 |- ( 0 ^ 3 ) = 0
309	306, 308	syl6eq 2514	. . . . . . 7 |- ( r = 0 -> ( r ^ 3 ) = 0 )
310		0ne1 10624	. . . . . . . 8 |- 0 =/= 1
311	310	a1i 11	. . . . . . 7 |- ( r = 0 -> 0 =/= 1 )
312	309, 311	eqnetrd 2750	. . . . . 6 |- ( r = 0 -> ( r ^ 3 ) =/= 1 )
313	312	necon2i 2700	. . . . 5 |- ( ( r ^ 3 ) = 1 -> r =/= 0 )
314		eqcom 2466	. . . . . . . 8 |- ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X )
315	2	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
316		simprl 756	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
317	43	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
318	316, 317	mulcld 9633	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
319	9	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
320		simprr 757	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
321	168	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
322	316, 317, 320, 321	mulne0d 10222	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
323	319, 318, 322	divcld 10341	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
324	318, 323	addcld 9632	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) + ( M / ( r x. T ) ) ) e. CC )
325	4	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 e. CC )
326	11	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 =/= 0 )
327	315, 324, 325, 326	divdird 10379	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) / 3 ) = ( ( B / 3 ) + ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
328	315, 318, 323	addassd 9635	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) = ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) )
329	328	oveq1d 6311	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) / 3 ) )
330	41	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
331	324, 325, 326	divcld 10341	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
332	330, 331	subnegd 9957	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) = ( ( B / 3 ) + ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
333	327, 329, 332	3eqtr4d 2508	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
334	333	negeqd 9833	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = -u ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
335	331	negcld 9937	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
336	330, 335	negsubdi2d 9966	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) = ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) )
337	334, 336	eqtrd 2498	. . . . . . . . 9 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) )
338	337	eqeq1d 2459	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
339	314, 338	syl5bb 257	. . . . . . 7 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
340	40	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
341	335, 330, 340	subadd2d 9969	. . . . . . 7 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X <-> ( X + ( B / 3 ) ) = -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
342	318, 323, 325, 326	divdird 10379	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) )
343	342	negeqd 9833	. . . . . . . . 9 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = -u ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) )
344	318, 325, 326	divcld 10341	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
345	323, 325, 326	divcld 10341	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
346	344, 345	negdi2d 9964	. . . . . . . . 9 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) = ( -u ( ( r x. T ) / 3 ) - ( ( M / ( r x. T ) ) / 3 ) ) )
347	316, 317, 325, 326	divassd 10376	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
348	347	negeqd 9833	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
349	44	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
350	316, 349	mulneg2d 10031	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
351	348, 350	eqtr4d 2501	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
352	319, 318, 325, 322, 326	divdiv32d 10366	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
353	13	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
354	353, 318, 325, 322, 326	divcan7d 10369	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
355	163	oveq1d 6311	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
356	355	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
357	352, 354, 356	3eqtr2d 2504	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
358	127	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
359	318, 325, 322, 326	divne0d 10357	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
360	358, 344, 359	div2negd 10356	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
361	351	oveq2d 6312	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
362	357, 360, 361	3eqtr2d 2504	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
363	351, 362	oveq12d 6314	. . . . . . . . 9 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( ( r x. T ) / 3 ) - ( ( M / ( r x. T ) ) / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) )
364	343, 346, 363	3eqtrd 2502	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) )
365	364	eqeq2d 2471	. . . . . . 7 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) )
366	339, 341, 365	3bitrrd 280	. . . . . 6 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
367	366	anassrs 648	. . . . 5 |- ( ( ( ph /\ r e. CC ) /\ r =/= 0 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
368	313, 367	sylan2 474	. . . 4 |- ( ( ( ph /\ r e. CC ) /\ ( r ^ 3 ) = 1 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
369	368	pm5.32da 641	. . 3 |- ( ( ph /\ r e. CC ) -> ( ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) <-> ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
370	369	rexbidva 2965	. 2 |- ( ph -> ( E. r e. CC ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
371	171, 305, 370	3bitr3d 283	1 |- ( ph -> ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1395   e. wcel 1819   =/= wne 2652   E.wrex 2808   class class class wbr 4456  (class class class)co 6296   CCcc 9507   0cc0 9509   1c1 9510   + caddc 9512   x. cmul 9514   - cmin 9824   -ucneg 9825   / cdiv 10227   NNcn 10556   2c2 10606   3c3 10607   4c4 10608   7c7 10611   9c9 10613   NN0cn0 10816  ;cdc 11000   ^cexp 12169   || cdvds 13998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-sup 7919  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-rp 11246  df-fz 11698  df-seq 12111  df-exp 12170  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-dvds 13999

This theorem is referenced by:  cubic2  23305  quart  23318