---

Step * 1 2 1 2 1 1 of Lemma derivative-rinv


1. k : ℕ+
2. M : ℕ+
3. fx : ℝ
4. fy : ℝ
5. gx : ℝ
6. gy : ℝ
7. e : ℝ
8. fx ≠ r0
9. fy ≠ r0
10. |fy - fx - gx * e| ≤ ((r1/r((2 * M * M) * k)) * |e|)
11. |fy - fx| ≤ (r1/r((2 * (M * M) * M * M) * k))
12. |gx| ≤ r(M)
13. |(r1/fx)| ≤ r(M)
14. |gy| ≤ r(M)
15. |(r1/fy)| ≤ r(M)
⊢ |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| ≤ ((r1/r(k)) * |e|)
BY
{ ((Assert fx * fx ≠ r0 BY
          (OrRight THEN Auto THEN D 8 THEN nRMul ⌜fx⌝ 8⋅ THEN Auto))
   THEN (Assert |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e|
               = ((|(r1/fx)| * |(r1/fy)|) * |fy - fx - (fy * (r1/fx)) * gx * e|) BY
               ((RW (AddrC [1] (RevLemmaC `rabs-rminus`)) 0 THENA Auto)
                THEN (RWW "rabs-rmul<" 0 THENA Auto)
                THEN nRNorm 0
                THEN (BLemma `rabs_functionality` THEN Auto)
                THEN BLemma `radd_functionality`
                THEN Auto
                THEN RepeatFor 2 (nRMul ⌜fx⌝ 0⋅)
                THEN MoveToConcl (-1)
                THEN (GenConclTerm ⌜fx * fx⌝⋅ THENA Auto)
                THEN Auto
                THEN nRNorm 0
                THEN Auto))
   ) }

1
1. k : ℕ+
2. M : ℕ+
3. fx : ℝ
4. fy : ℝ
5. gx : ℝ
6. gy : ℝ
7. e : ℝ
8. fx ≠ r0
9. fy ≠ r0
10. |fy - fx - gx * e| ≤ ((r1/r((2 * M * M) * k)) * |e|)
11. |fy - fx| ≤ (r1/r((2 * (M * M) * M * M) * k))
12. |gx| ≤ r(M)
13. |(r1/fx)| ≤ r(M)
14. |gy| ≤ r(M)
15. |(r1/fy)| ≤ r(M)
16. fx * fx ≠ r0
17. |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| = ((|(r1/fx)| * |(r1/fy)|) * |fy - fx - (fy * (r1/fx)) * gx * e|)
⊢ |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| ≤ ((r1/r(k)) * |e|)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  M  :  \mBbbN{}\msupplus{}
3.  fx  :  \mBbbR{}
4.  fy  :  \mBbbR{}
5.  gx  :  \mBbbR{}
6.  gy  :  \mBbbR{}
7.  e  :  \mBbbR{}
8.  fx  \mneq{}  r0
9.  fy  \mneq{}  r0
10.  |fy  -  fx  -  gx  *  e|  \mleq{}  ((r1/r((2  *  M  *  M)  *  k))  *  |e|)
11.  |fy  -  fx|  \mleq{}  (r1/r((2  *  (M  *  M)  *  M  *  M)  *  k))
12.  |gx|  \mleq{}  r(M)
13.  |(r1/fx)|  \mleq{}  r(M)
14.  |gy|  \mleq{}  r(M)
15.  |(r1/fy)|  \mleq{}  r(M)
\mvdash{}  |(r1/fy)  -  (r1/fx)  -  (-(gx)/fx  *  fx)  *  e|  \mleq{}  ((r1/r(k))  *  |e|)


By

---

Latex:
((Assert  fx  *  fx  \mneq{}  r0  BY
                (OrRight  THEN  Auto  THEN  D  8  THEN  nRMul  \mkleeneopen{}fx\mkleeneclose{}  8\mcdot{}  THEN  Auto))
  THEN  (Assert  |(r1/fy)  -  (r1/fx)  -  (-(gx)/fx  *  fx)  *  e|
                          =  ((|(r1/fx)|  *  |(r1/fy)|)  *  |fy  -  fx  -  (fy  *  (r1/fx))  *  gx  *  e|)  BY
                          ((RW  (AddrC  [1]  (RevLemmaC  `rabs-rminus`))  0  THENA  Auto)
                            THEN  (RWW  "rabs-rmul<"  0  THENA  Auto)
                            THEN  nRNorm  0
                            THEN  (BLemma  `rabs\_functionality`  THEN  Auto)
                            THEN  BLemma  `radd\_functionality`
                            THEN  Auto
                            THEN  RepeatFor  2  (nRMul  \mkleeneopen{}fx\mkleeneclose{}  0\mcdot{})
                            THEN  MoveToConcl  (-1)
                            THEN  (GenConclTerm  \mkleeneopen{}fx  *  fx\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  Auto
                            THEN  nRNorm  0
                            THEN  Auto))
  )

---

Home Index