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

Metamath Proof Explorer

Theorem cos9thpiminplylem1

Proof