---

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

.....assertion..... 
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. b : ℕ+
5. k < ((b * b) * n) - 1
6. c : ℤ
7. c = b ∈ ℤ
8. k < ((c * c) * n) - 1
⊢ 0 < c
BY
{ Auto⋅ }

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
4.  b  :  \mBbbN{}\msupplus{}
5.  k  <  ((b  *  b)  *  n)  -  1
6.  c  :  \mBbbZ{}
7.  c  =  b
8.  k  <  ((c  *  c)  *  n)  -  1
\mvdash{}  0  <  c


By

---

Latex:
Auto\mcdot{}

---

Home Index