---

Step * of Lemma q-geometric-series-converges

No Annotations
∀a:{a:ℚ| |a| < 1} . ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1)} .  ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ |Σ0 ≤ i < m. a ↑ i - (1/1 - a)| < e)
BY
{ ((Auto
    THEN (Assert ¬((1 - a) = 0 ∈ ℚ) BY
                ((D 0 THENA Auto) THEN QAdd ⌜a⌝ (-1)⋅ THEN DVar `a' THEN Eliminate ⌜a⌝⋅ THEN Auto))
    )
   THEN (Assert |a| ∈ {q:ℚ| (0 ≤ q) ∧ q < 1}  BY
               Auto)
   THEN (Evaluate ⌜e' = (|1 - a| * e) ∈ {e:ℚ| 0 < e} ⌝⋅ THENA Auto)) }

1
.....wf..... 
1. a : {a:ℚ| |a| < 1} 
2. e : {e:ℚ| 0 < e ∧ (e ≤ 1)} 
3. ¬((1 - a) = 0 ∈ ℚ)
4. |a| ∈ {q:ℚ| (0 ≤ q) ∧ q < 1} 
5. {e:ℚ| 0 < e}  ∈ ℙ{[1 | i 0]}
⊢ |1 - a| * e ∈ {e:ℚ| 0 < e} 

2
1. a : {a:ℚ| |a| < 1} 
2. e : {e:ℚ| 0 < e ∧ (e ≤ 1)} 
3. ¬((1 - a) = 0 ∈ ℚ)
4. |a| ∈ {q:ℚ| (0 ≤ q) ∧ q < 1} 
5. e' : {e:ℚ| 0 < e} 
6. e' = (|1 - a| * e) ∈ {e:ℚ| 0 < e} 
⊢ ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ |Σ0 ≤ i < m. a ↑ i - (1/1 - a)| < e)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\{a:\mBbbQ{}|  |a|  <  1\}  .  \mforall{}e:\{e:\mBbbQ{}|  0  <  e  \mwedge{}  (e  \mleq{}  1)\}  .
    \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  |\mSigma{}0  \mleq{}  i  <  m.  a  \muparrow{}  i  -  (1/1  -  a)|  <  e)


By

---

Latex:
((Auto
    THEN  (Assert  \mneg{}((1  -  a)  =  0)  BY
                            ((D  0  THENA  Auto)  THEN  QAdd  \mkleeneopen{}a\mkleeneclose{}  (-1)\mcdot{}  THEN  DVar  `a'  THEN  Eliminate  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THEN  Auto))
    )
  THEN  (Assert  |a|  \mmember{}  \{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\}    BY
                          Auto)
  THEN  (Evaluate  \mkleeneopen{}e'  =  (|1  -  a|  *  e)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index