Step * 2 1 1 1 3 of Lemma near-log-exists


1. ∀a:{a:ℝr1 ≤ a} . ∀N:ℕ+.  ∃m:ℕ+(∃z:ℤ [(|(r(z))/m rlog(a)| ≤ (r1/r(N)))])
2. {a:ℝr0 < a} 
3. : ℕ+
4. |r0 rlog(a)| ≤ (|r1 a|/rmin(a;r1))
5. r0 < rmin(a;r1)
6. |r1 a| ≤ (r1/r(N 1))
⊢ ∃m:ℕ+(∃z:ℤ [(|(r(z))/m rlog(a)| ≤ (r1/r(N)))])
BY
((D With ⌜1⌝  THENA Auto) THEN (D With ⌜0⌝  THENA Auto)) }

1
1. ∀a:{a:ℝr1 ≤ a} . ∀N:ℕ+.  ∃m:ℕ+(∃z:ℤ [(|(r(z))/m rlog(a)| ≤ (r1/r(N)))])
2. {a:ℝr0 < a} 
3. : ℕ+
4. |r0 rlog(a)| ≤ (|r1 a|/rmin(a;r1))
5. r0 < rmin(a;r1)
6. |r1 a| ≤ (r1/r(N 1))
⊢ |(r0)/1 rlog(a)| ≤ (r1/r(N))


Latex:


Latex:

1.  \mforall{}a:\{a:\mBbbR{}|  r1  \mleq{}  a\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])
2.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
3.  N  :  \mBbbN{}\msupplus{}
4.  |r0  -  rlog(a)|  \mleq{}  (|r1  -  a|/rmin(a;r1))
5.  r0  <  rmin(a;r1)
6.  |r1  -  a|  \mleq{}  (r1/r(N  +  1))
\mvdash{}  \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])


By


Latex:
((D  0  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto))




Home Index