Proof of Nuprl Lemma : near-inverse-of-increasing-function

Step * 1 2 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)

⊢ ∃c:ℤ. (∃j:ℕ⁺ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])

BY
{ ((Evaluate ⌜m = (a + b) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜j = (2 * k) ∈ ℤ⌝⋅ THENA Auto)
   THEN (InstLemma `nearby-cases` [⌜n⌝;⌜f[(r(m))/j]⌝;⌜z⌝]⋅ THENA Auto)
   THEN SplitOrHyps) }

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

⊢ ∃c:ℤ. (∃j:ℕ⁺ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])

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

⊢ ∃c:ℤ. (∃j:ℕ⁺ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])

3
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

⊢ ∃c:ℤ. (∃j:ℕ⁺ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/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) \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: ((Evaluate \mkleeneopen{}m = (a + b)\mkleeneclose{}\mcdot{} THENA Auto) THEN (Evaluate \mkleeneopen{}j = (2 * k)\mkleeneclose{}\mcdot{} THENA Auto) THEN (InstLemma `nearby-cases` [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f[(r(m))/j]\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{} THENA Auto) THEN SplitOrHyps) Home Index