Theorem mcubic 22127

Description: Solutions to a monic cubic equation, a special case of cubic 22129. (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 11990	. . . . . . 7 |- ( ph -> ( B ^ 2 ) e. CC )
4		3cn 10384	. . . . . . . 8 |- 3 e. CC
5		mcubic.c	. . . . . . . 8 |- ( ph -> C e. CC )
6		mulcl 9354	. . . . . . . 8 |- ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
7	4, 5, 6	sylancr 656	. . . . . . 7 |- ( ph -> ( 3 x. C ) e. CC )
8	3, 7	subcld 9707	. . . . . 6 |- ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
9	1, 8	eqeltrd 2507	. . . . 5 |- ( ph -> M e. CC )
10	4	a1i 11	. . . . 5 |- ( ph -> 3 e. CC )
11		3ne0 10404	. . . . . 6 |- 3 =/= 0
12	11	a1i 11	. . . . 5 |- ( ph -> 3 =/= 0 )
13	9, 10, 12	divcld 10095	. . . 4 |- ( ph -> ( M / 3 ) e. CC )
14	13	negcld 9694	. . 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 10380	. . . . . . . 8 |- 2 e. CC
17		3nn0 10585	. . . . . . . . 9 |- 3 e. NN0
18		expcl 11867	. . . . . . . . 9 |- ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
19	2, 17, 18	sylancl 655	. . . . . . . 8 |- ( ph -> ( B ^ 3 ) e. CC )
20		mulcl 9354	. . . . . . . 8 |- ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
21	16, 19, 20	sylancr 656	. . . . . . 7 |- ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
22		9cn 10397	. . . . . . . 8 |- 9 e. CC
23	2, 5	mulcld 9394	. . . . . . . 8 |- ( ph -> ( B x. C ) e. CC )
24		mulcl 9354	. . . . . . . 8 |- ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
25	22, 23, 24	sylancr 656	. . . . . . 7 |- ( ph -> ( 9 x. ( B x. C ) ) e. CC )
26	21, 25	subcld 9707	. . . . . 6 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
27		2nn0 10584	. . . . . . . . 9 |- 2 e. NN0
28		7nn 10472	. . . . . . . . 9 |- 7 e. NN
29	27, 28	decnncl 10756	. . . . . . . 8 |- ; 2 7 e. NN
30	29	nncni 10320	. . . . . . 7 |- ; 2 7 e. CC
31		mcubic.d	. . . . . . 7 |- ( ph -> D e. CC )
32		mulcl 9354	. . . . . . 7 |- ( (; 2 7 e. CC /\ D e. CC ) -> (; 2 7 x. D ) e. CC )
33	30, 31, 32	sylancr 656	. . . . . 6 |- ( ph -> (; 2 7 x. D ) e. CC )
34	26, 33	addcld 9393	. . . . 5 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) e. CC )
35	15, 34	eqeltrd 2507	. . . 4 |- ( ph -> N e. CC )
36	30	a1i 11	. . . 4 |- ( ph -> ; 2 7 e. CC )
37	29	nnne0i 10344	. . . . 5 |- ; 2 7 =/= 0
38	37	a1i 11	. . . 4 |- ( ph -> ; 2 7 =/= 0 )
39	35, 36, 38	divcld 10095	. . 3 |- ( ph -> ( N / ; 2 7 ) e. CC )
40		mcubic.x	. . . 4 |- ( ph -> X e. CC )
41	2, 10, 12	divcld 10095	. . . 4 |- ( ph -> ( B / 3 ) e. CC )
42	40, 41	addcld 9393	. . 3 |- ( ph -> ( X + ( B / 3 ) ) e. CC )
43		mcubic.t	. . . . 5 |- ( ph -> T e. CC )
44	43, 10, 12	divcld 10095	. . . 4 |- ( ph -> ( T / 3 ) e. CC )
45	44	negcld 9694	. . 3 |- ( ph -> -u ( T / 3 ) e. CC )
46		3nn 10468	. . . . . 6 |- 3 e. NN
47	46	a1i 11	. . . . 5 |- ( ph -> 3 e. NN )
48		2nn 10467	. . . . . . 7 |- 2 e. NN
49		1nn0 10583	. . . . . . 7 |- 1 e. NN0
50		1nn 10321	. . . . . . 7 |- 1 e. NN
51		2t1e2 10458	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
52	51	oveq1i 6090	. . . . . . . 8 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
53		2p1e3 10433	. . . . . . . 8 |- ( 2 + 1 ) = 3
54	52, 53	eqtri 2453	. . . . . . 7 |- ( ( 2 x. 1 ) + 1 ) = 3
55		1lt2 10476	. . . . . . 7 |- 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 13597	. . . . . 6 |- -. 2 || 3
57	56	a1i 11	. . . . 5 |- ( ph -> -. 2 || 3 )
58		oexpneg 13578	. . . . 5 |- ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
59	44, 47, 57, 58	syl3anc 1211	. . . 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 12006	. . . . . 6 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
62		mcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
63		3exp3 14101	. . . . . . . 8 |- ( 3 ^ 3 ) = ; 2 7
64	63	a1i 11	. . . . . . 7 |- ( ph -> ( 3 ^ 3 ) = ; 2 7 )
65	62, 64	oveq12d 6098	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
66		mcubic.g	. . . . . . . . 9 |- ( ph -> G e. CC )
67	35, 66	addcld 9393	. . . . . . . 8 |- ( ph -> ( N + G ) e. CC )
68		2cnd 10382	. . . . . . . 8 |- ( ph -> 2 e. CC )
69		2ne0 10402	. . . . . . . . 9 |- 2 =/= 0
70	69	a1i 11	. . . . . . . 8 |- ( ph -> 2 =/= 0 )
71	67, 68, 36, 70, 38	divdiv32d 10120	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
72	35, 66	addcomd 9559	. . . . . . . . . 10 |- ( ph -> ( N + G ) = ( G + N ) )
73	72	oveq1d 6095	. . . . . . . . 9 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
74	66, 35, 36, 38	divdird 10133	. . . . . . . . 9 |- ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
75	73, 74	eqtrd 2465	. . . . . . . 8 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
76	75	oveq1d 6095	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
77	66, 36, 38	divcld 10095	. . . . . . . 8 |- ( ph -> ( G / ; 2 7 ) e. CC )
78	77, 39, 68, 70	divdird 10133	. . . . . . 7 |- ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
79	71, 76, 78	3eqtrd 2469	. . . . . 6 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
80	61, 65, 79	3eqtrd 2469	. . . . 5 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
81	80	negeqd 9592	. . . 4 |- ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
82	77	halfcld 10557	. . . . 5 |- ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
83	39	halfcld 10557	. . . . 5 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
84	82, 83	negdi2d 9721	. . . 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 2469	. . 3 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
86	82	negcld 9694	. . 3 |- ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
87		sqneg 11910	. . . . 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 12005	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
90	39, 68, 70	sqdivd 12005	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
91	35, 36, 38	sqdivd 12005	. . . . . . . . 9 |- ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) )
92	91	oveq1d 6095	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
93	90, 92	eqtr2d 2466	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
94		4cn 10387	. . . . . . . . . . . 12 |- 4 e. CC
95	94	a1i 11	. . . . . . . . . . 11 |- ( ph -> 4 e. CC )
96		expcl 11867	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
97	9, 17, 96	sylancl 655	. . . . . . . . . . 11 |- ( ph -> ( M ^ 3 ) e. CC )
98	30	sqcli 11930	. . . . . . . . . . . 12 |- (; 2 7 ^ 2 ) e. CC
99	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) e. CC )
100		sqne0 11916	. . . . . . . . . . . . 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 10130	. . . . . . . . . 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 10474	. . . . . . . . . . . . . . 15 |- 9 e. NN
106	105	nnne0i 10344	. . . . . . . . . . . . . 14 |- 9 =/= 0
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 =/= 0 )
108	9, 104, 107, 60	expdivd 12006	. . . . . . . . . . . 12 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
109	16, 4	mulcomi 9380	. . . . . . . . . . . . . . . 16 |- ( 2 x. 3 ) = ( 3 x. 2 )
110	109	oveq2i 6091	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
111		expmul 11893	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
112	4, 27, 17, 111	mp3an 1307	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
113		expmul 11893	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
114	4, 17, 27, 113	mp3an 1307	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
115	110, 112, 114	3eqtr3i 2461	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
116		sq3 11947	. . . . . . . . . . . . . . 15 |- ( 3 ^ 2 ) = 9
117	116	oveq1i 6090	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
118	63	oveq1i 6090	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 3 ) ^ 2 ) = (; 2 7 ^ 2 )
119	115, 117, 118	3eqtr3i 2461	. . . . . . . . . . . . 13 |- ( 9 ^ 3 ) = (; 2 7 ^ 2 )
120	119	oveq2i 6091	. . . . . . . . . . . 12 |- ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) )
121	108, 120	syl6eq 2481	. . . . . . . . . . 11 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) )
122	121	oveq2d 6096	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
123	103, 122	eqtr4d 2468	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
124	123	oveq1d 6095	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
125		sq2 11946	. . . . . . . . . 10 |- ( 2 ^ 2 ) = 4
126	125	oveq2i 6091	. . . . . . . . 9 |- ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
127	9, 104, 107	divcld 10095	. . . . . . . . . . 11 |- ( ph -> ( M / 9 ) e. CC )
128		expcl 11867	. . . . . . . . . . 11 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
129	127, 17, 128	sylancl 655	. . . . . . . . . 10 |- ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
130		4ne0 10406	. . . . . . . . . . 11 |- 4 =/= 0
131	130	a1i 11	. . . . . . . . . 10 |- ( ph -> 4 =/= 0 )
132	129, 95, 131	divcan3d 10100	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
133	126, 132	syl5eq 2477	. . . . . . . 8 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
134	124, 133	eqtrd 2465	. . . . . . 7 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
135	93, 134	oveq12d 6098	. . . . . 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 11990	. . . . . . . 8 |- ( ph -> ( N ^ 2 ) e. CC )
137	136, 99, 102	divcld 10095	. . . . . . 7 |- ( ph -> ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) e. CC )
138		mulcl 9354	. . . . . . . . 9 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
139	94, 97, 138	sylancr 656	. . . . . . . 8 |- ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
140	139, 99, 102	divcld 10095	. . . . . . 7 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) e. CC )
141	16	sqcli 11930	. . . . . . . 8 |- ( 2 ^ 2 ) e. CC
142	141	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) e. CC )
143	125, 130	eqnetri 2615	. . . . . . . 8 |- ( 2 ^ 2 ) =/= 0
144	143	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) =/= 0 )
145	137, 140, 142, 144	divsubdird 10134	. . . . . 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 11990	. . . . . . 7 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
147	146, 129	negsubd 9713	. . . . . 6 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
148	135, 145, 147	3eqtr4d 2475	. . . . 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 12005	. . . . . . 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 6095	. . . . . . 7 |- ( ph -> ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) )
152	136, 139, 99, 102	divsubdird 10134	. . . . . . 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 2469	. . . . . 6 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
154	153	oveq1d 6095	. . . . 5 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
155		oexpneg 13578	. . . . . . 7 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
156	127, 47, 57, 155	syl3anc 1211	. . . . . 6 |- ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
157	156	oveq2d 6096	. . . . 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 2475	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
159	88, 89, 158	3eqtrd 2469	. . 3 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
160	9, 10, 10, 12, 12	divdiv1d 10126	. . . . . 6 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
161		3t3e9 10462	. . . . . . 7 |- ( 3 x. 3 ) = 9
162	161	oveq2i 6091	. . . . . 6 |- ( M / ( 3 x. 3 ) ) = ( M / 9 )
163	160, 162	syl6eq 2481	. . . . 5 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
164	163	negeqd 9592	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
165	13, 10, 12	divnegd 10108	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
166	164, 165	eqtr3d 2467	. . 3 |- ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
167		eqidd 2434	. . 3 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
168		mcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
169	43, 10, 168, 12	divne0d 10111	. . . 4 |- ( ph -> ( T / 3 ) =/= 0 )
170	44, 169	negne0d 9705	. . 3 |- ( ph -> -u ( T / 3 ) =/= 0 )
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 22126	. 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 11969	. . . . . . 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 654	. . . . . 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 11990	. . . . . . . . . 10 |- ( ph -> ( X ^ 2 ) e. CC )
175	10, 174, 41	mul12d 9566	. . . . . . . . 9 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
176	2, 10, 12	divcan2d 10097	. . . . . . . . . 10 |- ( ph -> ( 3 x. ( B / 3 ) ) = B )
177	176	oveq2d 6096	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
178	174, 2	mulcomd 9395	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
179	175, 177, 178	3eqtrd 2469	. . . . . . . 8 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
180	179	oveq2d 6096	. . . . . . 7 |- ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
181	180	oveq1d 6095	. . . . . 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 2465	. . . . 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 6095	. . . 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 11867	. . . . . . 7 |- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
185	40, 17, 184	sylancl 655	. . . . . 6 |- ( ph -> ( X ^ 3 ) e. CC )
186	2, 174	mulcld 9394	. . . . . 6 |- ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
187	185, 186	addcld 9393	. . . . 5 |- ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
188	41	sqcld 11990	. . . . . . . 8 |- ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
189	40, 188	mulcld 9394	. . . . . . 7 |- ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
190	10, 189	mulcld 9394	. . . . . 6 |- ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
191		expcl 11867	. . . . . . 7 |- ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
192	41, 17, 191	sylancl 655	. . . . . 6 |- ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
193	190, 192	addcld 9393	. . . . 5 |- ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
194	14, 42	mulcld 9394	. . . . . 6 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
195	194, 39	addcld 9393	. . . . 5 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
196	187, 193, 195	addassd 9396	. . . 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 9398	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
198	197	oveq1d 6095	. . . . . . . . 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 9394	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
200	14, 41	mulcld 9394	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
201	199, 200, 39	addassd 9396	. . . . . . . . 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 6095	. . . . . . . . . . . . . . 15 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
203	3, 7, 10, 12	divsubdird 10134	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
204	5, 10, 12	divcan3d 10100	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 3 x. C ) / 3 ) = C )
205	204	oveq2d 6096	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
206	202, 203, 205	3eqtrd 2469	. . . . . . . . . . . . . 14 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
207	206	negeqd 9592	. . . . . . . . . . . . 13 |- ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
208	3, 10, 12	divcld 10095	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
209	208, 5	negsubdi2d 9723	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
210	207, 209	eqtrd 2465	. . . . . . . . . . . 12 |- ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
211	210	oveq1d 6095	. . . . . . . . . . 11 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
212	5, 208, 40	subdird 9789	. . . . . . . . . . 11 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
213	208, 40	mulcomd 9395	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
214	4	sqvali 11929	. . . . . . . . . . . . . . . . . 18 |- ( 3 ^ 2 ) = ( 3 x. 3 )
215	214	oveq2i 6091	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
216	2, 10, 12	sqdivd 12005	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
217	3, 10, 10, 12, 12	divdiv1d 10126	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
218	215, 216, 217	3eqtr4a 2491	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
219	218	oveq2d 6096	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
220	208, 10, 12	divcan2d 10097	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
221	219, 220	eqtrd 2465	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
222	221	oveq2d 6096	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
223	40, 10, 188	mul12d 9566	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
224	213, 222, 223	3eqtr2d 2471	. . . . . . . . . . . 12 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
225	224	oveq2d 6096	. . . . . . . . . . 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 2469	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
227	210	oveq1d 6095	. . . . . . . . . . . . 13 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
228	5, 208, 41	subdird 9789	. . . . . . . . . . . . 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 10130	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
230	5, 2	mulcomd 9395	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C x. B ) = ( B x. C ) )
231	230	oveq1d 6095	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
232	229, 231	eqtr3d 2467	. . . . . . . . . . . . . 14 |- ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
233	3, 10, 2, 10, 12, 12	divmuldivd 10136	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
234		df-3 10369	. . . . . . . . . . . . . . . . . 18 |- 3 = ( 2 + 1 )
235	234	oveq2i 6091	. . . . . . . . . . . . . . . . 17 |- ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
236		expp1 11856	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
237	2, 27, 236	sylancl 655	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
238	235, 237	syl5req 2478	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
239	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 x. 3 ) = 9 )
240	238, 239	oveq12d 6098	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
241	233, 240	eqtrd 2465	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
242	232, 241	oveq12d 6098	. . . . . . . . . . . . 13 |- ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
243	227, 228, 242	3eqtrd 2469	. . . . . . . . . . . 12 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
244	15	oveq1d 6095	. . . . . . . . . . . . 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 10133	. . . . . . . . . . . . 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 10134	. . . . . . . . . . . . . . 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 10839	. . . . . . . . . . . . . . . . . 18 |- ( 9 x. 3 ) = ; 2 7
248	247	oveq2i 6091	. . . . . . . . . . . . . . . . 17 |- ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
249	23, 10, 104, 12, 107	divcan5d 10121	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
250	248, 249	syl5eqr 2479	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
251	250	oveq2d 6096	. . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . 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 10100	. . . . . . . . . . . . . 14 |- ( ph -> ( (; 2 7 x. D ) / ; 2 7 ) = D )
254	252, 253	oveq12d 6098	. . . . . . . . . . . . 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 2469	. . . . . . . . . . . 12 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
256	243, 255	oveq12d 6098	. . . . . . . . . . 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 10095	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
258	21, 36, 38	divcld 10095	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
259	257, 258	negsubdi2d 9723	. . . . . . . . . . . . . 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 12006	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
261	63	oveq2i 6091	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
262		ax-1cn 9328	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
263	4, 16, 262, 53	subaddrii 9685	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 - 2 ) = 1
264	263	oveq1i 6090	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
265	19	mulid2d 9392	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
266	264, 265	syl5eq 2477	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
267	10, 68, 19	subdird 9789	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
268	266, 267	eqtr3d 2467	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
269	268	oveq1d 6095	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
270		mulcl 9354	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
271	4, 19, 270	sylancr 656	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
272	271, 21, 36, 38	divsubdird 10134	. . . . . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274	261, 273	syl5eq 2477	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275	22, 4, 247	mulcomli 9381	. . . . . . . . . . . . . . . . . . 19 |- ( 3 x. 9 ) = ; 2 7
276	275	oveq2i 6091	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
277	19, 104, 10, 107, 12	divcan5d 10121	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
278	276, 277	syl5eqr 2479	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
279	278	oveq1d 6095	. . . . . . . . . . . . . . . 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 2469	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
281	280	negeqd 9592	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
282	23, 10, 12	divcld 10095	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B x. C ) / 3 ) e. CC )
283	282, 257, 258	npncan3d 9743	. . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . 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 6095	. . . . . . . . . . . 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 9694	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
287	286, 31	addcomd 9559	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
288	243, 200	eqeltrrd 2508	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
289	258, 282	subcld 9707	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
290	288, 289, 31	addassd 9396	. . . . . . . . . . . 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 2473	. . . . . . . . . . 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 9713	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
293	256, 291, 292	3eqtr2d 2471	. . . . . . . . . 10 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
294	226, 293	oveq12d 6098	. . . . . . . . 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 2469	. . . . . . . 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 9394	. . . . . . . . 9 |- ( ph -> ( C x. X ) e. CC )
297	296, 31, 190, 192	addsub4d 9754	. . . . . . . 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 2468	. . . . . . 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 6096	. . . . . 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 9393	. . . . . . 7 |- ( ph -> ( ( C x. X ) + D ) e. CC )
301	193, 300	pncan3d 9710	. . . . . 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 2465	. . . . 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 6096	. . . 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 2469	. . 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 2441	. 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 6087	. . . . . . . 8 |- ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
307		0exp 11883	. . . . . . . . 9 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
308	46, 307	ax-mp 5	. . . . . . . 8 |- ( 0 ^ 3 ) = 0
309	306, 308	syl6eq 2481	. . . . . . 7 |- ( r = 0 -> ( r ^ 3 ) = 0 )
310		0ne1 10377	. . . . . . . 8 |- 0 =/= 1
311	310	a1i 11	. . . . . . 7 |- ( r = 0 -> 0 =/= 1 )
312	309, 311	eqnetrd 2616	. . . . . 6 |- ( r = 0 -> ( r ^ 3 ) =/= 1 )
313	312	necon2i 2648	. . . . 5 |- ( ( r ^ 3 ) = 1 -> r =/= 0 )
314		eqcom 2435	. . . . . . . 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 462	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
316		simprl 748	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
317	43	adantr 462	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
318	316, 317	mulcld 9394	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
319	9	adantr 462	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
320		simprr 749	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
321	168	adantr 462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
322	316, 317, 320, 321	mulne0d 9976	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
323	319, 318, 322	divcld 10095	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
324	318, 323	addcld 9393	. . . . . . . . . . . . 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 10133	. . . . . . . . . . . 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 9396	. . . . . . . . . . . . 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 6095	. . . . . . . . . . . 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 462	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
331	324, 325, 326	divcld 10095	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
332	330, 331	subnegd 9714	. . . . . . . . . . . 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 2475	. . . . . . . . . . 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 9592	. . . . . . . . . 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 9694	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
336	330, 335	negsubdi2d 9723	. . . . . . . . . 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 2465	. . . . . . . . 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 2441	. . . . . . . 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 462	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
341	335, 330, 340	subadd2d 9726	. . . . . . 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 10133	. . . . . . . . . 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 9592	. . . . . . . . 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 10095	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
345	323, 325, 326	divcld 10095	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
346	344, 345	negdi2d 9721	. . . . . . . . 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 10130	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
348	347	negeqd 9592	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
349	44	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
350	316, 349	mulneg2d 9786	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
351	348, 350	eqtr4d 2468	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
352	319, 318, 325, 322, 326	divdiv32d 10120	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
353	13	adantr 462	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
354	353, 318, 325, 322, 326	divcan7d 10123	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
355	163	oveq1d 6095	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
356	355	adantr 462	. . . . . . . . . . . 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 2471	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
358	127	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
359	318, 325, 322, 326	divne0d 10111	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
360	358, 344, 359	div2negd 10110	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
361	351	oveq2d 6096	. . . . . . . . . . 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 2471	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
363	351, 362	oveq12d 6098	. . . . . . . . 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 2469	. . . . . . . 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 2444	. . . . . . 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 641	. . . . 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 471	. . . 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 634	. . 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 2722	. 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 1362   e. wcel 1755   =/= wne 2596   E.wrex 2706   class class class wbr 4280  (class class class)co 6080   CCcc 9268   0cc0 9270   1c1 9271   + caddc 9273   x. cmul 9275   - cmin 9583   -ucneg 9584   / cdiv 9981   NNcn 10310   2c2 10359   3c3 10360   4c4 10361   7c7 10364   9c9 10366   NN0cn0 10567  ;cdc 10743   ^cexp 11849   || cdivides 13518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-sup 7679  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-rp 10980  df-fz 11425  df-seq 11791  df-exp 11850  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-dvds 13519

This theorem is referenced by:  cubic2  22128  quart  22141