Theorem mcubic 23766

Description: Solutions to a monic cubic equation, a special case of cubic 23768. (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 12411	. . . . . . 7 |- ( ph -> ( B ^ 2 ) e. CC )
4		3cn 10681	. . . . . . . 8 |- 3 e. CC
5		mcubic.c	. . . . . . . 8 |- ( ph -> C e. CC )
6		mulcl 9620	. . . . . . . 8 |- ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
7	4, 5, 6	sylancr 668	. . . . . . 7 |- ( ph -> ( 3 x. C ) e. CC )
8	3, 7	subcld 9983	. . . . . 6 |- ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
9	1, 8	eqeltrd 2528	. . . . 5 |- ( ph -> M e. CC )
10	4	a1i 11	. . . . 5 |- ( ph -> 3 e. CC )
11		3ne0 10701	. . . . . 6 |- 3 =/= 0
12	11	a1i 11	. . . . 5 |- ( ph -> 3 =/= 0 )
13	9, 10, 12	divcld 10380	. . . 4 |- ( ph -> ( M / 3 ) e. CC )
14	13	negcld 9970	. . 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 10677	. . . . . . . 8 |- 2 e. CC
17		3nn0 10884	. . . . . . . . 9 |- 3 e. NN0
18		expcl 12287	. . . . . . . . 9 |- ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
19	2, 17, 18	sylancl 667	. . . . . . . 8 |- ( ph -> ( B ^ 3 ) e. CC )
20		mulcl 9620	. . . . . . . 8 |- ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
21	16, 19, 20	sylancr 668	. . . . . . 7 |- ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
22		9cn 10694	. . . . . . . 8 |- 9 e. CC
23	2, 5	mulcld 9660	. . . . . . . 8 |- ( ph -> ( B x. C ) e. CC )
24		mulcl 9620	. . . . . . . 8 |- ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
25	22, 23, 24	sylancr 668	. . . . . . 7 |- ( ph -> ( 9 x. ( B x. C ) ) e. CC )
26	21, 25	subcld 9983	. . . . . 6 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
27		2nn0 10883	. . . . . . . . 9 |- 2 e. NN0
28		7nn 10769	. . . . . . . . 9 |- 7 e. NN
29	27, 28	decnncl 11061	. . . . . . . 8 |- ; 2 7 e. NN
30	29	nncni 10616	. . . . . . 7 |- ; 2 7 e. CC
31		mcubic.d	. . . . . . 7 |- ( ph -> D e. CC )
32		mulcl 9620	. . . . . . 7 |- ( (; 2 7 e. CC /\ D e. CC ) -> (; 2 7 x. D ) e. CC )
33	30, 31, 32	sylancr 668	. . . . . 6 |- ( ph -> (; 2 7 x. D ) e. CC )
34	26, 33	addcld 9659	. . . . 5 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) e. CC )
35	15, 34	eqeltrd 2528	. . . 4 |- ( ph -> N e. CC )
36	30	a1i 11	. . . 4 |- ( ph -> ; 2 7 e. CC )
37	29	nnne0i 10641	. . . . 5 |- ; 2 7 =/= 0
38	37	a1i 11	. . . 4 |- ( ph -> ; 2 7 =/= 0 )
39	35, 36, 38	divcld 10380	. . 3 |- ( ph -> ( N / ; 2 7 ) e. CC )
40		mcubic.x	. . . 4 |- ( ph -> X e. CC )
41	2, 10, 12	divcld 10380	. . . 4 |- ( ph -> ( B / 3 ) e. CC )
42	40, 41	addcld 9659	. . 3 |- ( ph -> ( X + ( B / 3 ) ) e. CC )
43		mcubic.t	. . . . 5 |- ( ph -> T e. CC )
44	43, 10, 12	divcld 10380	. . . 4 |- ( ph -> ( T / 3 ) e. CC )
45	44	negcld 9970	. . 3 |- ( ph -> -u ( T / 3 ) e. CC )
46		3nn 10765	. . . . . 6 |- 3 e. NN
47	46	a1i 11	. . . . 5 |- ( ph -> 3 e. NN )
48		2nn 10764	. . . . . . 7 |- 2 e. NN
49		1nn0 10882	. . . . . . 7 |- 1 e. NN0
50		1nn 10617	. . . . . . 7 |- 1 e. NN
51		2t1e2 10755	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
52	51	oveq1i 6298	. . . . . . . 8 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
53		2p1e3 10730	. . . . . . . 8 |- ( 2 + 1 ) = 3
54	52, 53	eqtri 2472	. . . . . . 7 |- ( ( 2 x. 1 ) + 1 ) = 3
55		1lt2 10773	. . . . . . 7 |- 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 14384	. . . . . 6 |- -. 2 || 3
57	56	a1i 11	. . . . 5 |- ( ph -> -. 2 || 3 )
58		oexpneg 14361	. . . . 5 |- ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
59	44, 47, 57, 58	syl3anc 1267	. . . 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 12427	. . . . . 6 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
62		mcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
63		3exp3 15055	. . . . . . . 8 |- ( 3 ^ 3 ) = ; 2 7
64	63	a1i 11	. . . . . . 7 |- ( ph -> ( 3 ^ 3 ) = ; 2 7 )
65	62, 64	oveq12d 6306	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
66		mcubic.g	. . . . . . . . 9 |- ( ph -> G e. CC )
67	35, 66	addcld 9659	. . . . . . . 8 |- ( ph -> ( N + G ) e. CC )
68		2cnd 10679	. . . . . . . 8 |- ( ph -> 2 e. CC )
69		2ne0 10699	. . . . . . . . 9 |- 2 =/= 0
70	69	a1i 11	. . . . . . . 8 |- ( ph -> 2 =/= 0 )
71	67, 68, 36, 70, 38	divdiv32d 10405	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
72	35, 66	addcomd 9832	. . . . . . . . . 10 |- ( ph -> ( N + G ) = ( G + N ) )
73	72	oveq1d 6303	. . . . . . . . 9 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
74	66, 35, 36, 38	divdird 10418	. . . . . . . . 9 |- ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
75	73, 74	eqtrd 2484	. . . . . . . 8 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
76	75	oveq1d 6303	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
77	66, 36, 38	divcld 10380	. . . . . . . 8 |- ( ph -> ( G / ; 2 7 ) e. CC )
78	77, 39, 68, 70	divdird 10418	. . . . . . 7 |- ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
79	71, 76, 78	3eqtrd 2488	. . . . . 6 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
80	61, 65, 79	3eqtrd 2488	. . . . 5 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
81	80	negeqd 9866	. . . 4 |- ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
82	77	halfcld 10854	. . . . 5 |- ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
83	39	halfcld 10854	. . . . 5 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
84	82, 83	negdi2d 9997	. . . 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 2488	. . 3 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
86	82	negcld 9970	. . 3 |- ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
87		sqneg 12332	. . . . 5 |- ( ( ( G / ; 2 7 ) / 2 ) e. CC -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
88	82, 87	syl 17	. . . 4 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
89	77, 68, 70	sqdivd 12426	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
90	39, 68, 70	sqdivd 12426	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
91	35, 36, 38	sqdivd 12426	. . . . . . . . 9 |- ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) )
92	91	oveq1d 6303	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
93	90, 92	eqtr2d 2485	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
94		4cn 10684	. . . . . . . . . . . 12 |- 4 e. CC
95	94	a1i 11	. . . . . . . . . . 11 |- ( ph -> 4 e. CC )
96		expcl 12287	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
97	9, 17, 96	sylancl 667	. . . . . . . . . . 11 |- ( ph -> ( M ^ 3 ) e. CC )
98	30	sqcli 12352	. . . . . . . . . . . 12 |- (; 2 7 ^ 2 ) e. CC
99	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) e. CC )
100		sqne0 12338	. . . . . . . . . . . . 13 |- (; 2 7 e. CC -> ( (; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
101	36, 100	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( (; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
102	38, 101	mpbird 236	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) =/= 0 )
103	95, 97, 99, 102	divassd 10415	. . . . . . . . . 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 10771	. . . . . . . . . . . . . . 15 |- 9 e. NN
106	105	nnne0i 10641	. . . . . . . . . . . . . 14 |- 9 =/= 0
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 =/= 0 )
108	9, 104, 107, 60	expdivd 12427	. . . . . . . . . . . 12 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
109	16, 4	mulcomi 9646	. . . . . . . . . . . . . . . 16 |- ( 2 x. 3 ) = ( 3 x. 2 )
110	109	oveq2i 6299	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
111		expmul 12314	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
112	4, 27, 17, 111	mp3an 1363	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
113		expmul 12314	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
114	4, 17, 27, 113	mp3an 1363	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
115	110, 112, 114	3eqtr3i 2480	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
116		sq3 12369	. . . . . . . . . . . . . . 15 |- ( 3 ^ 2 ) = 9
117	116	oveq1i 6298	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
118	63	oveq1i 6298	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 3 ) ^ 2 ) = (; 2 7 ^ 2 )
119	115, 117, 118	3eqtr3i 2480	. . . . . . . . . . . . 13 |- ( 9 ^ 3 ) = (; 2 7 ^ 2 )
120	119	oveq2i 6299	. . . . . . . . . . . 12 |- ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) )
121	108, 120	syl6eq 2500	. . . . . . . . . . 11 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) )
122	121	oveq2d 6304	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
123	103, 122	eqtr4d 2487	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
124	123	oveq1d 6303	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
125		sq2 12368	. . . . . . . . . 10 |- ( 2 ^ 2 ) = 4
126	125	oveq2i 6299	. . . . . . . . 9 |- ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
127	9, 104, 107	divcld 10380	. . . . . . . . . . 11 |- ( ph -> ( M / 9 ) e. CC )
128		expcl 12287	. . . . . . . . . . 11 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
129	127, 17, 128	sylancl 667	. . . . . . . . . 10 |- ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
130		4ne0 10703	. . . . . . . . . . 11 |- 4 =/= 0
131	130	a1i 11	. . . . . . . . . 10 |- ( ph -> 4 =/= 0 )
132	129, 95, 131	divcan3d 10385	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
133	126, 132	syl5eq 2496	. . . . . . . 8 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
134	124, 133	eqtrd 2484	. . . . . . 7 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
135	93, 134	oveq12d 6306	. . . . . 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 12411	. . . . . . . 8 |- ( ph -> ( N ^ 2 ) e. CC )
137	136, 99, 102	divcld 10380	. . . . . . 7 |- ( ph -> ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) e. CC )
138		mulcl 9620	. . . . . . . . 9 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
139	94, 97, 138	sylancr 668	. . . . . . . 8 |- ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
140	139, 99, 102	divcld 10380	. . . . . . 7 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) e. CC )
141	16	sqcli 12352	. . . . . . . 8 |- ( 2 ^ 2 ) e. CC
142	141	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) e. CC )
143	125, 130	eqnetri 2693	. . . . . . . 8 |- ( 2 ^ 2 ) =/= 0
144	143	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) =/= 0 )
145	137, 140, 142, 144	divsubdird 10419	. . . . . 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 12411	. . . . . . 7 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
147	146, 129	negsubd 9989	. . . . . 6 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
148	135, 145, 147	3eqtr4d 2494	. . . . 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 12426	. . . . . . 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 6303	. . . . . . 7 |- ( ph -> ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) )
152	136, 139, 99, 102	divsubdird 10419	. . . . . . 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 2488	. . . . . 6 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
154	153	oveq1d 6303	. . . . 5 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
155		oexpneg 14361	. . . . . . 7 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
156	127, 47, 57, 155	syl3anc 1267	. . . . . 6 |- ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
157	156	oveq2d 6304	. . . . 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 2494	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
159	88, 89, 158	3eqtrd 2488	. . 3 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
160	9, 10, 10, 12, 12	divdiv1d 10411	. . . . . 6 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
161		3t3e9 10759	. . . . . . 7 |- ( 3 x. 3 ) = 9
162	161	oveq2i 6299	. . . . . 6 |- ( M / ( 3 x. 3 ) ) = ( M / 9 )
163	160, 162	syl6eq 2500	. . . . 5 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
164	163	negeqd 9866	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
165	13, 10, 12	divnegd 10393	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
166	164, 165	eqtr3d 2486	. . 3 |- ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
167		eqidd 2451	. . 3 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
168		mcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
169	43, 10, 168, 12	divne0d 10396	. . . 4 |- ( ph -> ( T / 3 ) =/= 0 )
170	44, 169	negne0d 9981	. . 3 |- ( ph -> -u ( T / 3 ) =/= 0 )
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 23765	. 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 12390	. . . . . . 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 666	. . . . . 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 12411	. . . . . . . . . 10 |- ( ph -> ( X ^ 2 ) e. CC )
175	10, 174, 41	mul12d 9839	. . . . . . . . 9 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
176	2, 10, 12	divcan2d 10382	. . . . . . . . . 10 |- ( ph -> ( 3 x. ( B / 3 ) ) = B )
177	176	oveq2d 6304	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
178	174, 2	mulcomd 9661	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
179	175, 177, 178	3eqtrd 2488	. . . . . . . 8 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
180	179	oveq2d 6304	. . . . . . 7 |- ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
181	180	oveq1d 6303	. . . . . 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 2484	. . . . 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 6303	. . . 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 12287	. . . . . . 7 |- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
185	40, 17, 184	sylancl 667	. . . . . 6 |- ( ph -> ( X ^ 3 ) e. CC )
186	2, 174	mulcld 9660	. . . . . 6 |- ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
187	185, 186	addcld 9659	. . . . 5 |- ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
188	41	sqcld 12411	. . . . . . . 8 |- ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
189	40, 188	mulcld 9660	. . . . . . 7 |- ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
190	10, 189	mulcld 9660	. . . . . 6 |- ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
191		expcl 12287	. . . . . . 7 |- ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
192	41, 17, 191	sylancl 667	. . . . . 6 |- ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
193	190, 192	addcld 9659	. . . . 5 |- ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
194	14, 42	mulcld 9660	. . . . . 6 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
195	194, 39	addcld 9659	. . . . 5 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
196	187, 193, 195	addassd 9662	. . . 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 9664	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
198	197	oveq1d 6303	. . . . . . . . 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 9660	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
200	14, 41	mulcld 9660	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
201	199, 200, 39	addassd 9662	. . . . . . . . 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 6303	. . . . . . . . . . . . . . 15 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
203	3, 7, 10, 12	divsubdird 10419	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
204	5, 10, 12	divcan3d 10385	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 3 x. C ) / 3 ) = C )
205	204	oveq2d 6304	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
206	202, 203, 205	3eqtrd 2488	. . . . . . . . . . . . . 14 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
207	206	negeqd 9866	. . . . . . . . . . . . 13 |- ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
208	3, 10, 12	divcld 10380	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
209	208, 5	negsubdi2d 9999	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
210	207, 209	eqtrd 2484	. . . . . . . . . . . 12 |- ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
211	210	oveq1d 6303	. . . . . . . . . . 11 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
212	5, 208, 40	subdird 10072	. . . . . . . . . . 11 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
213	208, 40	mulcomd 9661	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
214	4	sqvali 12351	. . . . . . . . . . . . . . . . . 18 |- ( 3 ^ 2 ) = ( 3 x. 3 )
215	214	oveq2i 6299	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
216	2, 10, 12	sqdivd 12426	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
217	3, 10, 10, 12, 12	divdiv1d 10411	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
218	215, 216, 217	3eqtr4a 2510	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
219	218	oveq2d 6304	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
220	208, 10, 12	divcan2d 10382	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
221	219, 220	eqtrd 2484	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
222	221	oveq2d 6304	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
223	40, 10, 188	mul12d 9839	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
224	213, 222, 223	3eqtr2d 2490	. . . . . . . . . . . 12 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
225	224	oveq2d 6304	. . . . . . . . . . 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 2488	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
227	210	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
228	5, 208, 41	subdird 10072	. . . . . . . . . . . . 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 10415	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
230	5, 2	mulcomd 9661	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C x. B ) = ( B x. C ) )
231	230	oveq1d 6303	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
232	229, 231	eqtr3d 2486	. . . . . . . . . . . . . 14 |- ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
233	3, 10, 2, 10, 12, 12	divmuldivd 10421	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
234		df-3 10666	. . . . . . . . . . . . . . . . . 18 |- 3 = ( 2 + 1 )
235	234	oveq2i 6299	. . . . . . . . . . . . . . . . 17 |- ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
236		expp1 12276	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
237	2, 27, 236	sylancl 667	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
238	235, 237	syl5req 2497	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
239	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 x. 3 ) = 9 )
240	238, 239	oveq12d 6306	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
241	233, 240	eqtrd 2484	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
242	232, 241	oveq12d 6306	. . . . . . . . . . . . 13 |- ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
243	227, 228, 242	3eqtrd 2488	. . . . . . . . . . . 12 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
244	15	oveq1d 6303	. . . . . . . . . . . . 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 10418	. . . . . . . . . . . . 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 10419	. . . . . . . . . . . . . . 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 11144	. . . . . . . . . . . . . . . . . 18 |- ( 9 x. 3 ) = ; 2 7
248	247	oveq2i 6299	. . . . . . . . . . . . . . . . 17 |- ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
249	23, 10, 104, 12, 107	divcan5d 10406	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
250	248, 249	syl5eqr 2498	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
251	250	oveq2d 6304	. . . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . . 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 10385	. . . . . . . . . . . . . 14 |- ( ph -> ( (; 2 7 x. D ) / ; 2 7 ) = D )
254	252, 253	oveq12d 6306	. . . . . . . . . . . . 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 2488	. . . . . . . . . . . 12 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
256	243, 255	oveq12d 6306	. . . . . . . . . . 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 10380	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
258	21, 36, 38	divcld 10380	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
259	257, 258	negsubdi2d 9999	. . . . . . . . . . . . . 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 12427	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
261	63	oveq2i 6299	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
262		ax-1cn 9594	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
263	4, 16, 262, 53	subaddrii 9961	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 - 2 ) = 1
264	263	oveq1i 6298	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
265	19	mulid2d 9658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
266	264, 265	syl5eq 2496	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
267	10, 68, 19	subdird 10072	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
268	266, 267	eqtr3d 2486	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
269	268	oveq1d 6303	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
270		mulcl 9620	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
271	4, 19, 270	sylancr 668	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
272	271, 21, 36, 38	divsubdird 10419	. . . . . . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274	261, 273	syl5eq 2496	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275	22, 4, 247	mulcomli 9647	. . . . . . . . . . . . . . . . . . 19 |- ( 3 x. 9 ) = ; 2 7
276	275	oveq2i 6299	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
277	19, 104, 10, 107, 12	divcan5d 10406	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
278	276, 277	syl5eqr 2498	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
279	278	oveq1d 6303	. . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
281	280	negeqd 9866	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
282	23, 10, 12	divcld 10380	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B x. C ) / 3 ) e. CC )
283	282, 257, 258	npncan3d 10019	. . . . . . . . . . . . . 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 2494	. . . . . . . . . . . . 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 6303	. . . . . . . . . . . 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 9970	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
287	286, 31	addcomd 9832	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
288	243, 200	eqeltrrd 2529	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
289	258, 282	subcld 9983	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
290	288, 289, 31	addassd 9662	. . . . . . . . . . . 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 2492	. . . . . . . . . . 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 9989	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
293	256, 291, 292	3eqtr2d 2490	. . . . . . . . . 10 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
294	226, 293	oveq12d 6306	. . . . . . . . 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 2488	. . . . . . . 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 9660	. . . . . . . . 9 |- ( ph -> ( C x. X ) e. CC )
297	296, 31, 190, 192	addsub4d 10030	. . . . . . . 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 2487	. . . . . . 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 6304	. . . . . 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 9659	. . . . . . 7 |- ( ph -> ( ( C x. X ) + D ) e. CC )
301	193, 300	pncan3d 9986	. . . . . 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 2484	. . . . 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 6304	. . . 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 2488	. . 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 2452	. 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 6295	. . . . . . . 8 |- ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
307		0exp 12304	. . . . . . . . 9 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
308	46, 307	ax-mp 5	. . . . . . . 8 |- ( 0 ^ 3 ) = 0
309	306, 308	syl6eq 2500	. . . . . . 7 |- ( r = 0 -> ( r ^ 3 ) = 0 )
310		0ne1 10674	. . . . . . . 8 |- 0 =/= 1
311	310	a1i 11	. . . . . . 7 |- ( r = 0 -> 0 =/= 1 )
312	309, 311	eqnetrd 2690	. . . . . 6 |- ( r = 0 -> ( r ^ 3 ) =/= 1 )
313	312	necon2i 2657	. . . . 5 |- ( ( r ^ 3 ) = 1 -> r =/= 0 )
314		eqcom 2457	. . . . . . . 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 467	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
316		simprl 763	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
317	43	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
318	316, 317	mulcld 9660	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
319	9	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
320		simprr 765	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
321	168	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
322	316, 317, 320, 321	mulne0d 10261	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
323	319, 318, 322	divcld 10380	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
324	318, 323	addcld 9659	. . . . . . . . . . . . 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 10418	. . . . . . . . . . . 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 9662	. . . . . . . . . . . . 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 6303	. . . . . . . . . . . 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 467	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
331	324, 325, 326	divcld 10380	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
332	330, 331	subnegd 9990	. . . . . . . . . . . 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 2494	. . . . . . . . . . 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 9866	. . . . . . . . . 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 9970	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
336	330, 335	negsubdi2d 9999	. . . . . . . . . 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 2484	. . . . . . . . 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 2452	. . . . . . . 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 261	. . . . . . 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 467	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
341	335, 330, 340	subadd2d 10002	. . . . . . 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 10418	. . . . . . . . . 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 9866	. . . . . . . . 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 10380	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
345	323, 325, 326	divcld 10380	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
346	344, 345	negdi2d 9997	. . . . . . . . 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 10415	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
348	347	negeqd 9866	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
349	44	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
350	316, 349	mulneg2d 10069	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
351	348, 350	eqtr4d 2487	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
352	319, 318, 325, 322, 326	divdiv32d 10405	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
353	13	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
354	353, 318, 325, 322, 326	divcan7d 10408	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
355	163	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
356	355	adantr 467	. . . . . . . . . . . 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 2490	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
358	127	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
359	318, 325, 322, 326	divne0d 10396	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
360	358, 344, 359	div2negd 10395	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
361	351	oveq2d 6304	. . . . . . . . . . 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 2490	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
363	351, 362	oveq12d 6306	. . . . . . . . 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 2488	. . . . . . . 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 2460	. . . . . . 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 284	. . . . . 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 653	. . . . 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 477	. . . 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 646	. . 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 2897	. 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 287	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 188   /\ wa 371   = wceq 1443   e. wcel 1886   =/= wne 2621   E.wrex 2737   class class class wbr 4401  (class class class)co 6288   CCcc 9534   0cc0 9536   1c1 9537   + caddc 9539   x. cmul 9541   - cmin 9857   -ucneg 9858   / cdiv 10266   NNcn 10606   2c2 10656   3c3 10657   4c4 10658   7c7 10661   9c9 10663   NN0cn0 10866  ;cdc 11048   ^cexp 12269   || cdvds 14298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-sup 7953  df-inf 7954  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-5 10668  df-6 10669  df-7 10670  df-8 10671  df-9 10672  df-10 10673  df-n0 10867  df-z 10935  df-dec 11049  df-uz 11157  df-rp 11300  df-fz 11782  df-seq 12211  df-exp 12270  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-dvds 14299

This theorem is referenced by:  cubic2  23767  quart  23780