Step
*
1
1
of Lemma
q-not-limit-zero-diverges
.....assertion.....
1. f : ℕ ⟶ ℚ
2. ∀n:ℕ. (0 ≤ f[n])
3. q : ℚ
4. 0 < q
5. c : ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (q ≤ f[m]))
6. B : ℚ
⊢ ∃N:ℕ. (B ≤ (N * q))
BY
{ ((InstLemma `q-archimedean` [⌜(B/q)⌝]⋅ THENA Auto) THEN ExRepD THEN (QMul ⌜q⌝ (-1))⋅ THEN Auto) }
Latex:
Latex:
.....assertion.....
1. f : \mBbbN{} {}\mrightarrow{} \mBbbQ{}
2. \mforall{}n:\mBbbN{}. (0 \mleq{} f[n])
3. q : \mBbbQ{}
4. 0 < q
5. c : \mforall{}n:\mBbbN{}. \mexists{}m:\mBbbN{}. ((n \mleq{} m) \mwedge{} (q \mleq{} f[m]))
6. B : \mBbbQ{}
\mvdash{} \mexists{}N:\mBbbN{}. (B \mleq{} (N * q))
By
Latex:
((InstLemma `q-archimedean` [\mkleeneopen{}(B/q)\mkleeneclose{}]\mcdot{} THENA Auto) THEN ExRepD THEN (QMul \mkleeneopen{}q\mkleeneclose{} (-1))\mcdot{} THEN Auto)
Home
Index