---

Step * of Lemma log-from_wf

∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} .  (log-from(a;b) ∈ {x:ℝ| x = rlog(a)} )
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `req-from-converges` 
            [⌜λ2n.logseq(a;b;n)⌝;⌜rlog(a)⌝;⌜TERMOF{logseq-converges-ext:o, \\v:l} a b⌝]⋅
         THENA Auto
         )
   THEN Assert ⌜log-from(a;b)
                = cauchy-limit(n.logseq(a;b;n);λk.(TERMOF{logseq-converges-ext:o, \\v:l} a b (2 * k)))
                ∈ (ℕ+ ⟶ ℤ)⌝⋅) }

1
.....assertion..... 
1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. rlog(a) = cauchy-limit(n.logseq(a;b;n);λk.(TERMOF{logseq-converges-ext:o, \\v:l} a b (2 * k)))
⊢ log-from(a;b) = cauchy-limit(n.logseq(a;b;n);λk.(TERMOF{logseq-converges-ext:o, \\v:l} a b (2 * k))) ∈ (ℕ+ ⟶ ℤ)

2
1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. rlog(a) = cauchy-limit(n.logseq(a;b;n);λk.(TERMOF{logseq-converges-ext:o, \\v:l} a b (2 * k)))
4. log-from(a;b) = cauchy-limit(n.logseq(a;b;n);λk.(TERMOF{logseq-converges-ext:o, \\v:l} a b (2 * k))) ∈ (ℕ+ ⟶ ℤ)
⊢ log-from(a;b) ∈ {x:ℝ| x = rlog(a)} 

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\}  .  \mforall{}b:\{b:\mBbbR{}|  |b  -  rlog(a)|  \mleq{}  (r1/r(10))\}  .    (log-from(a;b)  \mmember{}  \{x:\mBbbR{}|  x  =  rlog(a)\}  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `req-from-converges` 
                    [\mkleeneopen{}\mlambda{}\msubtwo{}n.logseq(a;b;n)\mkleeneclose{};\mkleeneopen{}rlog(a)\mkleeneclose{};\mkleeneopen{}TERMOF\{logseq-converges-ext:o,  \mbackslash{}\mbackslash{}v:l\}  a  b\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Assert  \mkleeneopen{}log-from(a;b)
                            =  cauchy-limit(n.logseq(a;b;n);\mlambda{}k.(TERMOF\{logseq-converges-ext:o,  \mbackslash{}\mbackslash{}v:l\}  a  b 
                                                                                                  (2  *  k)))\mkleeneclose{}\mcdot{})

---

Home Index