---

Step * of Lemma canonical-bound_wf

∀[r:ℝ]. (canonical-bound(r) ∈ {k:{2...}| ∀n:ℕ+. (|r n| ≤ ((2 * n) * k))} )
BY
{ ((InstLemma `canon-bnd_wf` [] THEN ParallelLast)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN ((InstLemma `div_rem_sum` [⌜|r 1| + 4⌝;⌜2⌝]⋅ THENA Auto)
         THEN (InstLemma `rem_bounds_1` [⌜|r 1| + 4⌝;⌜2⌝]⋅ THENA Auto)
         )
   THEN (Assert canonical-bound(r) ∈ {2...} BY
               ProveWfLemma)
   THEN (Assert ⌜canon-bnd(r) ≤ (2 * canonical-bound(r))⌝⋅
   THENM (MemTypeCD THEN Auto THEN Mul ⌜n⌝ (-2)⋅ THEN RWO "4" 0 THEN Auto)
   )) }

1
.....assertion..... 
1. ∀[x:ℝ]. (canon-bnd(x) ∈ {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))} )
2. r : ℝ
3. canon-bnd(r) = canon-bnd(r) ∈ {3...}
4. ∀n:ℕ+. (|r n| ≤ (n * canon-bnd(r)))
5. (|r 1| + 4) = ((((|r 1| + 4) ÷ 2) * 2) + (|r 1| + 4 rem 2)) ∈ ℤ
6. (0 ≤ (|r 1| + 4 rem 2)) ∧ |r 1| + 4 rem 2 < 2
7. canonical-bound(r) ∈ {2...}
⊢ canon-bnd(r) ≤ (2 * canonical-bound(r))

---

Latex:

---

Latex:
\mforall{}[r:\mBbbR{}].  (canonical-bound(r)  \mmember{}  \{k:\{2...\}|  \mforall{}n:\mBbbN{}\msupplus{}.  (|r  n|  \mleq{}  ((2  *  n)  *  k))\}  )


By

---

Latex:
((InstLemma  `canon-bnd\_wf`  []  THEN  ParallelLast)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}|r  1|  +  4\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}|r  1|  +  4\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  (Assert  canonical-bound(r)  \mmember{}  \{2...\}  BY
                          ProveWfLemma)
  THEN  (Assert  \mkleeneopen{}canon-bnd(r)  \mleq{}  (2  *  canonical-bound(r))\mkleeneclose{}\mcdot{}
  THENM  (MemTypeCD  THEN  Auto  THEN  Mul  \mkleeneopen{}n\mkleeneclose{}  (-2)\mcdot{}  THEN  RWO  "4"  0  THEN  Auto)
  ))

---

Home Index