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