---

Step * 2 1 1 of Lemma square-between-lemma2


1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. (k + 1) = ((((k + 1) ÷ n) * n) + (k + 1 rem n)) ∈ ℤ
5. 0 ≤ (k + 1 rem n)
6. k + 1 rem n < n
7. 0 ≤ ((k + 1) ÷ n)
8. v : ℕ
9. (v * v) ≤ (((k + 1) ÷ n) + 1)
10. ((k + 1) ÷ n) + 1 < (v + 1) * (v + 1)
⊢ k < (((v + 1) * (v + 1)) * n) - 1
BY
{ (MoveToConcl (-1) THEN GenConclAtAddr [1;2]) }

1
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. (k + 1) = ((((k + 1) ÷ n) * n) + (k + 1 rem n)) ∈ ℤ
5. 0 ≤ (k + 1 rem n)
6. k + 1 rem n < n
7. 0 ≤ ((k + 1) ÷ n)
8. v : ℕ
9. (v * v) ≤ (((k + 1) ÷ n) + 1)
10. v1 : ℤ
11. ((v + 1) * (v + 1)) = v1 ∈ ℤ
⊢ ((k + 1) ÷ n) + 1 < v1 ⇒ k < (v1 * n) - 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
4.  (k  +  1)  =  ((((k  +  1)  \mdiv{}  n)  *  n)  +  (k  +  1  rem  n))
5.  0  \mleq{}  (k  +  1  rem  n)
6.  k  +  1  rem  n  <  n
7.  0  \mleq{}  ((k  +  1)  \mdiv{}  n)
8.  v  :  \mBbbN{}
9.  (v  *  v)  \mleq{}  (((k  +  1)  \mdiv{}  n)  +  1)
10.  ((k  +  1)  \mdiv{}  n)  +  1  <  (v  +  1)  *  (v  +  1)
\mvdash{}  k  <  (((v  +  1)  *  (v  +  1))  *  n)  -  1


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;2])

---

Home Index