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	$⊢ φ \to X \in ℤ$
	Assertion	cos9thpiminplylem1	$⊢ φ \to X^{3} + -3 X^{2} + 1 \neq 0$

Proof

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

Metamath Proof Explorer

Theorem cos9thpiminplylem1

Proof