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