---

Step * 2 of Lemma q-constraint-negative

.....truecase..... 
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. r = 1 ∈ ℤ
⊢ uiff(0 ≤ (q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1]));0 ≤ (-(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y))))
BY
{ Auto }

1
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. r = 1 ∈ ℤ
11. 0 ≤ (q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1]))
⊢ 0 ≤ (-(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y)))

2
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. r = 1 ∈ ℤ
11. 0 ≤ (-(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y)))
⊢ 0 ≤ (q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1]))

---

Latex:

---

Latex:
.....truecase..... 
1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}
2.  r  :  \mBbbZ{}
3.  k  :  \mBbbN{}\msupplus{}
4.  y  :  \mBbbQ{}  List
5.  k  \mleq{}  ||y||
6.  x  k  <  0
7.  \mneg{}((x  k)  =  0)
8.  0  <  -(x  k)
9.  \mneg{}(r  =  0)
10.  r  =  1
\mvdash{}  uiff(0  \mleq{}  (q-linear(k  -  1;j.x  j;y)  +  ((x  k)  *  y[k  -  1]));0  \mleq{}  (-(y[k  -  1])
+  ((-1/x  k)  *  q-linear(k  -  1;j.x  j;y))))


By

---

Latex:
Auto

---

Home Index