Metamath Proof Explorer

Theorem cos9thpiminplylem1

Description: The polynomial ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) has no integer roots. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Hypothesis cos9thpiminplylem1.1 
|- ( ph -> X e. ZZ )
Assertion cos9thpiminplylem1 
|- ( ph -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem1.1 
 |-  ( ph -> X e. ZZ )
2 simpr 
 |-  ( ( ph /\ X = 0 ) -> X = 0 )
3 2 oveq1d 
 |-  ( ( ph /\ X = 0 ) -> ( X ^ 3 ) = ( 0 ^ 3 ) )
4 3nn 
 |-  3 e. NN
5 4 a1i 
 |-  ( ( ph /\ X = 0 ) -> 3 e. NN )
6 5 0expd 
 |-  ( ( ph /\ X = 0 ) -> ( 0 ^ 3 ) = 0 )
7 3 6 eqtrd 
 |-  ( ( ph /\ X = 0 ) -> ( X ^ 3 ) = 0 )
8 2 oveq1d 
 |-  ( ( ph /\ X = 0 ) -> ( X ^ 2 ) = ( 0 ^ 2 ) )
9 8 oveq2d 
 |-  ( ( ph /\ X = 0 ) -> ( -u 3 x. ( X ^ 2 ) ) = ( -u 3 x. ( 0 ^ 2 ) ) )
10 2nn 
 |-  2 e. NN
11 10 a1i 
 |-  ( ( ph /\ X = 0 ) -> 2 e. NN )
12 11 0expd 
 |-  ( ( ph /\ X = 0 ) -> ( 0 ^ 2 ) = 0 )
13 12 oveq2d 
 |-  ( ( ph /\ X = 0 ) -> ( -u 3 x. ( 0 ^ 2 ) ) = ( -u 3 x. 0 ) )
14 3nn0 
 |-  3 e. NN0
15 14 a1i 
 |-  ( ph -> 3 e. NN0 )
16 15 nn0cnd 
 |-  ( ph -> 3 e. CC )
17 16 adantr 
 |-  ( ( ph /\ X = 0 ) -> 3 e. CC )
18 17 negcld 
 |-  ( ( ph /\ X = 0 ) -> -u 3 e. CC )
19 18 mul01d 
 |-  ( ( ph /\ X = 0 ) -> ( -u 3 x. 0 ) = 0 )
20 9 13 19 3eqtrd 
 |-  ( ( ph /\ X = 0 ) -> ( -u 3 x. ( X ^ 2 ) ) = 0 )
21 20 oveq1d 
 |-  ( ( ph /\ X = 0 ) -> ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) = ( 0 + 1 ) )
22 7 21 oveq12d 
 |-  ( ( ph /\ X = 0 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = ( 0 + ( 0 + 1 ) ) )
23 0cnd 
 |-  ( ( ph /\ X = 0 ) -> 0 e. CC )
24 1cnd 
 |-  ( ( ph /\ X = 0 ) -> 1 e. CC )
25 23 24 addcld 
 |-  ( ( ph /\ X = 0 ) -> ( 0 + 1 ) e. CC )
26 25 addlidd 
 |-  ( ( ph /\ X = 0 ) -> ( 0 + ( 0 + 1 ) ) = ( 0 + 1 ) )
27 1cnd 
 |-  ( ph -> 1 e. CC )
28 27 addlidd 
 |-  ( ph -> ( 0 + 1 ) = 1 )
29 28 adantr 
 |-  ( ( ph /\ X = 0 ) -> ( 0 + 1 ) = 1 )
30 22 26 29 3eqtrd 
 |-  ( ( ph /\ X = 0 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = 1 )
31 ax-1ne0 
 |-  1 =/= 0
32 31 a1i 
 |-  ( ( ph /\ X = 0 ) -> 1 =/= 0 )
33 30 32 eqnetrd 
 |-  ( ( ph /\ X = 0 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
34 33 ad4ant14 
 |-  ( ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) /\ X = 0 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
35 simpr 
 |-  ( ( ph /\ X = 1 ) -> X = 1 )
36 35 oveq1d 
 |-  ( ( ph /\ X = 1 ) -> ( X ^ 3 ) = ( 1 ^ 3 ) )
37 3z 
 |-  3 e. ZZ
38 1exp 
 |-  ( 3 e. ZZ -> ( 1 ^ 3 ) = 1 )
39 37 38 mp1i 
 |-  ( ( ph /\ X = 1 ) -> ( 1 ^ 3 ) = 1 )
40 36 39 eqtrd 
 |-  ( ( ph /\ X = 1 ) -> ( X ^ 3 ) = 1 )
41 35 oveq1d 
 |-  ( ( ph /\ X = 1 ) -> ( X ^ 2 ) = ( 1 ^ 2 ) )
42 41 oveq2d 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 x. ( X ^ 2 ) ) = ( -u 3 x. ( 1 ^ 2 ) ) )
43 sq1 
 |-  ( 1 ^ 2 ) = 1
44 43 a1i 
 |-  ( ( ph /\ X = 1 ) -> ( 1 ^ 2 ) = 1 )
45 44 oveq2d 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 x. ( 1 ^ 2 ) ) = ( -u 3 x. 1 ) )
46 16 adantr 
 |-  ( ( ph /\ X = 1 ) -> 3 e. CC )
47 46 negcld 
 |-  ( ( ph /\ X = 1 ) -> -u 3 e. CC )
48 47 mulridd 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 x. 1 ) = -u 3 )
49 42 45 48 3eqtrd 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 x. ( X ^ 2 ) ) = -u 3 )
50 49 oveq1d 
 |-  ( ( ph /\ X = 1 ) -> ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) = ( -u 3 + 1 ) )
51 40 50 oveq12d 
 |-  ( ( ph /\ X = 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = ( 1 + ( -u 3 + 1 ) ) )
52 1cnd 
 |-  ( ( ph /\ X = 1 ) -> 1 e. CC )
53 47 52 addcomd 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 + 1 ) = ( 1 + -u 3 ) )
54 52 46 negsubd 
 |-  ( ( ph /\ X = 1 ) -> ( 1 + -u 3 ) = ( 1 - 3 ) )
55 53 54 eqtrd 
 |-  ( ( ph /\ X = 1 ) -> ( -u 3 + 1 ) = ( 1 - 3 ) )
56 55 oveq2d 
 |-  ( ( ph /\ X = 1 ) -> ( 1 + ( -u 3 + 1 ) ) = ( 1 + ( 1 - 3 ) ) )
57 1p1e2 
 |-  ( 1 + 1 ) = 2
58 57 a1i 
 |-  ( ( ph /\ X = 1 ) -> ( 1 + 1 ) = 2 )
59 58 oveq1d 
 |-  ( ( ph /\ X = 1 ) -> ( ( 1 + 1 ) - 3 ) = ( 2 - 3 ) )
60 52 52 46 addsubassd 
 |-  ( ( ph /\ X = 1 ) -> ( ( 1 + 1 ) - 3 ) = ( 1 + ( 1 - 3 ) ) )
61 2cnd 
 |-  ( ( ph /\ X = 1 ) -> 2 e. CC )
62 46 61 negsubdi2d 
 |-  ( ( ph /\ X = 1 ) -> -u ( 3 - 2 ) = ( 2 - 3 ) )
63 2p1e3 
 |-  ( 2 + 1 ) = 3
64 63 a1i 
 |-  ( ( ph /\ X = 1 ) -> ( 2 + 1 ) = 3 )
65 64 eqcomd 
 |-  ( ( ph /\ X = 1 ) -> 3 = ( 2 + 1 ) )
66 61 52 65 mvrladdd 
 |-  ( ( ph /\ X = 1 ) -> ( 3 - 2 ) = 1 )
67 66 negeqd 
 |-  ( ( ph /\ X = 1 ) -> -u ( 3 - 2 ) = -u 1 )
68 62 67 eqtr3d 
 |-  ( ( ph /\ X = 1 ) -> ( 2 - 3 ) = -u 1 )
69 59 60 68 3eqtr3d 
 |-  ( ( ph /\ X = 1 ) -> ( 1 + ( 1 - 3 ) ) = -u 1 )
70 51 56 69 3eqtrd 
 |-  ( ( ph /\ X = 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = -u 1 )
71 neg1ne0 
 |-  -u 1 =/= 0
72 71 a1i 
 |-  ( ( ph /\ X = 1 ) -> -u 1 =/= 0 )
73 70 72 eqnetrd 
 |-  ( ( ph /\ X = 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
74 73 ad4ant14 
 |-  ( ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) /\ X = 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
75 oveq1 
 |-  ( X = 2 -> ( X ^ 3 ) = ( 2 ^ 3 ) )
76 75 adantl 
 |-  ( ( ph /\ X = 2 ) -> ( X ^ 3 ) = ( 2 ^ 3 ) )
77 cu2 
 |-  ( 2 ^ 3 ) = 8
78 76 77 eqtrdi 
 |-  ( ( ph /\ X = 2 ) -> ( X ^ 3 ) = 8 )
79 1 zred 
 |-  ( ph -> X e. RR )
80 79 resqcld 
 |-  ( ph -> ( X ^ 2 ) e. RR )
81 80 recnd 
 |-  ( ph -> ( X ^ 2 ) e. CC )
82 16 81 mulneg1d 
 |-  ( ph -> ( -u 3 x. ( X ^ 2 ) ) = -u ( 3 x. ( X ^ 2 ) ) )
83 82 adantr 
 |-  ( ( ph /\ X = 2 ) -> ( -u 3 x. ( X ^ 2 ) ) = -u ( 3 x. ( X ^ 2 ) ) )
84 oveq1 
 |-  ( X = 2 -> ( X ^ 2 ) = ( 2 ^ 2 ) )
85 84 adantl 
 |-  ( ( ph /\ X = 2 ) -> ( X ^ 2 ) = ( 2 ^ 2 ) )
86 sq2 
 |-  ( 2 ^ 2 ) = 4
87 85 86 eqtrdi 
 |-  ( ( ph /\ X = 2 ) -> ( X ^ 2 ) = 4 )
88 87 oveq2d 
 |-  ( ( ph /\ X = 2 ) -> ( 3 x. ( X ^ 2 ) ) = ( 3 x. 4 ) )
89 88 negeqd 
 |-  ( ( ph /\ X = 2 ) -> -u ( 3 x. ( X ^ 2 ) ) = -u ( 3 x. 4 ) )
90 16 adantr 
 |-  ( ( ph /\ X = 2 ) -> 3 e. CC )
91 4cn 
 |-  4 e. CC
92 91 a1i 
 |-  ( ( ph /\ X = 2 ) -> 4 e. CC )
93 90 92 mulcomd 
 |-  ( ( ph /\ X = 2 ) -> ( 3 x. 4 ) = ( 4 x. 3 ) )
94 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
95 93 94 eqtrdi 
 |-  ( ( ph /\ X = 2 ) -> ( 3 x. 4 ) = ; 1 2 )
96 95 negeqd 
 |-  ( ( ph /\ X = 2 ) -> -u ( 3 x. 4 ) = -u ; 1 2 )
97 83 89 96 3eqtrd 
 |-  ( ( ph /\ X = 2 ) -> ( -u 3 x. ( X ^ 2 ) ) = -u ; 1 2 )
98 97 oveq1d 
 |-  ( ( ph /\ X = 2 ) -> ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) = ( -u ; 1 2 + 1 ) )
99 78 98 oveq12d 
 |-  ( ( ph /\ X = 2 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = ( 8 + ( -u ; 1 2 + 1 ) ) )
100 1nn0 
 |-  1 e. NN0
101 2nn0 
 |-  2 e. NN0
102 100 101 deccl 
 |-  ; 1 2 e. NN0
103 102 a1i 
 |-  ( ( ph /\ X = 2 ) -> ; 1 2 e. NN0 )
104 103 nn0cnd 
 |-  ( ( ph /\ X = 2 ) -> ; 1 2 e. CC )
105 104 negcld 
 |-  ( ( ph /\ X = 2 ) -> -u ; 1 2 e. CC )
106 1cnd 
 |-  ( ( ph /\ X = 2 ) -> 1 e. CC )
107 105 106 addcomd 
 |-  ( ( ph /\ X = 2 ) -> ( -u ; 1 2 + 1 ) = ( 1 + -u ; 1 2 ) )
108 106 104 negsubd 
 |-  ( ( ph /\ X = 2 ) -> ( 1 + -u ; 1 2 ) = ( 1 - ; 1 2 ) )
109 107 108 eqtrd 
 |-  ( ( ph /\ X = 2 ) -> ( -u ; 1 2 + 1 ) = ( 1 - ; 1 2 ) )
110 104 106 negsubdi2d 
 |-  ( ( ph /\ X = 2 ) -> -u ( ; 1 2 - 1 ) = ( 1 - ; 1 2 ) )
111 100 100 deccl 
 |-  ; 1 1 e. NN0
112 111 a1i 
 |-  ( ( ph /\ X = 2 ) -> ; 1 1 e. NN0 )
113 112 nn0cnd 
 |-  ( ( ph /\ X = 2 ) -> ; 1 1 e. CC )
114 106 113 addcomd 
 |-  ( ( ph /\ X = 2 ) -> ( 1 + ; 1 1 ) = ( ; 1 1 + 1 ) )
115 eqid 
 |-  ; 1 1 = ; 1 1
116 100 100 57 115 decsuc 
 |-  ( ; 1 1 + 1 ) = ; 1 2
117 114 116 eqtr2di 
 |-  ( ( ph /\ X = 2 ) -> ; 1 2 = ( 1 + ; 1 1 ) )
118 106 113 117 mvrladdd 
 |-  ( ( ph /\ X = 2 ) -> ( ; 1 2 - 1 ) = ; 1 1 )
119 118 negeqd 
 |-  ( ( ph /\ X = 2 ) -> -u ( ; 1 2 - 1 ) = -u ; 1 1 )
120 109 110 119 3eqtr2d 
 |-  ( ( ph /\ X = 2 ) -> ( -u ; 1 2 + 1 ) = -u ; 1 1 )
121 120 oveq2d 
 |-  ( ( ph /\ X = 2 ) -> ( 8 + ( -u ; 1 2 + 1 ) ) = ( 8 + -u ; 1 1 ) )
122 8nn0 
 |-  8 e. NN0
123 122 a1i 
 |-  ( ( ph /\ X = 2 ) -> 8 e. NN0 )
124 123 nn0cnd 
 |-  ( ( ph /\ X = 2 ) -> 8 e. CC )
125 124 113 negsubd 
 |-  ( ( ph /\ X = 2 ) -> ( 8 + -u ; 1 1 ) = ( 8 - ; 1 1 ) )
126 113 124 negsubdi2d 
 |-  ( ( ph /\ X = 2 ) -> -u ( ; 1 1 - 8 ) = ( 8 - ; 1 1 ) )
127 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
128 127 a1i 
 |-  ( ( ph /\ X = 2 ) -> ( 8 + 3 ) = ; 1 1 )
129 128 eqcomd 
 |-  ( ( ph /\ X = 2 ) -> ; 1 1 = ( 8 + 3 ) )
130 124 90 129 mvrladdd 
 |-  ( ( ph /\ X = 2 ) -> ( ; 1 1 - 8 ) = 3 )
131 130 negeqd 
 |-  ( ( ph /\ X = 2 ) -> -u ( ; 1 1 - 8 ) = -u 3 )
132 125 126 131 3eqtr2d 
 |-  ( ( ph /\ X = 2 ) -> ( 8 + -u ; 1 1 ) = -u 3 )
133 99 121 132 3eqtrd 
 |-  ( ( ph /\ X = 2 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) = -u 3 )
134 0red 
 |-  ( ph -> 0 e. RR )
135 15 nn0red 
 |-  ( ph -> 3 e. RR )
136 neg0 
 |-  -u 0 = 0
137 136 a1i 
 |-  ( ph -> -u 0 = 0 )
138 3pos 
 |-  0 < 3
139 137 138 eqbrtrdi 
 |-  ( ph -> -u 0 < 3 )
140 134 135 139 ltnegcon1d 
 |-  ( ph -> -u 3 < 0 )
141 140 adantr 
 |-  ( ( ph /\ X = 2 ) -> -u 3 < 0 )
142 141 lt0ne0d 
 |-  ( ( ph /\ X = 2 ) -> -u 3 =/= 0 )
143 133 142 eqnetrd 
 |-  ( ( ph /\ X = 2 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
144 143 ad4ant14 
 |-  ( ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) /\ X = 2 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
145 1 ad2antrr 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> X e. ZZ )
146 0zd 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> 0 e. ZZ )
147 37 a1i 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> 3 e. ZZ )
148 df-neg 
 |-  -u 1 = ( 0 - 1 )
149 simplr 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> -u 1 < X )
150 148 149 eqbrtrrid 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> ( 0 - 1 ) < X )
151 zlem1lt 
 |-  ( ( 0 e. ZZ /\ X e. ZZ ) -> ( 0 <_ X <-> ( 0 - 1 ) < X ) )
152 151 biimpar 
 |-  ( ( ( 0 e. ZZ /\ X e. ZZ ) /\ ( 0 - 1 ) < X ) -> 0 <_ X )
153 146 145 150 152 syl21anc 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> 0 <_ X )
154 simpr 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> X < 3 )
155 elfzo 
 |-  ( ( X e. ZZ /\ 0 e. ZZ /\ 3 e. ZZ ) -> ( X e. ( 0 ..^ 3 ) <-> ( 0 <_ X /\ X < 3 ) ) )
156 155 biimpar 
 |-  ( ( ( X e. ZZ /\ 0 e. ZZ /\ 3 e. ZZ ) /\ ( 0 <_ X /\ X < 3 ) ) -> X e. ( 0 ..^ 3 ) )
157 145 146 147 153 154 156 syl32anc 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> X e. ( 0 ..^ 3 ) )
158 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
159 157 158 eleqtrdi 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> X e. { 0 , 1 , 2 } )
160 eltpg 
 |-  ( X e. ZZ -> ( X e. { 0 , 1 , 2 } <-> ( X = 0 \/ X = 1 \/ X = 2 ) ) )
161 160 biimpa 
 |-  ( ( X e. ZZ /\ X e. { 0 , 1 , 2 } ) -> ( X = 0 \/ X = 1 \/ X = 2 ) )
162 145 159 161 syl2anc 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> ( X = 0 \/ X = 1 \/ X = 2 ) )
163 34 74 144 162 mpjao3dan 
 |-  ( ( ( ph /\ -u 1 < X ) /\ X < 3 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
164 1 15 zexpcld 
 |-  ( ph -> ( X ^ 3 ) e. ZZ )
165 164 zred 
 |-  ( ph -> ( X ^ 3 ) e. RR )
166 135 renegcld 
 |-  ( ph -> -u 3 e. RR )
167 166 80 remulcld 
 |-  ( ph -> ( -u 3 x. ( X ^ 2 ) ) e. RR )
168 165 167 readdcld 
 |-  ( ph -> ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) e. RR )
169 168 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) e. RR )
170 1red 
 |-  ( ( ph /\ 3 <_ X ) -> 1 e. RR )
171 80 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( X ^ 2 ) e. RR )
172 79 135 resubcld 
 |-  ( ph -> ( X - 3 ) e. RR )
173 172 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( X - 3 ) e. RR )
174 79 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> X e. RR )
175 174 sqge0d 
 |-  ( ( ph /\ 3 <_ X ) -> 0 <_ ( X ^ 2 ) )
176 135 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> 3 e. RR )
177 0red 
 |-  ( ( ph /\ 3 <_ X ) -> 0 e. RR )
178 simpr 
 |-  ( ( ph /\ 3 <_ X ) -> 3 <_ X )
179 79 recnd 
 |-  ( ph -> X e. CC )
180 179 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
181 180 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( X - 0 ) = X )
182 178 181 breqtrrd 
 |-  ( ( ph /\ 3 <_ X ) -> 3 <_ ( X - 0 ) )
183 176 174 177 182 lesubd 
 |-  ( ( ph /\ 3 <_ X ) -> 0 <_ ( X - 3 ) )
184 171 173 175 183 mulge0d 
 |-  ( ( ph /\ 3 <_ X ) -> 0 <_ ( ( X ^ 2 ) x. ( X - 3 ) ) )
185 81 179 16 subdid 
 |-  ( ph -> ( ( X ^ 2 ) x. ( X - 3 ) ) = ( ( ( X ^ 2 ) x. X ) - ( ( X ^ 2 ) x. 3 ) ) )
186 81 179 mulcld 
 |-  ( ph -> ( ( X ^ 2 ) x. X ) e. CC )
187 81 16 mulcld 
 |-  ( ph -> ( ( X ^ 2 ) x. 3 ) e. CC )
188 186 187 negsubd 
 |-  ( ph -> ( ( ( X ^ 2 ) x. X ) + -u ( ( X ^ 2 ) x. 3 ) ) = ( ( ( X ^ 2 ) x. X ) - ( ( X ^ 2 ) x. 3 ) ) )
189 100 a1i 
 |-  ( ph -> 1 e. NN0 )
190 101 a1i 
 |-  ( ph -> 2 e. NN0 )
191 179 189 190 expaddd 
 |-  ( ph -> ( X ^ ( 2 + 1 ) ) = ( ( X ^ 2 ) x. ( X ^ 1 ) ) )
192 63 a1i 
 |-  ( ph -> ( 2 + 1 ) = 3 )
193 192 oveq2d 
 |-  ( ph -> ( X ^ ( 2 + 1 ) ) = ( X ^ 3 ) )
194 179 exp1d 
 |-  ( ph -> ( X ^ 1 ) = X )
195 194 oveq2d 
 |-  ( ph -> ( ( X ^ 2 ) x. ( X ^ 1 ) ) = ( ( X ^ 2 ) x. X ) )
196 191 193 195 3eqtr3rd 
 |-  ( ph -> ( ( X ^ 2 ) x. X ) = ( X ^ 3 ) )
197 81 16 mulcomd 
 |-  ( ph -> ( ( X ^ 2 ) x. 3 ) = ( 3 x. ( X ^ 2 ) ) )
198 197 negeqd 
 |-  ( ph -> -u ( ( X ^ 2 ) x. 3 ) = -u ( 3 x. ( X ^ 2 ) ) )
199 198 82 eqtr4d 
 |-  ( ph -> -u ( ( X ^ 2 ) x. 3 ) = ( -u 3 x. ( X ^ 2 ) ) )
200 196 199 oveq12d 
 |-  ( ph -> ( ( ( X ^ 2 ) x. X ) + -u ( ( X ^ 2 ) x. 3 ) ) = ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) )
201 185 188 200 3eqtr2d 
 |-  ( ph -> ( ( X ^ 2 ) x. ( X - 3 ) ) = ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) )
202 201 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( ( X ^ 2 ) x. ( X - 3 ) ) = ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) )
203 184 202 breqtrd 
 |-  ( ( ph /\ 3 <_ X ) -> 0 <_ ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) )
204 0lt1 
 |-  0 < 1
205 204 a1i 
 |-  ( ( ph /\ 3 <_ X ) -> 0 < 1 )
206 169 170 203 205 addgegt0d 
 |-  ( ( ph /\ 3 <_ X ) -> 0 < ( ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) + 1 ) )
207 165 recnd 
 |-  ( ph -> ( X ^ 3 ) e. CC )
208 207 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( X ^ 3 ) e. CC )
209 167 recnd 
 |-  ( ph -> ( -u 3 x. ( X ^ 2 ) ) e. CC )
210 209 adantr 
 |-  ( ( ph /\ 3 <_ X ) -> ( -u 3 x. ( X ^ 2 ) ) e. CC )
211 1cnd 
 |-  ( ( ph /\ 3 <_ X ) -> 1 e. CC )
212 208 210 211 addassd 
 |-  ( ( ph /\ 3 <_ X ) -> ( ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) + 1 ) = ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) )
213 206 212 breqtrd 
 |-  ( ( ph /\ 3 <_ X ) -> 0 < ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) )
214 213 gt0ne0d 
 |-  ( ( ph /\ 3 <_ X ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
215 214 adantlr 
 |-  ( ( ( ph /\ -u 1 < X ) /\ 3 <_ X ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
216 79 adantr 
 |-  ( ( ph /\ -u 1 < X ) -> X e. RR )
217 135 adantr 
 |-  ( ( ph /\ -u 1 < X ) -> 3 e. RR )
218 163 215 216 217 ltlecasei 
 |-  ( ( ph /\ -u 1 < X ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
219 165 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 3 ) e. RR )
220 167 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 3 x. ( X ^ 2 ) ) e. RR )
221 1red 
 |-  ( ( ph /\ X <_ -u 1 ) -> 1 e. RR )
222 220 221 readdcld 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) e. RR )
223 219 222 readdcld 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) e. RR )
224 166 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 3 e. RR )
225 0red 
 |-  ( ( ph /\ X <_ -u 1 ) -> 0 e. RR )
226 219 220 readdcld 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) e. RR )
227 4re 
 |-  4 e. RR
228 227 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> 4 e. RR )
229 228 renegcld 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 4 e. RR )
230 1red 
 |-  ( ph -> 1 e. RR )
231 230 renegcld 
 |-  ( ph -> -u 1 e. RR )
232 231 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 1 e. RR )
233 79 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> X e. RR )
234 4 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> 3 e. NN )
235 n2dvds3 
 |-  -. 2 || 3
236 235 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> -. 2 || 3 )
237 simpr 
 |-  ( ( ph /\ X <_ -u 1 ) -> X <_ -u 1 )
238 233 232 234 236 237 oexpled 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 3 ) <_ ( -u 1 ^ 3 ) )
239 m1expo 
 |-  ( ( 3 e. ZZ /\ -. 2 || 3 ) -> ( -u 1 ^ 3 ) = -u 1 )
240 37 236 239 sylancr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 1 ^ 3 ) = -u 1 )
241 238 240 breqtrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 3 ) <_ -u 1 )
242 234 nncnd 
 |-  ( ( ph /\ X <_ -u 1 ) -> 3 e. CC )
243 81 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 2 ) e. CC )
244 242 243 mulneg1d 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 3 x. ( X ^ 2 ) ) = -u ( 3 x. ( X ^ 2 ) ) )
245 135 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> 3 e. RR )
246 135 80 remulcld 
 |-  ( ph -> ( 3 x. ( X ^ 2 ) ) e. RR )
247 246 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 3 x. ( X ^ 2 ) ) e. RR )
248 80 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 2 ) e. RR )
249 14 nn0ge0i 
 |-  0 <_ 3
250 249 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> 0 <_ 3 )
251 233 221 237 lenegcon2d 
 |-  ( ( ph /\ X <_ -u 1 ) -> 1 <_ -u X )
252 233 renegcld 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u X e. RR )
253 0le1 
 |-  0 <_ 1
254 253 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> 0 <_ 1 )
255 neg1rr 
 |-  -u 1 e. RR
256 0re 
 |-  0 e. RR
257 neg1lt0 
 |-  -u 1 < 0
258 255 256 257 ltleii 
 |-  -u 1 <_ 0
259 258 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 1 <_ 0 )
260 233 232 225 237 259 letrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> X <_ 0 )
261 leneg 
 |-  ( ( X e. RR /\ 0 e. RR ) -> ( X <_ 0 <-> -u 0 <_ -u X ) )
262 261 biimpa 
 |-  ( ( ( X e. RR /\ 0 e. RR ) /\ X <_ 0 ) -> -u 0 <_ -u X )
263 233 225 260 262 syl21anc 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 0 <_ -u X )
264 136 263 eqbrtrrid 
 |-  ( ( ph /\ X <_ -u 1 ) -> 0 <_ -u X )
265 221 252 254 264 le2sqd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 1 <_ -u X <-> ( 1 ^ 2 ) <_ ( -u X ^ 2 ) ) )
266 251 265 mpbid 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 1 ^ 2 ) <_ ( -u X ^ 2 ) )
267 233 recnd 
 |-  ( ( ph /\ X <_ -u 1 ) -> X e. CC )
268 267 sqnegd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u X ^ 2 ) = ( X ^ 2 ) )
269 266 268 breqtrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 1 ^ 2 ) <_ ( X ^ 2 ) )
270 43 269 eqbrtrrid 
 |-  ( ( ph /\ X <_ -u 1 ) -> 1 <_ ( X ^ 2 ) )
271 245 248 250 270 lemulge11d 
 |-  ( ( ph /\ X <_ -u 1 ) -> 3 <_ ( 3 x. ( X ^ 2 ) ) )
272 leneg 
 |-  ( ( 3 e. RR /\ ( 3 x. ( X ^ 2 ) ) e. RR ) -> ( 3 <_ ( 3 x. ( X ^ 2 ) ) <-> -u ( 3 x. ( X ^ 2 ) ) <_ -u 3 ) )
273 272 biimpa 
 |-  ( ( ( 3 e. RR /\ ( 3 x. ( X ^ 2 ) ) e. RR ) /\ 3 <_ ( 3 x. ( X ^ 2 ) ) ) -> -u ( 3 x. ( X ^ 2 ) ) <_ -u 3 )
274 245 247 271 273 syl21anc 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u ( 3 x. ( X ^ 2 ) ) <_ -u 3 )
275 244 274 eqbrtrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 3 x. ( X ^ 2 ) ) <_ -u 3 )
276 219 220 232 224 241 275 le2addd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) <_ ( -u 1 + -u 3 ) )
277 1cnd 
 |-  ( ( ph /\ X <_ -u 1 ) -> 1 e. CC )
278 277 242 negdid 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u ( 1 + 3 ) = ( -u 1 + -u 3 ) )
279 277 242 addcomd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 1 + 3 ) = ( 3 + 1 ) )
280 3p1e4 
 |-  ( 3 + 1 ) = 4
281 279 280 eqtrdi 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( 1 + 3 ) = 4 )
282 281 negeqd 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u ( 1 + 3 ) = -u 4 )
283 278 282 eqtr3d 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 1 + -u 3 ) = -u 4 )
284 276 283 breqtrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) <_ -u 4 )
285 226 229 221 284 leadd1dd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) + 1 ) <_ ( -u 4 + 1 ) )
286 207 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( X ^ 3 ) e. CC )
287 209 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 3 x. ( X ^ 2 ) ) e. CC )
288 286 287 277 addassd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( ( X ^ 3 ) + ( -u 3 x. ( X ^ 2 ) ) ) + 1 ) = ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) )
289 ax-1cn 
 |-  1 e. CC
290 91 289 negsubdii 
 |-  -u ( 4 - 1 ) = ( -u 4 + 1 )
291 4m1e3 
 |-  ( 4 - 1 ) = 3
292 291 negeqi 
 |-  -u ( 4 - 1 ) = -u 3
293 290 292 eqtr3i 
 |-  ( -u 4 + 1 ) = -u 3
294 293 a1i 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( -u 4 + 1 ) = -u 3 )
295 285 288 294 3brtr3d 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) <_ -u 3 )
296 140 adantr 
 |-  ( ( ph /\ X <_ -u 1 ) -> -u 3 < 0 )
297 223 224 225 295 296 lelttrd 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) < 0 )
298 297 lt0ne0d 
 |-  ( ( ph /\ X <_ -u 1 ) -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )
299 218 298 231 79 ltlecasei 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( -u 3 x. ( X ^ 2 ) ) + 1 ) ) =/= 0 )