Theorem dcubic2 24571

Description: Reverse direction of dcubic 24573. Given a solution U to the "substitution" quadratic equation X = U - M / U, show that X is in the desired form. (Contributed by Mario Carneiro, 25-Apr-2015.)

Hypotheses

Ref	Expression
dcubic.c	|- ( ph -> P e. CC )
dcubic.d	|- ( ph -> Q e. CC )
dcubic.x	|- ( ph -> X e. CC )
dcubic.t	|- ( ph -> T e. CC )
dcubic.3	|- ( ph -> ( T ^ 3 ) = ( G - N ) )
dcubic.g	|- ( ph -> G e. CC )
dcubic.2	|- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
dcubic.m	|- ( ph -> M = ( P / 3 ) )
dcubic.n	|- ( ph -> N = ( Q / 2 ) )
dcubic.0	|- ( ph -> T =/= 0 )
dcubic2.u	|- ( ph -> U e. CC )
dcubic2.z	|- ( ph -> U =/= 0 )
dcubic2.2	|- ( ph -> X = ( U - ( M / U ) ) )
dcubic2.x	|- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )

Assertion

Ref	Expression
dcubic2	|- ( ph -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )

Distinct variable groups:   M, r   P, r   ph, r   Q, r   T, r   U, r   X, r

Allowed substitution hints:   G( r)   N( r)

Proof of Theorem dcubic2

Step	Hyp	Ref	Expression
1		dcubic2.u	. . . . 5 |- ( ph -> U e. CC )
2		dcubic.t	. . . . 5 |- ( ph -> T e. CC )
3		dcubic.0	. . . . 5 |- ( ph -> T =/= 0 )
4	1, 2, 3	divcld 10801	. . . 4 |- ( ph -> ( U / T ) e. CC )
5	4	adantr 481	. . 3 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( U / T ) e. CC )
6		3nn0 11310	. . . . . . 7 |- 3 e. NN0
7	6	a1i 11	. . . . . 6 |- ( ph -> 3 e. NN0 )
8	1, 2, 3, 7	expdivd 13022	. . . . 5 |- ( ph -> ( ( U / T ) ^ 3 ) = ( ( U ^ 3 ) / ( T ^ 3 ) ) )
9	8	adantr 481	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U / T ) ^ 3 ) = ( ( U ^ 3 ) / ( T ^ 3 ) ) )
10		oveq1 6657	. . . . 5 |- ( ( U ^ 3 ) = ( G - N ) -> ( ( U ^ 3 ) / ( T ^ 3 ) ) = ( ( G - N ) / ( T ^ 3 ) ) )
11		dcubic.3	. . . . . . 7 |- ( ph -> ( T ^ 3 ) = ( G - N ) )
12	11	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( T ^ 3 ) ) = ( ( G - N ) / ( T ^ 3 ) ) )
13		expcl 12878	. . . . . . . 8 |- ( ( T e. CC /\ 3 e. NN0 ) -> ( T ^ 3 ) e. CC )
14	2, 6, 13	sylancl 694	. . . . . . 7 |- ( ph -> ( T ^ 3 ) e. CC )
15		3z 11410	. . . . . . . . 9 |- 3 e. ZZ
16	15	a1i 11	. . . . . . . 8 |- ( ph -> 3 e. ZZ )
17	2, 3, 16	expne0d 13014	. . . . . . 7 |- ( ph -> ( T ^ 3 ) =/= 0 )
18	14, 17	dividd 10799	. . . . . 6 |- ( ph -> ( ( T ^ 3 ) / ( T ^ 3 ) ) = 1 )
19	12, 18	eqtr3d 2658	. . . . 5 |- ( ph -> ( ( G - N ) / ( T ^ 3 ) ) = 1 )
20	10, 19	sylan9eqr 2678	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U ^ 3 ) / ( T ^ 3 ) ) = 1 )
21	9, 20	eqtrd 2656	. . 3 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U / T ) ^ 3 ) = 1 )
22		dcubic2.2	. . . . 5 |- ( ph -> X = ( U - ( M / U ) ) )
23	1, 2, 3	divcan1d 10802	. . . . . 6 |- ( ph -> ( ( U / T ) x. T ) = U )
24	23	oveq2d 6666	. . . . . 6 |- ( ph -> ( M / ( ( U / T ) x. T ) ) = ( M / U ) )
25	23, 24	oveq12d 6668	. . . . 5 |- ( ph -> ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) = ( U - ( M / U ) ) )
26	22, 25	eqtr4d 2659	. . . 4 |- ( ph -> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
27	26	adantr 481	. . 3 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
28		oveq1 6657	. . . . . 6 |- ( r = ( U / T ) -> ( r ^ 3 ) = ( ( U / T ) ^ 3 ) )
29	28	eqeq1d 2624	. . . . 5 |- ( r = ( U / T ) -> ( ( r ^ 3 ) = 1 <-> ( ( U / T ) ^ 3 ) = 1 ) )
30		oveq1 6657	. . . . . . 7 |- ( r = ( U / T ) -> ( r x. T ) = ( ( U / T ) x. T ) )
31	30	oveq2d 6666	. . . . . . 7 |- ( r = ( U / T ) -> ( M / ( r x. T ) ) = ( M / ( ( U / T ) x. T ) ) )
32	30, 31	oveq12d 6668	. . . . . 6 |- ( r = ( U / T ) -> ( ( r x. T ) - ( M / ( r x. T ) ) ) = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
33	32	eqeq2d 2632	. . . . 5 |- ( r = ( U / T ) -> ( X = ( ( r x. T ) - ( M / ( r x. T ) ) ) <-> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) )
34	29, 33	anbi12d 747	. . . 4 |- ( r = ( U / T ) -> ( ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) <-> ( ( ( U / T ) ^ 3 ) = 1 /\ X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) ) )
35	34	rspcev 3309	. . 3 |- ( ( ( U / T ) e. CC /\ ( ( ( U / T ) ^ 3 ) = 1 /\ X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
36	5, 21, 27, 35	syl12anc 1324	. 2 |- ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
37		dcubic.m	. . . . . . . 8 |- ( ph -> M = ( P / 3 ) )
38		dcubic.c	. . . . . . . . 9 |- ( ph -> P e. CC )
39		3cn 11095	. . . . . . . . . 10 |- 3 e. CC
40	39	a1i 11	. . . . . . . . 9 |- ( ph -> 3 e. CC )
41		3ne0 11115	. . . . . . . . . 10 |- 3 =/= 0
42	41	a1i 11	. . . . . . . . 9 |- ( ph -> 3 =/= 0 )
43	38, 40, 42	divcld 10801	. . . . . . . 8 |- ( ph -> ( P / 3 ) e. CC )
44	37, 43	eqeltrd 2701	. . . . . . 7 |- ( ph -> M e. CC )
45		dcubic2.z	. . . . . . 7 |- ( ph -> U =/= 0 )
46	44, 1, 45	divcld 10801	. . . . . 6 |- ( ph -> ( M / U ) e. CC )
47	46	negcld 10379	. . . . 5 |- ( ph -> -u ( M / U ) e. CC )
48	47, 2, 3	divcld 10801	. . . 4 |- ( ph -> ( -u ( M / U ) / T ) e. CC )
49	48	adantr 481	. . 3 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( M / U ) / T ) e. CC )
50	47, 2, 3, 7	expdivd 13022	. . . . . 6 |- ( ph -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( ( -u ( M / U ) ^ 3 ) / ( T ^ 3 ) ) )
51	44, 1, 45	divnegd 10814	. . . . . . . . 9 |- ( ph -> -u ( M / U ) = ( -u M / U ) )
52	51	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( -u ( M / U ) ^ 3 ) = ( ( -u M / U ) ^ 3 ) )
53	44	negcld 10379	. . . . . . . . 9 |- ( ph -> -u M e. CC )
54	53, 1, 45, 7	expdivd 13022	. . . . . . . 8 |- ( ph -> ( ( -u M / U ) ^ 3 ) = ( ( -u M ^ 3 ) / ( U ^ 3 ) ) )
55	11	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( ( G + N ) x. ( G - N ) ) )
56		dcubic.g	. . . . . . . . . . . . . . 15 |- ( ph -> G e. CC )
57		dcubic.n	. . . . . . . . . . . . . . . 16 |- ( ph -> N = ( Q / 2 ) )
58		dcubic.d	. . . . . . . . . . . . . . . . 17 |- ( ph -> Q e. CC )
59	58	halfcld 11277	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q / 2 ) e. CC )
60	57, 59	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
61		subsq 12972	. . . . . . . . . . . . . . 15 |- ( ( G e. CC /\ N e. CC ) -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( G + N ) x. ( G - N ) ) )
62	56, 60, 61	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( G + N ) x. ( G - N ) ) )
63	55, 62	eqtr4d 2659	. . . . . . . . . . . . 13 |- ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( ( G ^ 2 ) - ( N ^ 2 ) ) )
64		dcubic.2	. . . . . . . . . . . . . 14 |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
65	64	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ph -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( N ^ 2 ) ) )
66	60	sqcld 13006	. . . . . . . . . . . . . 14 |- ( ph -> ( N ^ 2 ) e. CC )
67		expcl 12878	. . . . . . . . . . . . . . 15 |- ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
68	44, 6, 67	sylancl 694	. . . . . . . . . . . . . 14 |- ( ph -> ( M ^ 3 ) e. CC )
69	66, 68	pncan2d 10394	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( N ^ 2 ) ) = ( M ^ 3 ) )
70	63, 65, 69	3eqtrd 2660	. . . . . . . . . . . 12 |- ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( M ^ 3 ) )
71	70	negeqd 10275	. . . . . . . . . . 11 |- ( ph -> -u ( ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
72	56, 60	addcld 10059	. . . . . . . . . . . 12 |- ( ph -> ( G + N ) e. CC )
73	72, 14	mulneg1d 10483	. . . . . . . . . . 11 |- ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( ( G + N ) x. ( T ^ 3 ) ) )
74		3nn 11186	. . . . . . . . . . . . 13 |- 3 e. NN
75	74	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 3 e. NN )
76		2nn 11185	. . . . . . . . . . . . . 14 |- 2 e. NN
77		1nn0 11308	. . . . . . . . . . . . . 14 |- 1 e. NN0
78		1nn 11031	. . . . . . . . . . . . . 14 |- 1 e. NN
79		2t1e2 11176	. . . . . . . . . . . . . . . 16 |- ( 2 x. 1 ) = 2
80	79	oveq1i 6660	. . . . . . . . . . . . . . 15 |- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
81		2p1e3 11151	. . . . . . . . . . . . . . 15 |- ( 2 + 1 ) = 3
82	80, 81	eqtri 2644	. . . . . . . . . . . . . 14 |- ( ( 2 x. 1 ) + 1 ) = 3
83		1lt2 11194	. . . . . . . . . . . . . 14 |- 1 < 2
84	76, 77, 78, 82, 83	ndvdsi 15136	. . . . . . . . . . . . 13 |- -. 2 || 3
85	84	a1i 11	. . . . . . . . . . . 12 |- ( ph -> -. 2 || 3 )
86		oexpneg 15069	. . . . . . . . . . . 12 |- ( ( M e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u M ^ 3 ) = -u ( M ^ 3 ) )
87	44, 75, 85, 86	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( -u M ^ 3 ) = -u ( M ^ 3 ) )
88	71, 73, 87	3eqtr4d 2666	. . . . . . . . . 10 |- ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = ( -u M ^ 3 ) )
89	88	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( -u ( G + N ) x. ( T ^ 3 ) ) / ( U ^ 3 ) ) = ( ( -u M ^ 3 ) / ( U ^ 3 ) ) )
90	72	negcld 10379	. . . . . . . . . 10 |- ( ph -> -u ( G + N ) e. CC )
91		expcl 12878	. . . . . . . . . . 11 |- ( ( U e. CC /\ 3 e. NN0 ) -> ( U ^ 3 ) e. CC )
92	1, 6, 91	sylancl 694	. . . . . . . . . 10 |- ( ph -> ( U ^ 3 ) e. CC )
93	1, 45, 16	expne0d 13014	. . . . . . . . . 10 |- ( ph -> ( U ^ 3 ) =/= 0 )
94	90, 14, 92, 93	div23d 10838	. . . . . . . . 9 |- ( ph -> ( ( -u ( G + N ) x. ( T ^ 3 ) ) / ( U ^ 3 ) ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
95	89, 94	eqtr3d 2658	. . . . . . . 8 |- ( ph -> ( ( -u M ^ 3 ) / ( U ^ 3 ) ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
96	52, 54, 95	3eqtrd 2660	. . . . . . 7 |- ( ph -> ( -u ( M / U ) ^ 3 ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
97	96	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( -u ( M / U ) ^ 3 ) / ( T ^ 3 ) ) = ( ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) / ( T ^ 3 ) ) )
98	90, 92, 93	divcld 10801	. . . . . . 7 |- ( ph -> ( -u ( G + N ) / ( U ^ 3 ) ) e. CC )
99	98, 14, 17	divcan4d 10807	. . . . . 6 |- ( ph -> ( ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) / ( T ^ 3 ) ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
100	50, 97, 99	3eqtrd 2660	. . . . 5 |- ( ph -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
101	100	adantr 481	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
102		oveq1 6657	. . . . . 6 |- ( ( U ^ 3 ) = -u ( G + N ) -> ( ( U ^ 3 ) / ( U ^ 3 ) ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
103	102	eqcomd 2628	. . . . 5 |- ( ( U ^ 3 ) = -u ( G + N ) -> ( -u ( G + N ) / ( U ^ 3 ) ) = ( ( U ^ 3 ) / ( U ^ 3 ) ) )
104	92, 93	dividd 10799	. . . . 5 |- ( ph -> ( ( U ^ 3 ) / ( U ^ 3 ) ) = 1 )
105	103, 104	sylan9eqr 2678	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) / ( U ^ 3 ) ) = 1 )
106	101, 105	eqtrd 2656	. . 3 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) ^ 3 ) = 1 )
107	46, 1	neg2subd 10409	. . . . . 6 |- ( ph -> ( -u ( M / U ) - -u U ) = ( U - ( M / U ) ) )
108	22, 107	eqtr4d 2659	. . . . 5 |- ( ph -> X = ( -u ( M / U ) - -u U ) )
109	108	adantr 481	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> X = ( -u ( M / U ) - -u U ) )
110	47, 2, 3	divcan1d 10802	. . . . . 6 |- ( ph -> ( ( -u ( M / U ) / T ) x. T ) = -u ( M / U ) )
111	110	adantr 481	. . . . 5 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) x. T ) = -u ( M / U ) )
112	44, 1, 45	divneg2d 10815	. . . . . . . . 9 |- ( ph -> -u ( M / U ) = ( M / -u U ) )
113	110, 112	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( ( -u ( M / U ) / T ) x. T ) = ( M / -u U ) )
114	113	adantr 481	. . . . . . 7 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) x. T ) = ( M / -u U ) )
115	114	oveq2d 6666	. . . . . 6 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( ( -u ( M / U ) / T ) x. T ) ) = ( M / ( M / -u U ) ) )
116	44	adantr 481	. . . . . . 7 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> M e. CC )
117	1	negcld 10379	. . . . . . . 8 |- ( ph -> -u U e. CC )
118	117	adantr 481	. . . . . . 7 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u U e. CC )
119	73, 71	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
120	119	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
121	90	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( G + N ) e. CC )
122	14	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( T ^ 3 ) e. CC )
123		simpr 477	. . . . . . . . . . 11 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( U ^ 3 ) = -u ( G + N ) )
124	93	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( U ^ 3 ) =/= 0 )
125	123, 124	eqnetrrd 2862	. . . . . . . . . 10 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( G + N ) =/= 0 )
126	17	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( T ^ 3 ) =/= 0 )
127	121, 122, 125, 126	mulne0d 10679	. . . . . . . . 9 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) x. ( T ^ 3 ) ) =/= 0 )
128	120, 127	eqnetrrd 2862	. . . . . . . 8 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( M ^ 3 ) =/= 0 )
129		oveq1 6657	. . . . . . . . . . . 12 |- ( M = 0 -> ( M ^ 3 ) = ( 0 ^ 3 ) )
130		0exp 12895	. . . . . . . . . . . . 13 |- ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
131	74, 130	ax-mp 5	. . . . . . . . . . . 12 |- ( 0 ^ 3 ) = 0
132	129, 131	syl6eq 2672	. . . . . . . . . . 11 |- ( M = 0 -> ( M ^ 3 ) = 0 )
133	132	negeqd 10275	. . . . . . . . . 10 |- ( M = 0 -> -u ( M ^ 3 ) = -u 0 )
134		neg0 10327	. . . . . . . . . 10 |- -u 0 = 0
135	133, 134	syl6eq 2672	. . . . . . . . 9 |- ( M = 0 -> -u ( M ^ 3 ) = 0 )
136	135	necon3i 2826	. . . . . . . 8 |- ( -u ( M ^ 3 ) =/= 0 -> M =/= 0 )
137	128, 136	syl 17	. . . . . . 7 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> M =/= 0 )
138	1, 45	negne0d 10390	. . . . . . . 8 |- ( ph -> -u U =/= 0 )
139	138	adantr 481	. . . . . . 7 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u U =/= 0 )
140	116, 118, 137, 139	ddcand 10821	. . . . . 6 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( M / -u U ) ) = -u U )
141	115, 140	eqtrd 2656	. . . . 5 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( ( -u ( M / U ) / T ) x. T ) ) = -u U )
142	111, 141	oveq12d 6668	. . . 4 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) = ( -u ( M / U ) - -u U ) )
143	109, 142	eqtr4d 2659	. . 3 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) )
144		oveq1 6657	. . . . . 6 |- ( r = ( -u ( M / U ) / T ) -> ( r ^ 3 ) = ( ( -u ( M / U ) / T ) ^ 3 ) )
145	144	eqeq1d 2624	. . . . 5 |- ( r = ( -u ( M / U ) / T ) -> ( ( r ^ 3 ) = 1 <-> ( ( -u ( M / U ) / T ) ^ 3 ) = 1 ) )
146		oveq1 6657	. . . . . . 7 |- ( r = ( -u ( M / U ) / T ) -> ( r x. T ) = ( ( -u ( M / U ) / T ) x. T ) )
147	146	oveq2d 6666	. . . . . . 7 |- ( r = ( -u ( M / U ) / T ) -> ( M / ( r x. T ) ) = ( M / ( ( -u ( M / U ) / T ) x. T ) ) )
148	146, 147	oveq12d 6668	. . . . . 6 |- ( r = ( -u ( M / U ) / T ) -> ( ( r x. T ) - ( M / ( r x. T ) ) ) = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) )
149	148	eqeq2d 2632	. . . . 5 |- ( r = ( -u ( M / U ) / T ) -> ( X = ( ( r x. T ) - ( M / ( r x. T ) ) ) <-> X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) )
150	145, 149	anbi12d 747	. . . 4 |- ( r = ( -u ( M / U ) / T ) -> ( ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) <-> ( ( ( -u ( M / U ) / T ) ^ 3 ) = 1 /\ X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) ) )
151	150	rspcev 3309	. . 3 |- ( ( ( -u ( M / U ) / T ) e. CC /\ ( ( ( -u ( M / U ) / T ) ^ 3 ) = 1 /\ X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
152	49, 106, 143, 151	syl12anc 1324	. 2 |- ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
153	92	sqcld 13006	. . . . . . 7 |- ( ph -> ( ( U ^ 3 ) ^ 2 ) e. CC )
154	153	mulid2d 10058	. . . . . 6 |- ( ph -> ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) = ( ( U ^ 3 ) ^ 2 ) )
155	58, 92	mulcld 10060	. . . . . . 7 |- ( ph -> ( Q x. ( U ^ 3 ) ) e. CC )
156	155, 68	negsubd 10398	. . . . . 6 |- ( ph -> ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) = ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) )
157	154, 156	oveq12d 6668	. . . . 5 |- ( ph -> ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) )
158		dcubic2.x	. . . . . 6 |- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
159		dcubic.x	. . . . . . 7 |- ( ph -> X e. CC )
160	38, 58, 159, 2, 11, 56, 64, 37, 57, 3, 1, 45, 22	dcubic1lem 24570	. . . . . 6 |- ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )
161	158, 160	mpbid 222	. . . . 5 |- ( ph -> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 )
162	157, 161	eqtrd 2656	. . . 4 |- ( ph -> ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = 0 )
163		1cnd 10056	. . . . 5 |- ( ph -> 1 e. CC )
164		ax-1ne0 10005	. . . . . 6 |- 1 =/= 0
165	164	a1i 11	. . . . 5 |- ( ph -> 1 =/= 0 )
166	68	negcld 10379	. . . . 5 |- ( ph -> -u ( M ^ 3 ) e. CC )
167		2cn 11091	. . . . . 6 |- 2 e. CC
168		mulcl 10020	. . . . . 6 |- ( ( 2 e. CC /\ G e. CC ) -> ( 2 x. G ) e. CC )
169	167, 56, 168	sylancr 695	. . . . 5 |- ( ph -> ( 2 x. G ) e. CC )
170		sqmul 12926	. . . . . . 7 |- ( ( 2 e. CC /\ G e. CC ) -> ( ( 2 x. G ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) )
171	167, 56, 170	sylancr 695	. . . . . 6 |- ( ph -> ( ( 2 x. G ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) )
172	64	oveq2d 6666	. . . . . 6 |- ( ph -> ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) = ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) )
173	167	sqcli 12944	. . . . . . . . 9 |- ( 2 ^ 2 ) e. CC
174		mulcl 10020	. . . . . . . . 9 |- ( ( ( 2 ^ 2 ) e. CC /\ ( N ^ 2 ) e. CC ) -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) e. CC )
175	173, 66, 174	sylancr 695	. . . . . . . 8 |- ( ph -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) e. CC )
176		mulcl 10020	. . . . . . . . 9 |- ( ( ( 2 ^ 2 ) e. CC /\ ( M ^ 3 ) e. CC ) -> ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) e. CC )
177	173, 68, 176	sylancr 695	. . . . . . . 8 |- ( ph -> ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) e. CC )
178	175, 177	subnegd 10399	. . . . . . 7 |- ( ph -> ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) - -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) + ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
179	57	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( 2 x. N ) = ( 2 x. ( Q / 2 ) ) )
180	167	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 2 e. CC )
181		2ne0 11113	. . . . . . . . . . . . 13 |- 2 =/= 0
182	181	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 2 =/= 0 )
183	58, 180, 182	divcan2d 10803	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( Q / 2 ) ) = Q )
184	179, 183	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) = Q )
185	184	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) ^ 2 ) = ( Q ^ 2 ) )
186		sqmul 12926	. . . . . . . . . 10 |- ( ( 2 e. CC /\ N e. CC ) -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
187	167, 60, 186	sylancr 695	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
188	185, 187	eqtr3d 2658	. . . . . . . 8 |- ( ph -> ( Q ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
189	166	mulid2d 10058	. . . . . . . . . . 11 |- ( ph -> ( 1 x. -u ( M ^ 3 ) ) = -u ( M ^ 3 ) )
190	189	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = ( 4 x. -u ( M ^ 3 ) ) )
191		4cn 11098	. . . . . . . . . . 11 |- 4 e. CC
192		mulneg2 10467	. . . . . . . . . . 11 |- ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. -u ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) ) )
193	191, 68, 192	sylancr 695	. . . . . . . . . 10 |- ( ph -> ( 4 x. -u ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) ) )
194	190, 193	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = -u ( 4 x. ( M ^ 3 ) ) )
195		sq2 12960	. . . . . . . . . . 11 |- ( 2 ^ 2 ) = 4
196	195	oveq1i 6660	. . . . . . . . . 10 |- ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) = ( 4 x. ( M ^ 3 ) )
197	196	negeqi 10274	. . . . . . . . 9 |- -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) )
198	194, 197	syl6eqr 2674	. . . . . . . 8 |- ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) )
199	188, 198	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) - -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
200	173	a1i 11	. . . . . . . 8 |- ( ph -> ( 2 ^ 2 ) e. CC )
201	200, 66, 68	adddid 10064	. . . . . . 7 |- ( ph -> ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) + ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
202	178, 199, 201	3eqtr4rd 2667	. . . . . 6 |- ( ph -> ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) = ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) )
203	171, 172, 202	3eqtrd 2660	. . . . 5 |- ( ph -> ( ( 2 x. G ) ^ 2 ) = ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) )
204	163, 165, 58, 166, 92, 169, 203	quad2 24566	. . . 4 |- ( ph -> ( ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = 0 <-> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) ) )
205	162, 204	mpbid 222	. . 3 |- ( ph -> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) )
206	79	oveq2i 6661	. . . . . 6 |- ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( ( -u Q + ( 2 x. G ) ) / 2 )
207	58	negcld 10379	. . . . . . . 8 |- ( ph -> -u Q e. CC )
208	207, 169, 180, 182	divdird 10839	. . . . . . 7 |- ( ph -> ( ( -u Q + ( 2 x. G ) ) / 2 ) = ( ( -u Q / 2 ) + ( ( 2 x. G ) / 2 ) ) )
209	57	negeqd 10275	. . . . . . . . 9 |- ( ph -> -u N = -u ( Q / 2 ) )
210	58, 180, 182	divnegd 10814	. . . . . . . . 9 |- ( ph -> -u ( Q / 2 ) = ( -u Q / 2 ) )
211	209, 210	eqtr2d 2657	. . . . . . . 8 |- ( ph -> ( -u Q / 2 ) = -u N )
212	56, 180, 182	divcan3d 10806	. . . . . . . 8 |- ( ph -> ( ( 2 x. G ) / 2 ) = G )
213	211, 212	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( -u Q / 2 ) + ( ( 2 x. G ) / 2 ) ) = ( -u N + G ) )
214	60	negcld 10379	. . . . . . . . 9 |- ( ph -> -u N e. CC )
215	214, 56	addcomd 10238	. . . . . . . 8 |- ( ph -> ( -u N + G ) = ( G + -u N ) )
216	56, 60	negsubd 10398	. . . . . . . 8 |- ( ph -> ( G + -u N ) = ( G - N ) )
217	215, 216	eqtrd 2656	. . . . . . 7 |- ( ph -> ( -u N + G ) = ( G - N ) )
218	208, 213, 217	3eqtrd 2660	. . . . . 6 |- ( ph -> ( ( -u Q + ( 2 x. G ) ) / 2 ) = ( G - N ) )
219	206, 218	syl5eq 2668	. . . . 5 |- ( ph -> ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( G - N ) )
220	219	eqeq2d 2632	. . . 4 |- ( ph -> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) <-> ( U ^ 3 ) = ( G - N ) ) )
221	79	oveq2i 6661	. . . . . 6 |- ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( ( -u Q - ( 2 x. G ) ) / 2 )
222	211, 212	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( -u Q / 2 ) - ( ( 2 x. G ) / 2 ) ) = ( -u N - G ) )
223	207, 169, 180, 182	divsubdird 10840	. . . . . . 7 |- ( ph -> ( ( -u Q - ( 2 x. G ) ) / 2 ) = ( ( -u Q / 2 ) - ( ( 2 x. G ) / 2 ) ) )
224	56, 60	addcomd 10238	. . . . . . . . 9 |- ( ph -> ( G + N ) = ( N + G ) )
225	224	negeqd 10275	. . . . . . . 8 |- ( ph -> -u ( G + N ) = -u ( N + G ) )
226	60, 56	negdi2d 10406	. . . . . . . 8 |- ( ph -> -u ( N + G ) = ( -u N - G ) )
227	225, 226	eqtrd 2656	. . . . . . 7 |- ( ph -> -u ( G + N ) = ( -u N - G ) )
228	222, 223, 227	3eqtr4d 2666	. . . . . 6 |- ( ph -> ( ( -u Q - ( 2 x. G ) ) / 2 ) = -u ( G + N ) )
229	221, 228	syl5eq 2668	. . . . 5 |- ( ph -> ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) = -u ( G + N ) )
230	229	eqeq2d 2632	. . . 4 |- ( ph -> ( ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) <-> ( U ^ 3 ) = -u ( G + N ) ) )
231	220, 230	orbi12d 746	. . 3 |- ( ph -> ( ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) <-> ( ( U ^ 3 ) = ( G - N ) \/ ( U ^ 3 ) = -u ( G + N ) ) ) )
232	205, 231	mpbid 222	. 2 |- ( ph -> ( ( U ^ 3 ) = ( G - N ) \/ ( U ^ 3 ) = -u ( G + N ) ) )
233	36, 152, 232	mpjaodan 827	1 |- ( ph -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ 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   NN0cn0 11292   ZZcz 11377   ^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-n0 11293  df-z 11378  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:  dcubic  24573