---

Step * of Lemma near-inverse-of-increasing-function

∀f:ℝ ⟶ ℝ. ∀n,M:ℕ+. ∀z:ℝ. ∀a,b:ℤ.
  ∀k:ℕ+
    (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
       ((z ≤ f[(r(b))/k]) and 
       (f[(r(a))/k] ≤ z) and 
       (∀x,y:ℝ.
          (((r(a))/k ≤ x)
          ⇒ (x < y)
          ⇒ (y ≤ (r(b))/k)
          ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n)))))))) 
  supposing a < b
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN Assert ⌜∀[d:ℕ]
                  ∀a,b:ℤ.
                    ∀k:ℕ+
                      (∃c:ℤ
                        (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n)))
                               ∧ ((r(a))/k ≤ (r(c))/j)
                               ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
                         ((z ≤ f[(r(b))/k]) and 
                         (f[(r(a))/k] ≤ z) and 
                         (∀x,y:ℝ.
                            (((r(a))/k ≤ x)
                            ⇒ (x < y)
                            ⇒ (y ≤ (r(b))/k)
                            ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and 
                         (((M * (b - a)) - k) ≤ d)) 
                    supposing a < b⌝⋅
   ) }

1
.....assertion..... 
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
⊢ ∀[d:ℕ]
    ∀a,b:ℤ.
      ∀k:ℕ+
        (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
           ((z ≤ f[(r(b))/k]) and 
           (f[(r(a))/k] ≤ z) and 
           (∀x,y:ℝ.
              (((r(a))/k ≤ x)
              ⇒ (x < y)
              ⇒ (y ≤ (r(b))/k)
              ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and 
           (((M * (b - a)) - k) ≤ d)) 
      supposing a < b

2
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. ∀[d:ℕ]
     ∀a,b:ℤ.
       ∀k:ℕ+
         (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
            ((z ≤ f[(r(b))/k]) and 
            (f[(r(a))/k] ≤ z) and 
            (∀x,y:ℝ.
               (((r(a))/k ≤ x)
               ⇒ (x < y)
               ⇒ (y ≤ (r(b))/k)
               ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and 
            (((M * (b - a)) - k) ≤ d)) 
       supposing a < b
⊢ ∀a,b:ℤ.
    ∀k:ℕ+
      (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
         ((z ≤ f[(r(b))/k]) and 
         (f[(r(a))/k] ≤ z) and 
         (∀x,y:ℝ.
            (((r(a))/k ≤ x)
            ⇒ (x < y)
            ⇒ (y ≤ (r(b))/k)
            ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n)))))))) 
    supposing a < b

---

Latex:

---

Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}n,M:\mBbbN{}\msupplus{}.  \mforall{}z:\mBbbR{}.  \mforall{}a,b:\mBbbZ{}.
    \mforall{}k:\mBbbN{}\msupplus{}
        (\mexists{}c:\mBbbZ{}
            (\mexists{}j:\mBbbN{}\msupplus{}  [((|f[(r(c))/j]  -  z|  \mleq{}  (r1/r(n)))
                          \mwedge{}  ((r(a))/k  \mleq{}  (r(c))/j)
                          \mwedge{}  ((r(c))/j  \mleq{}  (r(b))/k))]))  supposing 
              ((z  \mleq{}  f[(r(b))/k])  and 
              (f[(r(a))/k]  \mleq{}  z)  and 
              (\mforall{}x,y:\mBbbR{}.
                    (((r(a))/k  \mleq{}  x)
                    {}\mRightarrow{}  (x  <  y)
                    {}\mRightarrow{}  (y  \mleq{}  (r(b))/k)
                    {}\mRightarrow{}  ((f[x]  \mleq{}  f[y])  \mwedge{}  (((y  -  x)  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  ((f[y]  -  f[x])  \mleq{}  (r1/r(n)))))))) 
    supposing  a  <  b


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}[d:\mBbbN{}]
                                \mforall{}a,b:\mBbbZ{}.
                                    \mforall{}k:\mBbbN{}\msupplus{}
                                        (\mexists{}c:\mBbbZ{}
                                            (\mexists{}j:\mBbbN{}\msupplus{}  [((|f[(r(c))/j]  -  z|  \mleq{}  (r1/r(n)))
                                                          \mwedge{}  ((r(a))/k  \mleq{}  (r(c))/j)
                                                          \mwedge{}  ((r(c))/j  \mleq{}  (r(b))/k))]))  supposing 
                                              ((z  \mleq{}  f[(r(b))/k])  and 
                                              (f[(r(a))/k]  \mleq{}  z)  and 
                                              (\mforall{}x,y:\mBbbR{}.
                                                    (((r(a))/k  \mleq{}  x)
                                                    {}\mRightarrow{}  (x  <  y)
                                                    {}\mRightarrow{}  (y  \mleq{}  (r(b))/k)
                                                    {}\mRightarrow{}  ((f[x]  \mleq{}  f[y])
                                                          \mwedge{}  (((y  -  x)  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  ((f[y]  -  f[x])  \mleq{}  (r1/r(n)))))))  and 
                                              (((M  *  (b  -  a))  -  k)  \mleq{}  d)) 
                                    supposing  a  <  b\mkleeneclose{}\mcdot{}
  )

---

Home Index