Theorem mcubic 24574

Description: Solutions to a monic cubic equation, a special case of cubic 24576. (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 13006	. . . . . . 7 |- ( ph -> ( B ^ 2 ) e. CC )
4		3cn 11095	. . . . . . . 8 |- 3 e. CC
5		mcubic.c	. . . . . . . 8 |- ( ph -> C e. CC )
6		mulcl 10020	. . . . . . . 8 |- ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
7	4, 5, 6	sylancr 695	. . . . . . 7 |- ( ph -> ( 3 x. C ) e. CC )
8	3, 7	subcld 10392	. . . . . 6 |- ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
9	1, 8	eqeltrd 2701	. . . . 5 |- ( ph -> M e. CC )
10	4	a1i 11	. . . . 5 |- ( ph -> 3 e. CC )
11		3ne0 11115	. . . . . 6 |- 3 =/= 0
12	11	a1i 11	. . . . 5 |- ( ph -> 3 =/= 0 )
13	9, 10, 12	divcld 10801	. . . 4 |- ( ph -> ( M / 3 ) e. CC )
14	13	negcld 10379	. . 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 11091	. . . . . . . 8 |- 2 e. CC
17		3nn0 11310	. . . . . . . . 9 |- 3 e. NN0
18		expcl 12878	. . . . . . . . 9 |- ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
19	2, 17, 18	sylancl 694	. . . . . . . 8 |- ( ph -> ( B ^ 3 ) e. CC )
20		mulcl 10020	. . . . . . . 8 |- ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
21	16, 19, 20	sylancr 695	. . . . . . 7 |- ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
22		9cn 11108	. . . . . . . 8 |- 9 e. CC
23	2, 5	mulcld 10060	. . . . . . . 8 |- ( ph -> ( B x. C ) e. CC )
24		mulcl 10020	. . . . . . . 8 |- ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
25	22, 23, 24	sylancr 695	. . . . . . 7 |- ( ph -> ( 9 x. ( B x. C ) ) e. CC )
26	21, 25	subcld 10392	. . . . . 6 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
27		2nn0 11309	. . . . . . . . 9 |- 2 e. NN0
28		7nn 11190	. . . . . . . . 9 |- 7 e. NN
29	27, 28	decnncl 11518	. . . . . . . 8 |- ; 2 7 e. NN
30	29	nncni 11030	. . . . . . 7 |- ; 2 7 e. CC
31		mcubic.d	. . . . . . 7 |- ( ph -> D e. CC )
32		mulcl 10020	. . . . . . 7 |- ( (; 2 7 e. CC /\ D e. CC ) -> (; 2 7 x. D ) e. CC )
33	30, 31, 32	sylancr 695	. . . . . 6 |- ( ph -> (; 2 7 x. D ) e. CC )
34	26, 33	addcld 10059	. . . . 5 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) e. CC )
35	15, 34	eqeltrd 2701	. . . 4 |- ( ph -> N e. CC )
36	30	a1i 11	. . . 4 |- ( ph -> ; 2 7 e. CC )
37	29	nnne0i 11055	. . . . 5 |- ; 2 7 =/= 0
38	37	a1i 11	. . . 4 |- ( ph -> ; 2 7 =/= 0 )
39	35, 36, 38	divcld 10801	. . 3 |- ( ph -> ( N / ; 2 7 ) e. CC )
40		mcubic.x	. . . 4 |- ( ph -> X e. CC )
41	2, 10, 12	divcld 10801	. . . 4 |- ( ph -> ( B / 3 ) e. CC )
42	40, 41	addcld 10059	. . 3 |- ( ph -> ( X + ( B / 3 ) ) e. CC )
43		mcubic.t	. . . . 5 |- ( ph -> T e. CC )
44	43, 10, 12	divcld 10801	. . . 4 |- ( ph -> ( T / 3 ) e. CC )
45	44	negcld 10379	. . 3 |- ( ph -> -u ( T / 3 ) e. CC )
46		3nn 11186	. . . . . 6 |- 3 e. NN
47	46	a1i 11	. . . . 5 |- ( ph -> 3 e. NN )
48		2nn 11185	. . . . . . 7 |- 2 e. NN
49		1nn0 11308	. . . . . . 7 |- 1 e. NN0
50		1nn 11031	. . . . . . 7 |- 1 e. NN
51		2t1e2 11176	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
52	51	oveq1i 6660	. . . . . . . 8 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
53		2p1e3 11151	. . . . . . . 8 |- ( 2 + 1 ) = 3
54	52, 53	eqtri 2644	. . . . . . 7 |- ( ( 2 x. 1 ) + 1 ) = 3
55		1lt2 11194	. . . . . . 7 |- 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 15136	. . . . . 6 |- -. 2 || 3
57	56	a1i 11	. . . . 5 |- ( ph -> -. 2 || 3 )
58		oexpneg 15069	. . . . 5 |- ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
59	44, 47, 57, 58	syl3anc 1326	. . . 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 13022	. . . . . 6 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
62		mcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
63		3exp3 15798	. . . . . . . 8 |- ( 3 ^ 3 ) = ; 2 7
64	63	a1i 11	. . . . . . 7 |- ( ph -> ( 3 ^ 3 ) = ; 2 7 )
65	62, 64	oveq12d 6668	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
66		mcubic.g	. . . . . . . . 9 |- ( ph -> G e. CC )
67	35, 66	addcld 10059	. . . . . . . 8 |- ( ph -> ( N + G ) e. CC )
68		2cnd 11093	. . . . . . . 8 |- ( ph -> 2 e. CC )
69		2ne0 11113	. . . . . . . . 9 |- 2 =/= 0
70	69	a1i 11	. . . . . . . 8 |- ( ph -> 2 =/= 0 )
71	67, 68, 36, 70, 38	divdiv32d 10826	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
72	35, 66	addcomd 10238	. . . . . . . . . 10 |- ( ph -> ( N + G ) = ( G + N ) )
73	72	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
74	66, 35, 36, 38	divdird 10839	. . . . . . . . 9 |- ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
75	73, 74	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
76	75	oveq1d 6665	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
77	66, 36, 38	divcld 10801	. . . . . . . 8 |- ( ph -> ( G / ; 2 7 ) e. CC )
78	77, 39, 68, 70	divdird 10839	. . . . . . 7 |- ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
79	71, 76, 78	3eqtrd 2660	. . . . . 6 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
80	61, 65, 79	3eqtrd 2660	. . . . 5 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
81	80	negeqd 10275	. . . 4 |- ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
82	77	halfcld 11277	. . . . 5 |- ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
83	39	halfcld 11277	. . . . 5 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
84	82, 83	negdi2d 10406	. . . 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 2660	. . 3 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
86	82	negcld 10379	. . 3 |- ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
87		sqneg 12923	. . . . 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 13021	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
90	39, 68, 70	sqdivd 13021	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
91	35, 36, 38	sqdivd 13021	. . . . . . . . 9 |- ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) )
92	91	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
93	90, 92	eqtr2d 2657	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
94		4cn 11098	. . . . . . . . . . . 12 |- 4 e. CC
95	94	a1i 11	. . . . . . . . . . 11 |- ( ph -> 4 e. CC )
96		expcl 12878	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
97	9, 17, 96	sylancl 694	. . . . . . . . . . 11 |- ( ph -> ( M ^ 3 ) e. CC )
98	30	sqcli 12944	. . . . . . . . . . . 12 |- (; 2 7 ^ 2 ) e. CC
99	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) e. CC )
100		sqne0 12930	. . . . . . . . . . . . 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 247	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) =/= 0 )
103	95, 97, 99, 102	divassd 10836	. . . . . . . . . 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 11192	. . . . . . . . . . . . . . 15 |- 9 e. NN
106	105	nnne0i 11055	. . . . . . . . . . . . . 14 |- 9 =/= 0
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 =/= 0 )
108	9, 104, 107, 60	expdivd 13022	. . . . . . . . . . . 12 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
109	16, 4	mulcomi 10046	. . . . . . . . . . . . . . . 16 |- ( 2 x. 3 ) = ( 3 x. 2 )
110	109	oveq2i 6661	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
111		expmul 12905	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
112	4, 27, 17, 111	mp3an 1424	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
113		expmul 12905	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
114	4, 17, 27, 113	mp3an 1424	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
115	110, 112, 114	3eqtr3i 2652	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
116		sq3 12961	. . . . . . . . . . . . . . 15 |- ( 3 ^ 2 ) = 9
117	116	oveq1i 6660	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
118	63	oveq1i 6660	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 3 ) ^ 2 ) = (; 2 7 ^ 2 )
119	115, 117, 118	3eqtr3i 2652	. . . . . . . . . . . . 13 |- ( 9 ^ 3 ) = (; 2 7 ^ 2 )
120	119	oveq2i 6661	. . . . . . . . . . . 12 |- ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) )
121	108, 120	syl6eq 2672	. . . . . . . . . . 11 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) )
122	121	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
123	103, 122	eqtr4d 2659	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
124	123	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
125		sq2 12960	. . . . . . . . . 10 |- ( 2 ^ 2 ) = 4
126	125	oveq2i 6661	. . . . . . . . 9 |- ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
127	9, 104, 107	divcld 10801	. . . . . . . . . . 11 |- ( ph -> ( M / 9 ) e. CC )
128		expcl 12878	. . . . . . . . . . 11 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
129	127, 17, 128	sylancl 694	. . . . . . . . . 10 |- ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
130		4ne0 11117	. . . . . . . . . . 11 |- 4 =/= 0
131	130	a1i 11	. . . . . . . . . 10 |- ( ph -> 4 =/= 0 )
132	129, 95, 131	divcan3d 10806	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
133	126, 132	syl5eq 2668	. . . . . . . 8 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
134	124, 133	eqtrd 2656	. . . . . . 7 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
135	93, 134	oveq12d 6668	. . . . . 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 13006	. . . . . . . 8 |- ( ph -> ( N ^ 2 ) e. CC )
137	136, 99, 102	divcld 10801	. . . . . . 7 |- ( ph -> ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) e. CC )
138		mulcl 10020	. . . . . . . . 9 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
139	94, 97, 138	sylancr 695	. . . . . . . 8 |- ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
140	139, 99, 102	divcld 10801	. . . . . . 7 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) e. CC )
141	16	sqcli 12944	. . . . . . . 8 |- ( 2 ^ 2 ) e. CC
142	141	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) e. CC )
143	125, 130	eqnetri 2864	. . . . . . . 8 |- ( 2 ^ 2 ) =/= 0
144	143	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) =/= 0 )
145	137, 140, 142, 144	divsubdird 10840	. . . . . 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 13006	. . . . . . 7 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
147	146, 129	negsubd 10398	. . . . . 6 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
148	135, 145, 147	3eqtr4d 2666	. . . . 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 13021	. . . . . . 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 6665	. . . . . . 7 |- ( ph -> ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) )
152	136, 139, 99, 102	divsubdird 10840	. . . . . . 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 2660	. . . . . 6 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
154	153	oveq1d 6665	. . . . 5 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
155		oexpneg 15069	. . . . . . 7 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
156	127, 47, 57, 155	syl3anc 1326	. . . . . 6 |- ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
157	156	oveq2d 6666	. . . . 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 2666	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
159	88, 89, 158	3eqtrd 2660	. . 3 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
160	9, 10, 10, 12, 12	divdiv1d 10832	. . . . . 6 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
161		3t3e9 11180	. . . . . . 7 |- ( 3 x. 3 ) = 9
162	161	oveq2i 6661	. . . . . 6 |- ( M / ( 3 x. 3 ) ) = ( M / 9 )
163	160, 162	syl6eq 2672	. . . . 5 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
164	163	negeqd 10275	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
165	13, 10, 12	divnegd 10814	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
166	164, 165	eqtr3d 2658	. . 3 |- ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
167		eqidd 2623	. . 3 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
168		mcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
169	43, 10, 168, 12	divne0d 10817	. . . 4 |- ( ph -> ( T / 3 ) =/= 0 )
170	44, 169	negne0d 10390	. . 3 |- ( ph -> -u ( T / 3 ) =/= 0 )
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 24573	. 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 12985	. . . . . . 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 693	. . . . . 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 13006	. . . . . . . . . 10 |- ( ph -> ( X ^ 2 ) e. CC )
175	10, 174, 41	mul12d 10245	. . . . . . . . 9 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
176	2, 10, 12	divcan2d 10803	. . . . . . . . . 10 |- ( ph -> ( 3 x. ( B / 3 ) ) = B )
177	176	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
178	174, 2	mulcomd 10061	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
179	175, 177, 178	3eqtrd 2660	. . . . . . . 8 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
180	179	oveq2d 6666	. . . . . . 7 |- ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
181	180	oveq1d 6665	. . . . . 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 2656	. . . . 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 6665	. . . 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 12878	. . . . . . 7 |- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
185	40, 17, 184	sylancl 694	. . . . . 6 |- ( ph -> ( X ^ 3 ) e. CC )
186	2, 174	mulcld 10060	. . . . . 6 |- ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
187	185, 186	addcld 10059	. . . . 5 |- ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
188	41	sqcld 13006	. . . . . . . 8 |- ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
189	40, 188	mulcld 10060	. . . . . . 7 |- ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
190	10, 189	mulcld 10060	. . . . . 6 |- ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
191		expcl 12878	. . . . . . 7 |- ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
192	41, 17, 191	sylancl 694	. . . . . 6 |- ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
193	190, 192	addcld 10059	. . . . 5 |- ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
194	14, 42	mulcld 10060	. . . . . 6 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
195	194, 39	addcld 10059	. . . . 5 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
196	187, 193, 195	addassd 10062	. . . 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 10064	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
198	197	oveq1d 6665	. . . . . . . . 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 10060	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
200	14, 41	mulcld 10060	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
201	199, 200, 39	addassd 10062	. . . . . . . . 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 6665	. . . . . . . . . . . . . . 15 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
203	3, 7, 10, 12	divsubdird 10840	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
204	5, 10, 12	divcan3d 10806	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 3 x. C ) / 3 ) = C )
205	204	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
206	202, 203, 205	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
207	206	negeqd 10275	. . . . . . . . . . . . 13 |- ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
208	3, 10, 12	divcld 10801	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
209	208, 5	negsubdi2d 10408	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
210	207, 209	eqtrd 2656	. . . . . . . . . . . 12 |- ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
211	210	oveq1d 6665	. . . . . . . . . . 11 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
212	5, 208, 40	subdird 10487	. . . . . . . . . . 11 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
213	208, 40	mulcomd 10061	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
214	4	sqvali 12943	. . . . . . . . . . . . . . . . . 18 |- ( 3 ^ 2 ) = ( 3 x. 3 )
215	214	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
216	2, 10, 12	sqdivd 13021	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
217	3, 10, 10, 12, 12	divdiv1d 10832	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
218	215, 216, 217	3eqtr4a 2682	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
219	218	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
220	208, 10, 12	divcan2d 10803	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
221	219, 220	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
222	221	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
223	40, 10, 188	mul12d 10245	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
224	213, 222, 223	3eqtr2d 2662	. . . . . . . . . . . 12 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
225	224	oveq2d 6666	. . . . . . . . . . 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 2660	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
227	210	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
228	5, 208, 41	subdird 10487	. . . . . . . . . . . . 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 10836	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
230	5, 2	mulcomd 10061	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C x. B ) = ( B x. C ) )
231	230	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
232	229, 231	eqtr3d 2658	. . . . . . . . . . . . . 14 |- ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
233	3, 10, 2, 10, 12, 12	divmuldivd 10842	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
234		df-3 11080	. . . . . . . . . . . . . . . . . 18 |- 3 = ( 2 + 1 )
235	234	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
236		expp1 12867	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
237	2, 27, 236	sylancl 694	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
238	235, 237	syl5req 2669	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
239	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 x. 3 ) = 9 )
240	238, 239	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
241	233, 240	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
242	232, 241	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
243	227, 228, 242	3eqtrd 2660	. . . . . . . . . . . 12 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
244	15	oveq1d 6665	. . . . . . . . . . . . 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 10839	. . . . . . . . . . . . 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 10840	. . . . . . . . . . . . . . 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 11664	. . . . . . . . . . . . . . . . . 18 |- ( 9 x. 3 ) = ; 2 7
248	247	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
249	23, 10, 104, 12, 107	divcan5d 10827	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
250	248, 249	syl5eqr 2670	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
251	250	oveq2d 6666	. . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . 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 10806	. . . . . . . . . . . . . 14 |- ( ph -> ( (; 2 7 x. D ) / ; 2 7 ) = D )
254	252, 253	oveq12d 6668	. . . . . . . . . . . . 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 2660	. . . . . . . . . . . 12 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
256	243, 255	oveq12d 6668	. . . . . . . . . . 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 10801	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
258	21, 36, 38	divcld 10801	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
259	257, 258	negsubdi2d 10408	. . . . . . . . . . . . . 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 13022	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
261	63	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
262		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
263	4, 16, 262, 53	subaddrii 10370	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 - 2 ) = 1
264	263	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
265	19	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
266	264, 265	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
267	10, 68, 19	subdird 10487	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
268	266, 267	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
269	268	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
270		mulcl 10020	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
271	4, 19, 270	sylancr 695	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
272	271, 21, 36, 38	divsubdird 10840	. . . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274	261, 273	syl5eq 2668	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275	22, 4, 247	mulcomli 10047	. . . . . . . . . . . . . . . . . . 19 |- ( 3 x. 9 ) = ; 2 7
276	275	oveq2i 6661	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
277	19, 104, 10, 107, 12	divcan5d 10827	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
278	276, 277	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
279	278	oveq1d 6665	. . . . . . . . . . . . . . . 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 2660	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
281	280	negeqd 10275	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
282	23, 10, 12	divcld 10801	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B x. C ) / 3 ) e. CC )
283	282, 257, 258	npncan3d 10428	. . . . . . . . . . . . . 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 2666	. . . . . . . . . . . . 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 6665	. . . . . . . . . . . 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 10379	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
287	286, 31	addcomd 10238	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
288	243, 200	eqeltrrd 2702	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
289	258, 282	subcld 10392	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
290	288, 289, 31	addassd 10062	. . . . . . . . . . . 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 2664	. . . . . . . . . . 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 10398	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
293	256, 291, 292	3eqtr2d 2662	. . . . . . . . . 10 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
294	226, 293	oveq12d 6668	. . . . . . . . 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 2660	. . . . . . . 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 10060	. . . . . . . . 9 |- ( ph -> ( C x. X ) e. CC )
297	296, 31, 190, 192	addsub4d 10439	. . . . . . . 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 2659	. . . . . . 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 6666	. . . . . 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 10059	. . . . . . 7 |- ( ph -> ( ( C x. X ) + D ) e. CC )
301	193, 300	pncan3d 10395	. . . . . 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 2656	. . . . 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 6666	. . . 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 2660	. . 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 2624	. 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 6657	. . . . . . . 8 |- ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
307		0exp 12895	. . . . . . . . 9 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
308	46, 307	ax-mp 5	. . . . . . . 8 |- ( 0 ^ 3 ) = 0
309	306, 308	syl6eq 2672	. . . . . . 7 |- ( r = 0 -> ( r ^ 3 ) = 0 )
310		0ne1 11088	. . . . . . . 8 |- 0 =/= 1
311	310	a1i 11	. . . . . . 7 |- ( r = 0 -> 0 =/= 1 )
312	309, 311	eqnetrd 2861	. . . . . 6 |- ( r = 0 -> ( r ^ 3 ) =/= 1 )
313	312	necon2i 2828	. . . . 5 |- ( ( r ^ 3 ) = 1 -> r =/= 0 )
314		eqcom 2629	. . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
316		simprl 794	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
317	43	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
318	316, 317	mulcld 10060	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
319	9	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
320		simprr 796	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
321	168	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
322	316, 317, 320, 321	mulne0d 10679	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
323	319, 318, 322	divcld 10801	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
324	318, 323	addcld 10059	. . . . . . . . . . . . 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 10839	. . . . . . . . . . . 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 10062	. . . . . . . . . . . . 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 6665	. . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
331	324, 325, 326	divcld 10801	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
332	330, 331	subnegd 10399	. . . . . . . . . . . 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 2666	. . . . . . . . . . 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 10275	. . . . . . . . . 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 10379	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
336	330, 335	negsubdi2d 10408	. . . . . . . . . 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 2656	. . . . . . . . 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 2624	. . . . . . . 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 272	. . . . . . 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 481	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
341	335, 330, 340	subadd2d 10411	. . . . . . 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 10839	. . . . . . . . . 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 10275	. . . . . . . . 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 10801	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
345	323, 325, 326	divcld 10801	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
346	344, 345	negdi2d 10406	. . . . . . . . 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 10836	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
348	347	negeqd 10275	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
349	44	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
350	316, 349	mulneg2d 10484	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
351	348, 350	eqtr4d 2659	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
352	319, 318, 325, 322, 326	divdiv32d 10826	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
353	13	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
354	353, 318, 325, 322, 326	divcan7d 10829	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
355	163	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
356	355	adantr 481	. . . . . . . . . . . 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 2662	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
358	127	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
359	318, 325, 322, 326	divne0d 10817	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
360	358, 344, 359	div2negd 10816	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
361	351	oveq2d 6666	. . . . . . . . . . 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 2662	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
363	351, 362	oveq12d 6668	. . . . . . . . 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 2660	. . . . . . . 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 2632	. . . . . . 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 295	. . . . . 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 680	. . . . 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 491	. . . 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 673	. . 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 3049	. 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 298	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 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   class class class wbr 4653  (class class class)co 6650   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   7c7 11075   9c9 11077   NN0cn0 11292  ;cdc 11493   ^cexp 12860   || cdvds 14983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984

This theorem is referenced by:  cubic2  24575  quart  24588