Proof of Nuprl Lemma : derivative-rinv

Step * 1 2 of Lemma derivative-rinv

1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. d(f[x])/dx = λx.g[x] on I
6. k : ℕ⁺
7. n : {n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
8. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
9. i-approx(I;n) ⊆ I
10. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
11. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
12. (r1/f[x]) continuous for x ∈ i-approx(I;n)
13. g[x] continuous for x ∈ i-approx(I;n)
14. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
15. ∃M:ℕ⁺. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]
BY
{ (D (-1)
   THEN (With ⌜(2 * M * M) * k⌝ (D 5)⋅ THENA Auto)
   THEN With ⌜n⌝ (D (-1))⋅
   THEN Auto
   THEN D -1
   THEN (Assert (2 * (M * M) * M * M) * k ∈ ℕ⁺ BY
               Auto)
   THEN (InstLemma `function-is-continuous` [⌜i-approx(I;n)⌝;⌜λ₂x.f[x]⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜n⌝  THENA (RWO "i-approx-approx" 0 THEN Auto))
   THEN (RWO "i-approx-approx" (-1) THENA Auto)
   THEN With ⌜(2 * (M * M) * M * M) * k⌝ (D (-1))⋅
   THEN Auto
   THEN D -1) }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ⁺
6. n : {n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ⁺
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. [%24] : (r0 < del)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;n))
     ⇒ (y ∈ i-approx(I;n))
     ⇒ (|y - x| ≤ del)
     ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|))))
18. (2 * (M * M) * M * M) * k ∈ ℕ⁺
19. d : ℝ
20. [%33] : (r0 < d)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;n))
     ⇒ (y ∈ i-approx(I;n))
     ⇒ (|x - y| ≤ d)
     ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k)))))
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]

Latex:

Latex:
1. I : Interval 2. f : I {}\mrightarrow{}\mBbbR{} 3. g : I {}\mrightarrow{}\mBbbR{} 4. \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (g[x] = g[y])) 5. d(f[x])/dx = \mlambda{}x.g[x] on I 6. k : \mBbbN{}\msupplus{} 7. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\} 8. \mforall{}a,b:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . ((a = b) {}\mRightarrow{} (f[a] = f[b])) 9. i-approx(I;n) \msubseteq{} I 10. \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} f[x] \mneq{} r0) 11. \mexists{}c:\mBbbR{} [((r0 < c) \mwedge{} (\mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (c \mleq{} |f[x]|))))] 12. (r1/f[x]) continuous for x \mmember{} i-approx(I;n) 13. g[x] continuous for x \mmember{} i-approx(I;n) 14. \mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} f[x] \mneq{} r0) 15. \mexists{}M:\mBbbN{}\msupplus{}. \mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} ((|g[x]| \mleq{} r(M)) \mwedge{} (|(r1/f[x])| \mleq{} r(M)))) \mvdash{} \mexists{}del:\mBbbR{} [((r0 < del) \mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (y \mmember{} i-approx(I;n)) {}\mRightarrow{} (|y - x| \mleq{} del) {}\mRightarrow{} (|(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)))))] By Latex: (D (-1) THEN (With \mkleeneopen{}(2 * M * M) * k\mkleeneclose{} (D 5)\mcdot{} THENA Auto) THEN With \mkleeneopen{}n\mkleeneclose{} (D (-1))\mcdot{} THEN Auto THEN D -1 THEN (Assert (2 * (M * M) * M * M) * k \mmember{} \mBbbN{}\msupplus{} BY Auto) THEN (InstLemma `function-is-continuous` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f[x]\mkleeneclose{}]\mcdot{} THENA Auto) THEN (D -1 With \mkleeneopen{}n\mkleeneclose{} THENA (RWO "i-approx-approx" 0 THEN Auto)) THEN (RWO "i-approx-approx" (-1) THENA Auto) THEN With \mkleeneopen{}(2 * (M * M) * M * M) * k\mkleeneclose{} (D (-1))\mcdot{} THEN Auto THEN D -1) Home Index