Theorem mcubic 22217

Description: Solutions to a monic cubic equation, a special case of cubic 22219. (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 11998	. . . . . . 7 |- ( ph -> ( B ^ 2 ) e. CC )
4		3cn 10388	. . . . . . . 8 |- 3 e. CC
5		mcubic.c	. . . . . . . 8 |- ( ph -> C e. CC )
6		mulcl 9358	. . . . . . . 8 |- ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
7	4, 5, 6	sylancr 663	. . . . . . 7 |- ( ph -> ( 3 x. C ) e. CC )
8	3, 7	subcld 9711	. . . . . 6 |- ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
9	1, 8	eqeltrd 2512	. . . . 5 |- ( ph -> M e. CC )
10	4	a1i 11	. . . . 5 |- ( ph -> 3 e. CC )
11		3ne0 10408	. . . . . 6 |- 3 =/= 0
12	11	a1i 11	. . . . 5 |- ( ph -> 3 =/= 0 )
13	9, 10, 12	divcld 10099	. . . 4 |- ( ph -> ( M / 3 ) e. CC )
14	13	negcld 9698	. . 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 10384	. . . . . . . 8 |- 2 e. CC
17		3nn0 10589	. . . . . . . . 9 |- 3 e. NN0
18		expcl 11875	. . . . . . . . 9 |- ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
19	2, 17, 18	sylancl 662	. . . . . . . 8 |- ( ph -> ( B ^ 3 ) e. CC )
20		mulcl 9358	. . . . . . . 8 |- ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
21	16, 19, 20	sylancr 663	. . . . . . 7 |- ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
22		9cn 10401	. . . . . . . 8 |- 9 e. CC
23	2, 5	mulcld 9398	. . . . . . . 8 |- ( ph -> ( B x. C ) e. CC )
24		mulcl 9358	. . . . . . . 8 |- ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
25	22, 23, 24	sylancr 663	. . . . . . 7 |- ( ph -> ( 9 x. ( B x. C ) ) e. CC )
26	21, 25	subcld 9711	. . . . . 6 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
27		2nn0 10588	. . . . . . . . 9 |- 2 e. NN0
28		7nn 10476	. . . . . . . . 9 |- 7 e. NN
29	27, 28	decnncl 10760	. . . . . . . 8 |- ; 2 7 e. NN
30	29	nncni 10324	. . . . . . 7 |- ; 2 7 e. CC
31		mcubic.d	. . . . . . 7 |- ( ph -> D e. CC )
32		mulcl 9358	. . . . . . 7 |- ( (; 2 7 e. CC /\ D e. CC ) -> (; 2 7 x. D ) e. CC )
33	30, 31, 32	sylancr 663	. . . . . 6 |- ( ph -> (; 2 7 x. D ) e. CC )
34	26, 33	addcld 9397	. . . . 5 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) e. CC )
35	15, 34	eqeltrd 2512	. . . 4 |- ( ph -> N e. CC )
36	30	a1i 11	. . . 4 |- ( ph -> ; 2 7 e. CC )
37	29	nnne0i 10348	. . . . 5 |- ; 2 7 =/= 0
38	37	a1i 11	. . . 4 |- ( ph -> ; 2 7 =/= 0 )
39	35, 36, 38	divcld 10099	. . 3 |- ( ph -> ( N / ; 2 7 ) e. CC )
40		mcubic.x	. . . 4 |- ( ph -> X e. CC )
41	2, 10, 12	divcld 10099	. . . 4 |- ( ph -> ( B / 3 ) e. CC )
42	40, 41	addcld 9397	. . 3 |- ( ph -> ( X + ( B / 3 ) ) e. CC )
43		mcubic.t	. . . . 5 |- ( ph -> T e. CC )
44	43, 10, 12	divcld 10099	. . . 4 |- ( ph -> ( T / 3 ) e. CC )
45	44	negcld 9698	. . 3 |- ( ph -> -u ( T / 3 ) e. CC )
46		3nn 10472	. . . . . 6 |- 3 e. NN
47	46	a1i 11	. . . . 5 |- ( ph -> 3 e. NN )
48		2nn 10471	. . . . . . 7 |- 2 e. NN
49		1nn0 10587	. . . . . . 7 |- 1 e. NN0
50		1nn 10325	. . . . . . 7 |- 1 e. NN
51		2t1e2 10462	. . . . . . . . 9 |- ( 2 x. 1 ) = 2
52	51	oveq1i 6096	. . . . . . . 8 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
53		2p1e3 10437	. . . . . . . 8 |- ( 2 + 1 ) = 3
54	52, 53	eqtri 2458	. . . . . . 7 |- ( ( 2 x. 1 ) + 1 ) = 3
55		1lt2 10480	. . . . . . 7 |- 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 13606	. . . . . 6 |- -. 2 || 3
57	56	a1i 11	. . . . 5 |- ( ph -> -. 2 || 3 )
58		oexpneg 13587	. . . . 5 |- ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
59	44, 47, 57, 58	syl3anc 1218	. . . 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 12014	. . . . . 6 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
62		mcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
63		3exp3 14110	. . . . . . . 8 |- ( 3 ^ 3 ) = ; 2 7
64	63	a1i 11	. . . . . . 7 |- ( ph -> ( 3 ^ 3 ) = ; 2 7 )
65	62, 64	oveq12d 6104	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
66		mcubic.g	. . . . . . . . 9 |- ( ph -> G e. CC )
67	35, 66	addcld 9397	. . . . . . . 8 |- ( ph -> ( N + G ) e. CC )
68		2cnd 10386	. . . . . . . 8 |- ( ph -> 2 e. CC )
69		2ne0 10406	. . . . . . . . 9 |- 2 =/= 0
70	69	a1i 11	. . . . . . . 8 |- ( ph -> 2 =/= 0 )
71	67, 68, 36, 70, 38	divdiv32d 10124	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
72	35, 66	addcomd 9563	. . . . . . . . . 10 |- ( ph -> ( N + G ) = ( G + N ) )
73	72	oveq1d 6101	. . . . . . . . 9 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
74	66, 35, 36, 38	divdird 10137	. . . . . . . . 9 |- ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
75	73, 74	eqtrd 2470	. . . . . . . 8 |- ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
76	75	oveq1d 6101	. . . . . . 7 |- ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
77	66, 36, 38	divcld 10099	. . . . . . . 8 |- ( ph -> ( G / ; 2 7 ) e. CC )
78	77, 39, 68, 70	divdird 10137	. . . . . . 7 |- ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
79	71, 76, 78	3eqtrd 2474	. . . . . 6 |- ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
80	61, 65, 79	3eqtrd 2474	. . . . 5 |- ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
81	80	negeqd 9596	. . . 4 |- ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
82	77	halfcld 10561	. . . . 5 |- ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
83	39	halfcld 10561	. . . . 5 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
84	82, 83	negdi2d 9725	. . . 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 2474	. . 3 |- ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
86	82	negcld 9698	. . 3 |- ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
87		sqneg 11918	. . . . 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 12013	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
90	39, 68, 70	sqdivd 12013	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
91	35, 36, 38	sqdivd 12013	. . . . . . . . 9 |- ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) )
92	91	oveq1d 6101	. . . . . . . 8 |- ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
93	90, 92	eqtr2d 2471	. . . . . . 7 |- ( ph -> ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
94		4cn 10391	. . . . . . . . . . . 12 |- 4 e. CC
95	94	a1i 11	. . . . . . . . . . 11 |- ( ph -> 4 e. CC )
96		expcl 11875	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
97	9, 17, 96	sylancl 662	. . . . . . . . . . 11 |- ( ph -> ( M ^ 3 ) e. CC )
98	30	sqcli 11938	. . . . . . . . . . . 12 |- (; 2 7 ^ 2 ) e. CC
99	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> (; 2 7 ^ 2 ) e. CC )
100		sqne0 11924	. . . . . . . . . . . . 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 10134	. . . . . . . . . 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 10478	. . . . . . . . . . . . . . 15 |- 9 e. NN
106	105	nnne0i 10348	. . . . . . . . . . . . . 14 |- 9 =/= 0
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 9 =/= 0 )
108	9, 104, 107, 60	expdivd 12014	. . . . . . . . . . . 12 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
109	16, 4	mulcomi 9384	. . . . . . . . . . . . . . . 16 |- ( 2 x. 3 ) = ( 3 x. 2 )
110	109	oveq2i 6097	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
111		expmul 11901	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
112	4, 27, 17, 111	mp3an 1314	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
113		expmul 11901	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
114	4, 17, 27, 113	mp3an 1314	. . . . . . . . . . . . . . 15 |- ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
115	110, 112, 114	3eqtr3i 2466	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
116		sq3 11955	. . . . . . . . . . . . . . 15 |- ( 3 ^ 2 ) = 9
117	116	oveq1i 6096	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
118	63	oveq1i 6096	. . . . . . . . . . . . . 14 |- ( ( 3 ^ 3 ) ^ 2 ) = (; 2 7 ^ 2 )
119	115, 117, 118	3eqtr3i 2466	. . . . . . . . . . . . 13 |- ( 9 ^ 3 ) = (; 2 7 ^ 2 )
120	119	oveq2i 6097	. . . . . . . . . . . 12 |- ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) )
121	108, 120	syl6eq 2486	. . . . . . . . . . 11 |- ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) )
122	121	oveq2d 6102	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / (; 2 7 ^ 2 ) ) ) )
123	103, 122	eqtr4d 2473	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
124	123	oveq1d 6101	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
125		sq2 11954	. . . . . . . . . 10 |- ( 2 ^ 2 ) = 4
126	125	oveq2i 6097	. . . . . . . . 9 |- ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
127	9, 104, 107	divcld 10099	. . . . . . . . . . 11 |- ( ph -> ( M / 9 ) e. CC )
128		expcl 11875	. . . . . . . . . . 11 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
129	127, 17, 128	sylancl 662	. . . . . . . . . 10 |- ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
130		4ne0 10410	. . . . . . . . . . 11 |- 4 =/= 0
131	130	a1i 11	. . . . . . . . . 10 |- ( ph -> 4 =/= 0 )
132	129, 95, 131	divcan3d 10104	. . . . . . . . 9 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
133	126, 132	syl5eq 2482	. . . . . . . 8 |- ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
134	124, 133	eqtrd 2470	. . . . . . 7 |- ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
135	93, 134	oveq12d 6104	. . . . . 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 11998	. . . . . . . 8 |- ( ph -> ( N ^ 2 ) e. CC )
137	136, 99, 102	divcld 10099	. . . . . . 7 |- ( ph -> ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) e. CC )
138		mulcl 9358	. . . . . . . . 9 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
139	94, 97, 138	sylancr 663	. . . . . . . 8 |- ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
140	139, 99, 102	divcld 10099	. . . . . . 7 |- ( ph -> ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) e. CC )
141	16	sqcli 11938	. . . . . . . 8 |- ( 2 ^ 2 ) e. CC
142	141	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) e. CC )
143	125, 130	eqnetri 2620	. . . . . . . 8 |- ( 2 ^ 2 ) =/= 0
144	143	a1i 11	. . . . . . 7 |- ( ph -> ( 2 ^ 2 ) =/= 0 )
145	137, 140, 142, 144	divsubdird 10138	. . . . . 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 11998	. . . . . . 7 |- ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
147	146, 129	negsubd 9717	. . . . . 6 |- ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
148	135, 145, 147	3eqtr4d 2480	. . . . 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 12013	. . . . . . 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 6101	. . . . . . 7 |- ( ph -> ( ( G ^ 2 ) / (; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / (; 2 7 ^ 2 ) ) )
152	136, 139, 99, 102	divsubdird 10138	. . . . . . 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 2474	. . . . . 6 |- ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) )
154	153	oveq1d 6101	. . . . 5 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / (; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / (; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
155		oexpneg 13587	. . . . . . 7 |- ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
156	127, 47, 57, 155	syl3anc 1218	. . . . . 6 |- ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
157	156	oveq2d 6102	. . . . 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 2480	. . . 4 |- ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
159	88, 89, 158	3eqtrd 2474	. . 3 |- ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
160	9, 10, 10, 12, 12	divdiv1d 10130	. . . . . 6 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
161		3t3e9 10466	. . . . . . 7 |- ( 3 x. 3 ) = 9
162	161	oveq2i 6097	. . . . . 6 |- ( M / ( 3 x. 3 ) ) = ( M / 9 )
163	160, 162	syl6eq 2486	. . . . 5 |- ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
164	163	negeqd 9596	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
165	13, 10, 12	divnegd 10112	. . . 4 |- ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
166	164, 165	eqtr3d 2472	. . 3 |- ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
167		eqidd 2439	. . 3 |- ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
168		mcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
169	43, 10, 168, 12	divne0d 10115	. . . 4 |- ( ph -> ( T / 3 ) =/= 0 )
170	44, 169	negne0d 9709	. . 3 |- ( ph -> -u ( T / 3 ) =/= 0 )
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 22216	. 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 11977	. . . . . . 7 |- ( ( X e. CC /\ ( B / 3 ) e. CC ) -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
173	40, 41, 172	syl2anc 661	. . . . . 6 |- ( ph -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
174	40	sqcld 11998	. . . . . . . . . 10 |- ( ph -> ( X ^ 2 ) e. CC )
175	10, 174, 41	mul12d 9570	. . . . . . . . 9 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
176	2, 10, 12	divcan2d 10101	. . . . . . . . . 10 |- ( ph -> ( 3 x. ( B / 3 ) ) = B )
177	176	oveq2d 6102	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
178	174, 2	mulcomd 9399	. . . . . . . . 9 |- ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
179	175, 177, 178	3eqtrd 2474	. . . . . . . 8 |- ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
180	179	oveq2d 6102	. . . . . . 7 |- ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
181	180	oveq1d 6101	. . . . . 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 2470	. . . . 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 6101	. . . 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 11875	. . . . . . 7 |- ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
185	40, 17, 184	sylancl 662	. . . . . 6 |- ( ph -> ( X ^ 3 ) e. CC )
186	2, 174	mulcld 9398	. . . . . 6 |- ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
187	185, 186	addcld 9397	. . . . 5 |- ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
188	41	sqcld 11998	. . . . . . . 8 |- ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
189	40, 188	mulcld 9398	. . . . . . 7 |- ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
190	10, 189	mulcld 9398	. . . . . 6 |- ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
191		expcl 11875	. . . . . . 7 |- ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
192	41, 17, 191	sylancl 662	. . . . . 6 |- ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
193	190, 192	addcld 9397	. . . . 5 |- ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
194	14, 42	mulcld 9398	. . . . . 6 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
195	194, 39	addcld 9397	. . . . 5 |- ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
196	187, 193, 195	addassd 9400	. . . 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 9402	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
198	197	oveq1d 6101	. . . . . . . . 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 9398	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
200	14, 41	mulcld 9398	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
201	199, 200, 39	addassd 9400	. . . . . . . . 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 6101	. . . . . . . . . . . . . . 15 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
203	3, 7, 10, 12	divsubdird 10138	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
204	5, 10, 12	divcan3d 10104	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 3 x. C ) / 3 ) = C )
205	204	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
206	202, 203, 205	3eqtrd 2474	. . . . . . . . . . . . . 14 |- ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
207	206	negeqd 9596	. . . . . . . . . . . . 13 |- ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
208	3, 10, 12	divcld 10099	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
209	208, 5	negsubdi2d 9727	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
210	207, 209	eqtrd 2470	. . . . . . . . . . . 12 |- ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
211	210	oveq1d 6101	. . . . . . . . . . 11 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
212	5, 208, 40	subdird 9793	. . . . . . . . . . 11 |- ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
213	208, 40	mulcomd 9399	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
214	4	sqvali 11937	. . . . . . . . . . . . . . . . . 18 |- ( 3 ^ 2 ) = ( 3 x. 3 )
215	214	oveq2i 6097	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
216	2, 10, 12	sqdivd 12013	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
217	3, 10, 10, 12, 12	divdiv1d 10130	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
218	215, 216, 217	3eqtr4a 2496	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
219	218	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
220	208, 10, 12	divcan2d 10101	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
221	219, 220	eqtrd 2470	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
222	221	oveq2d 6102	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
223	40, 10, 188	mul12d 9570	. . . . . . . . . . . . 13 |- ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
224	213, 222, 223	3eqtr2d 2476	. . . . . . . . . . . 12 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
225	224	oveq2d 6102	. . . . . . . . . . 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 2474	. . . . . . . . . 10 |- ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
227	210	oveq1d 6101	. . . . . . . . . . . . 13 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
228	5, 208, 41	subdird 9793	. . . . . . . . . . . . 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 10134	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
230	5, 2	mulcomd 9399	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C x. B ) = ( B x. C ) )
231	230	oveq1d 6101	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
232	229, 231	eqtr3d 2472	. . . . . . . . . . . . . 14 |- ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
233	3, 10, 2, 10, 12, 12	divmuldivd 10140	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
234		df-3 10373	. . . . . . . . . . . . . . . . . 18 |- 3 = ( 2 + 1 )
235	234	oveq2i 6097	. . . . . . . . . . . . . . . . 17 |- ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
236		expp1 11864	. . . . . . . . . . . . . . . . . 18 |- ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
237	2, 27, 236	sylancl 662	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
238	235, 237	syl5req 2483	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
239	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 x. 3 ) = 9 )
240	238, 239	oveq12d 6104	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
241	233, 240	eqtrd 2470	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
242	232, 241	oveq12d 6104	. . . . . . . . . . . . 13 |- ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
243	227, 228, 242	3eqtrd 2474	. . . . . . . . . . . 12 |- ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
244	15	oveq1d 6101	. . . . . . . . . . . . 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 10137	. . . . . . . . . . . . 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 10138	. . . . . . . . . . . . . . 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 10843	. . . . . . . . . . . . . . . . . 18 |- ( 9 x. 3 ) = ; 2 7
248	247	oveq2i 6097	. . . . . . . . . . . . . . . . 17 |- ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
249	23, 10, 104, 12, 107	divcan5d 10125	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
250	248, 249	syl5eqr 2484	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
251	250	oveq2d 6102	. . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . . 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 10104	. . . . . . . . . . . . . 14 |- ( ph -> ( (; 2 7 x. D ) / ; 2 7 ) = D )
254	252, 253	oveq12d 6104	. . . . . . . . . . . . 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 2474	. . . . . . . . . . . 12 |- ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
256	243, 255	oveq12d 6104	. . . . . . . . . . 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 10099	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
258	21, 36, 38	divcld 10099	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
259	257, 258	negsubdi2d 9727	. . . . . . . . . . . . . 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 12014	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
261	63	oveq2i 6097	. . . . . . . . . . . . . . . . 17 |- ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
262		ax-1cn 9332	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
263	4, 16, 262, 53	subaddrii 9689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 3 - 2 ) = 1
264	263	oveq1i 6096	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
265	19	mulid2d 9396	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
266	264, 265	syl5eq 2482	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
267	10, 68, 19	subdird 9793	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
268	266, 267	eqtr3d 2472	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
269	268	oveq1d 6101	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
270		mulcl 9358	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
271	4, 19, 270	sylancr 663	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
272	271, 21, 36, 38	divsubdird 10138	. . . . . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274	261, 273	syl5eq 2482	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275	22, 4, 247	mulcomli 9385	. . . . . . . . . . . . . . . . . . 19 |- ( 3 x. 9 ) = ; 2 7
276	275	oveq2i 6097	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
277	19, 104, 10, 107, 12	divcan5d 10125	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
278	276, 277	syl5eqr 2484	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
279	278	oveq1d 6101	. . . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
281	280	negeqd 9596	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
282	23, 10, 12	divcld 10099	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( B x. C ) / 3 ) e. CC )
283	282, 257, 258	npncan3d 9747	. . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . 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 6101	. . . . . . . . . . . 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 9698	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
287	286, 31	addcomd 9563	. . . . . . . . . . . 12 |- ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
288	243, 200	eqeltrrd 2513	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
289	258, 282	subcld 9711	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
290	288, 289, 31	addassd 9400	. . . . . . . . . . . 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 2478	. . . . . . . . . . 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 9717	. . . . . . . . . . 11 |- ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
293	256, 291, 292	3eqtr2d 2476	. . . . . . . . . 10 |- ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
294	226, 293	oveq12d 6104	. . . . . . . . 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 2474	. . . . . . . 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 9398	. . . . . . . . 9 |- ( ph -> ( C x. X ) e. CC )
297	296, 31, 190, 192	addsub4d 9758	. . . . . . . 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 2473	. . . . . . 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 6102	. . . . . 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 9397	. . . . . . 7 |- ( ph -> ( ( C x. X ) + D ) e. CC )
301	193, 300	pncan3d 9714	. . . . . 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 2470	. . . . 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 6102	. . . 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 2474	. . 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 2446	. 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 6093	. . . . . . . 8 |- ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
307		0exp 11891	. . . . . . . . 9 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
308	46, 307	ax-mp 5	. . . . . . . 8 |- ( 0 ^ 3 ) = 0
309	306, 308	syl6eq 2486	. . . . . . 7 |- ( r = 0 -> ( r ^ 3 ) = 0 )
310		0ne1 10381	. . . . . . . 8 |- 0 =/= 1
311	310	a1i 11	. . . . . . 7 |- ( r = 0 -> 0 =/= 1 )
312	309, 311	eqnetrd 2621	. . . . . 6 |- ( r = 0 -> ( r ^ 3 ) =/= 1 )
313	312	necon2i 2653	. . . . 5 |- ( ( r ^ 3 ) = 1 -> r =/= 0 )
314		eqcom 2440	. . . . . . . 8 |- ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X )
315	2	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
316		simprl 755	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
317	43	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
318	316, 317	mulcld 9398	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
319	9	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
320		simprr 756	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
321	168	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
322	316, 317, 320, 321	mulne0d 9980	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
323	319, 318, 322	divcld 10099	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
324	318, 323	addcld 9397	. . . . . . . . . . . . 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 10137	. . . . . . . . . . . 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 9400	. . . . . . . . . . . . 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 6101	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) / 3 ) )
330	41	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
331	324, 325, 326	divcld 10099	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
332	330, 331	subnegd 9718	. . . . . . . . . . . 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 2480	. . . . . . . . . . 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 9596	. . . . . . . . . 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 9698	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
336	330, 335	negsubdi2d 9727	. . . . . . . . . 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 2470	. . . . . . . . 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 2446	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
339	314, 338	syl5bb 257	. . . . . . 7 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
340	40	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
341	335, 330, 340	subadd2d 9730	. . . . . . 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 10137	. . . . . . . . . 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 9596	. . . . . . . . 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 10099	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
345	323, 325, 326	divcld 10099	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
346	344, 345	negdi2d 9725	. . . . . . . . 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 10134	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
348	347	negeqd 9596	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
349	44	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
350	316, 349	mulneg2d 9790	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
351	348, 350	eqtr4d 2473	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
352	319, 318, 325, 322, 326	divdiv32d 10124	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
353	13	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
354	353, 318, 325, 322, 326	divcan7d 10127	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
355	163	oveq1d 6101	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
356	355	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
357	352, 354, 356	3eqtr2d 2476	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
358	127	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
359	318, 325, 322, 326	divne0d 10115	. . . . . . . . . . . 12 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
360	358, 344, 359	div2negd 10114	. . . . . . . . . . 11 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
361	351	oveq2d 6102	. . . . . . . . . . 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 2476	. . . . . . . . . 10 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
363	351, 362	oveq12d 6104	. . . . . . . . 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 2474	. . . . . . . 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 2449	. . . . . . 7 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) )
366	339, 341, 365	3bitrrd 280	. . . . . 6 |- ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
367	366	anassrs 648	. . . . 5 |- ( ( ( ph /\ r e. CC ) /\ r =/= 0 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
368	313, 367	sylan2 474	. . . 4 |- ( ( ( ph /\ r e. CC ) /\ ( r ^ 3 ) = 1 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
369	368	pm5.32da 641	. . 3 |- ( ( ph /\ r e. CC ) -> ( ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) <-> ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
370	369	rexbidva 2727	. 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 1369   e. wcel 1756   =/= wne 2601   E.wrex 2711   class class class wbr 4287  (class class class)co 6086   CCcc 9272   0cc0 9274   1c1 9275   + caddc 9277   x. cmul 9279   - cmin 9587   -ucneg 9588   / cdiv 9985   NNcn 10314   2c2 10363   3c3 10364   4c4 10365   7c7 10368   9c9 10370   NN0cn0 10571  ;cdc 10747   ^cexp 11857   || cdivides 13527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-sup 7683  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-rp 10984  df-fz 11430  df-seq 11799  df-exp 11858  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-dvds 13528

This theorem is referenced by:  cubic2  22218  quart  22231