Step * 2 of Lemma square-between-lemma2


1. : ℕ+
2. : ℕ
3. ¬k < 1
⊢ ∃q:ℚ [(((k/n) ≤ (q q)) ∧ q < (k 1/n) ∧ (0 ≤ q))]
BY
Assert ⌜∃b:ℕ+ [k < ((b b) n) 1]⌝⋅ }

1
.....assertion..... 
1. : ℕ+
2. : ℕ
3. ¬k < 1
⊢ ∃b:ℕ+ [k < ((b b) n) 1]

2
1. : ℕ+
2. : ℕ
3. ¬k < 1
4. ∃b:ℕ+ [k < ((b b) n) 1]
⊢ ∃q:ℚ [(((k/n) ≤ (q q)) ∧ q < (k 1/n) ∧ (0 ≤ q))]


Latex:


Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
\mvdash{}  \mexists{}q:\mBbbQ{}  [(((k/n)  \mleq{}  (q  *  q))  \mwedge{}  q  *  q  <  (k  +  1/n)  \mwedge{}  (0  \mleq{}  q))]


By


Latex:
Assert  \mkleeneopen{}\mexists{}b:\mBbbN{}\msupplus{}  [k  <  ((b  *  b)  *  n)  -  1]\mkleeneclose{}\mcdot{}




Home Index