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 ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
Assertion cos9thpiminplylem1 ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( - 3 · ( 𝑋 ↑ 2 ) ) + 1 ) ) ≠ 0 )

Proof

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