---

Step * 1 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 ∈ ℤ
⊢ 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. 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. 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.  r  =  0
\mvdash{}  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

---

Latex:
Auto

---

Home Index