Proof of Nuprl Lemma : derivative-rinv

Step * of Lemma derivative-rinv

∀I:Interval. ∀f,g:I ⟶ℝ.
  ((∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y])))
  ⇒ f[x]≠r0 for x ∈ I
  ⇒ d(f[x])/dx = λx.g[x] on I
  ⇒ d((r1/f[x]))/dx = λx.(-(g[x])/f[x] * f[x]) on I)
BY
{ TACTIC:(Auto
          THEN (D 0 THEN Auto)
          THEN (Assert i-approx(I;n) ⊆ I  BY
                      Auto)
          THEN (InstLemma `nonzero-on-implies` [⌜I⌝;⌜f⌝]⋅ THENA Auto)
          THEN (With ⌜n⌝ (D 5)⋅ THENA Auto)
          THEN (Assert ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b])) BY

                      (InstLemma `continuous-implies-functional` [⌜i-approx(I;n)⌝;⌜f⌝]⋅

                       THEN Auto
                       THEN BLemma `proper-continuous-implies`
                       THEN Auto
                       THEN FLemma `differentiable-continuous` [5]
                       THEN Auto))
          THEN (InstLemma `function-is-continuous` [⌜i-approx(I;n)⌝;⌜λ₂x.(r1/f[x])⌝]⋅
                THENA (Auto THEN BLemma `rdiv_functionality` THEN Auto)
                )
          THEN (InstLemma `function-is-continuous` [⌜i-approx(I;n)⌝;⌜λ₂x.g[x]⌝]⋅ THENA Auto)
          THEN (Assert ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0) BY

                      (ParallelOp -5 THEN ParallelLast THEN FLemma `i-member-approx` [-1] THEN Auto))

          THEN PromoteHyp (-4) 8) }

1
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)
⊢ ∃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:
\mforall{}I:Interval. \mforall{}f,g:I {}\mrightarrow{}\mBbbR{}. ((\mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (g[x] = g[y]))) {}\mRightarrow{} f[x]\mneq{}r0 for x \mmember{} I {}\mRightarrow{} d(f[x])/dx = \mlambda{}x.g[x] on I {}\mRightarrow{} d((r1/f[x]))/dx = \mlambda{}x.(-(g[x])/f[x] * f[x]) on I) By Latex: TACTIC:(Auto THEN (D 0 THEN Auto) THEN (Assert i-approx(I;n) \msubseteq{} I BY Auto) THEN (InstLemma `nonzero-on-implies` [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto) THEN (With \mkleeneopen{}n\mkleeneclose{} (D 5)\mcdot{} THENA Auto) THEN (Assert \mforall{}a,b:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . ((a = b) {}\mRightarrow{} (f[a] = f[b])) BY (InstLemma `continuous-implies-functional` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THEN Auto THEN BLemma `proper-continuous-implies` THEN Auto THEN FLemma `differentiable-continuous` [5] THEN Auto)) THEN (InstLemma `function-is-continuous` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/f[x])\mkleeneclose{}]\mcdot{} THENA (Auto THEN BLemma `rdiv\_functionality` THEN Auto) ) THEN (InstLemma `function-is-continuous` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g[x]\mkleeneclose{}]\mcdot{} THENA Auto) THEN (Assert \mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} f[x] \mneq{} r0) BY (ParallelOp -5 THEN ParallelLast THEN FLemma `i-member-approx` [-1] THEN Auto)) THEN PromoteHyp (-4) 8) Home Index