---

Step * 1 2 1 7 of Lemma near-inverse-of-increasing-function


1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. [n@0] : ℕ
6. ∀[m:ℕn@0]
     ∀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) ≤ m)) 
       supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀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))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. f[(r(m))/j] < z
21. bb : ℤ
22. bb = (2 * b) ∈ ℤ
23. ∃c:ℤ. (∃j@0:ℕ+ [((|f[(r(c))/j@0] - z| ≤ (r1/r(n))) ∧ ((r(m))/j ≤ (r(c))/j@0) ∧ ((r(c))/j@0 ≤ (r(bb))/j))])
⊢ ∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])
BY
{ (RepeatFor 2 (ParallelLast) THEN Auto THEN (RWO "-3< -3" 0 THENA Auto)) }

1
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
     ∀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) ≤ m)) 
       supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀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))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. f[(r(m))/j] < z
21. bb : ℤ
22. bb = (2 * b) ∈ ℤ
23. c : ℤ
24. j@0 : ℕ+
25. |f[(r(c))/j@0] - z| ≤ (r1/r(n))
26. (r(m))/j ≤ (r(c))/j@0
27. (r(c))/j@0 ≤ (r(bb))/j
28. |f[(r(c))/j@0] - z| ≤ (r1/r(n))
⊢ (r(a))/k ≤ (r(m))/j

2
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
     ∀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) ≤ m)) 
       supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀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))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. f[(r(m))/j] < z
21. bb : ℤ
22. bb = (2 * b) ∈ ℤ
23. c : ℤ
24. j@0 : ℕ+
25. |f[(r(c))/j@0] - z| ≤ (r1/r(n))
26. (r(m))/j ≤ (r(c))/j@0
27. (r(c))/j@0 ≤ (r(bb))/j
28. |f[(r(c))/j@0] - z| ≤ (r1/r(n))
29. (r(a))/k ≤ (r(c))/j@0
⊢ (r(bb))/j ≤ (r(b))/k

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  M  :  \mBbbN{}\msupplus{}
4.  z  :  \mBbbR{}
5.  [n@0]  :  \mBbbN{}
6.  \mforall{}[m:\mBbbN{}n@0]
          \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{}  m)) 
              supposing  a  <  b
7.  a  :  \mBbbZ{}
8.  b  :  \mBbbZ{}
9.  a  <  b
10.  k  :  \mBbbN{}\msupplus{}
11.  ((M  *  (b  -  a))  -  k)  \mleq{}  n@0
12.  \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))))))
13.  f[(r(a))/k]  \mleq{}  z
14.  z  \mleq{}  f[(r(b))/k]
15.  \mneg{}((M  *  (b  -  a))  \mleq{}  k)
16.  m  :  \mBbbZ{}
17.  m  =  (a  +  b)
18.  j  :  \mBbbZ{}
19.  j  =  (2  *  k)
20.  f[(r(m))/j]  <  z
21.  bb  :  \mBbbZ{}
22.  bb  =  (2  *  b)
23.  \mexists{}c:\mBbbZ{}
          (\mexists{}j@0:\mBbbN{}\msupplus{}  [((|f[(r(c))/j@0]  -  z|  \mleq{}  (r1/r(n)))
                            \mwedge{}  ((r(m))/j  \mleq{}  (r(c))/j@0)
                            \mwedge{}  ((r(c))/j@0  \mleq{}  (r(bb))/j))])
\mvdash{}  \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))])


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  Auto  THEN  (RWO  "-3<  -3"  0  THENA  Auto))

---

Home Index