---

Step * of Lemma case-real3-seq_wf

∀[f:ℕ+ ⟶ 𝔹]. ∀[b:ℝ]. ∀[a:ℝ supposing ∃n:ℕ+. (↑(f n))].
  case-real3-seq(a;b;f) ∈ {s:ℕ+ ⟶ ℤ| 3-regular-seq(s)}  supposing ∀n,m:ℕ+.  ((↑(f n)) ⇒ (¬↑(f m)) ⇒ (|(a m) - b m| ≤ \000C4))
BY
{ (Auto
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``case-real3-seq`` 0
   THEN Auto
   THEN RepeatFor 2 ((D 0 THENW Auto))
   THEN Reduce 0
   THEN (BoolCase ⌜f n⌝⋅ THENA Auto)
   THEN (BoolCase ⌜f m⌝⋅ THENA Auto)
   THEN (Assert |(m * (b n)) - n * (b m)| ≤ (2 * (n + m)) BY
               (((DVar `b' THEN Unhide) THENA Auto) THEN BackThruSomeHyp' THEN Auto))
   THEN Try ((RWO "-1" 0 THEN Auto))
   THEN (Assert |(m * (a n)) - n * (a m)| ≤ (2 * (n + m)) BY
               ((Assert a ∈ ℝ BY
                       Auto)
                THEN (MemTypeHD (-1) THENA Auto)
                THEN (Unhide THENA Auto)
                THEN BackThruHyp' (-1)
                THEN Auto))
   THEN Try ((RWO "-1" 0 THEN Auto))) }

1
1. f : ℕ+ ⟶ 𝔹
2. b : ℝ
3. a : ℝ supposing ∃n:ℕ+. (↑(f n))
4. ∀n,m:ℕ+.  ((↑(f n)) ⇒ (¬↑(f m)) ⇒ (|(a m) - b m| ≤ 4))
5. n : ℕ+
6. m : ℕ+
7. ¬↑(f m)
8. ↑(f n)
9. |(m * (b n)) - n * (b m)| ≤ (2 * (n + m))
10. |(m * (a n)) - n * (a m)| ≤ (2 * (n + m))
⊢ |(m * (a n)) - n * (b m)| ≤ (6 * (n + m))

2
1. f : ℕ+ ⟶ 𝔹
2. b : ℝ
3. a : ℝ supposing ∃n:ℕ+. (↑(f n))
4. ∀n,m:ℕ+.  ((↑(f n)) ⇒ (¬↑(f m)) ⇒ (|(a m) - b m| ≤ 4))
5. n : ℕ+
6. ¬↑(f n)
7. m : ℕ+
8. ↑(f m)
9. |(m * (b n)) - n * (b m)| ≤ (2 * (n + m))
10. |(m * (a n)) - n * (a m)| ≤ (2 * (n + m))
⊢ |(m * (b n)) - n * (a m)| ≤ (6 * (n + m))

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:\mBbbR{}].  \mforall{}[a:\mBbbR{}  supposing  \mexists{}n:\mBbbN{}\msupplus{}.  (\muparrow{}(f  n))].
    case-real3-seq(a;b;f)  \mmember{}  \{s:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  3-regular-seq(s)\}    supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    ((\muparrow{}(f  n))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  m))  \000C{}\mRightarrow{}  (|(a  m)  -  b  m|  \mleq{}  4))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``case-real3-seq``  0
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THENW  Auto))
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}f  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}f  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  |(m  *  (b  n))  -  n  *  (b  m)|  \mleq{}  (2  *  (n  +  m))  BY
                          (((DVar  `b'  THEN  Unhide)  THENA  Auto)  THEN  BackThruSomeHyp'  THEN  Auto))
  THEN  Try  ((RWO  "-1"  0  THEN  Auto))
  THEN  (Assert  |(m  *  (a  n))  -  n  *  (a  m)|  \mleq{}  (2  *  (n  +  m))  BY
                          ((Assert  a  \mmember{}  \mBbbR{}  BY
                                          Auto)
                            THEN  (MemTypeHD  (-1)  THENA  Auto)
                            THEN  (Unhide  THENA  Auto)
                            THEN  BackThruHyp'  (-1)
                            THEN  Auto))
  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))

---

Home Index