Step
*
1
of Lemma
qlog-exists
.....assertion.....
1. e : {e:ℚ| 0 < e}
2. q : {q:ℚ| (0 ≤ q) ∧ q < 1}
⊢ ∀[d:ℕ]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ d < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e}
BY
{ (ThinVar `e' THEN (UniformCompNatInd THEN Auto THEN (Decide e ≤ q THENA Auto))⋅)⋅ }
1
1. q : {q:ℚ| (0 ≤ q) ∧ q < 1}
2. [n] : ℕ
3. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e}
4. e : {e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ n < e}
5. e ≤ q
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e}
2
1. q : {q:ℚ| (0 ≤ q) ∧ q < 1}
2. [n] : ℕ
3. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e}
4. e : {e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ n < e}
5. ¬(e ≤ q)
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e}
Latex:
Latex:
.....assertion.....
1. e : \{e:\mBbbQ{}| 0 < e\}
2. q : \{q:\mBbbQ{}| (0 \mleq{} q) \mwedge{} q < 1\}
\mvdash{} \mforall{}[d:\mBbbN{}]. \mforall{}e:\{e:\mBbbQ{}| 0 < e \mwedge{} (e \mleq{} 1) \mwedge{} q \muparrow{} d < e\} . \{n:\mBbbN{}\msupplus{}| (e \mleq{} q \muparrow{} n - 1) \mwedge{} q \muparrow{} n < e\}
By
Latex:
(ThinVar `e' THEN (UniformCompNatInd THEN Auto THEN (Decide e \mleq{} q THENA Auto))\mcdot{})\mcdot{}
Home
Index