---

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


1. n : ℕ+
2. k : ℕn - 1
3. a : ℕ
4. (a * a) ≤ ((4 * n) * k)
5. (4 * n) * k < (a + 1) * (a + 1)
6. (k/n) ≤ ((a + 1/2 * n) * (a + 1/2 * n))
7. ¬(2 * a) + 1 < 4 * n
8. (2 * n) - 1 < a
9. (4 * n * n) + (-(4 * n)) + 1 < a * a
10. (4 * n * n) + (-(4 * n)) + 1 < (4 * n) * k
⊢ (2 * a) + 1 < 4 * n
BY
{ (Assert ((4 * n) * k) ≤ ((4 * n) * (n - 2)) BY
         Auto)⋅ }

1
.....assertion..... 
1. n : ℕ+
2. k : ℕn - 1
3. a : ℕ
4. (a * a) ≤ ((4 * n) * k)
5. (4 * n) * k < (a + 1) * (a + 1)
6. (k/n) ≤ ((a + 1/2 * n) * (a + 1/2 * n))
7. ¬(2 * a) + 1 < 4 * n
8. (2 * n) - 1 < a
9. (4 * n * n) + (-(4 * n)) + 1 < a * a
10. (4 * n * n) + (-(4 * n)) + 1 < (4 * n) * k
⊢ ((4 * n) * k) ≤ ((4 * n) * (n - 2))

2
1. n : ℕ+
2. k : ℕn - 1
3. a : ℕ
4. (a * a) ≤ ((4 * n) * k)
5. (4 * n) * k < (a + 1) * (a + 1)
6. (k/n) ≤ ((a + 1/2 * n) * (a + 1/2 * n))
7. ¬(2 * a) + 1 < 4 * n
8. (2 * n) - 1 < a
9. (4 * n * n) + (-(4 * n)) + 1 < a * a
10. (4 * n * n) + (-(4 * n)) + 1 < (4 * n) * k
11. ((4 * n) * k) ≤ ((4 * n) * (n - 2))
⊢ (2 * a) + 1 < 4 * n

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  ((4  *  n)  *  k)  \mleq{}  ((4  *  n)  *  (n  -  2))  BY
              Auto)\mcdot{}

---

Home Index