---

Step * of Lemma rinv-functionality-lemma

∀x,y:ℤ. ∀a,b,n:ℕ+.
  ((n ≤ (a * |x|)) ⇒ (n ≤ (b * |y|)) ⇒ (|x - y| ≤ 4) ⇒ (|((4 * n * n) ÷ x) - (4 * n * n) ÷ y| ≤ (2 + (16 * a * b))))
BY
{ (Auto
   THEN (Assert x ≠ 0 BY
               ((D 0 THENA Auto)
                THEN OnMaybeHyp 6 (\h. (HypSubst' (-1) h THEN RepUR ``absval`` h THEN Complete (Auto')))
                ))
   THEN (Assert y ≠ 0 BY
               ((D 0 THENA Auto)
                THEN OnMaybeHyp 6 (\h. (HypSubst' (-1) h THEN RepUR ``absval`` h THEN Complete (Auto')))
                ))
   THEN (Using [`n',⌜|x * y|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)) }

1
1. x : ℤ@i
2. y : ℤ@i
3. a : ℕ+@i
4. b : ℕ+@i
5. n : ℕ+@i
6. n ≤ (a * |x|)@i
7. n ≤ (b * |y|)@i
8. |x - y| ≤ 4@i
9. x ≠ 0
10. y ≠ 0
⊢ (|x * y| * |((4 * n * n) ÷ x) - (4 * n * n) ÷ y|) ≤ (|x * y| * (2 + (16 * a * b)))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.  \mforall{}a,b,n:\mBbbN{}\msupplus{}.
    ((n  \mleq{}  (a  *  |x|))
    {}\mRightarrow{}  (n  \mleq{}  (b  *  |y|))
    {}\mRightarrow{}  (|x  -  y|  \mleq{}  4)
    {}\mRightarrow{}  (|((4  *  n  *  n)  \mdiv{}  x)  -  (4  *  n  *  n)  \mdiv{}  y|  \mleq{}  (2  +  (16  *  a  *  b))))


By

---

Latex:
(Auto
  THEN  (Assert  x  \mneq{}  0  BY
                          ((D  0  THENA  Auto)
                            THEN  OnMaybeHyp  6  (\mbackslash{}h.  (HypSubst'  (-1)  h
                                                                            THEN  RepUR  ``absval``  h
                                                                            THEN  Complete  (Auto')))
                            ))
  THEN  (Assert  y  \mneq{}  0  BY
                          ((D  0  THENA  Auto)
                            THEN  OnMaybeHyp  6  (\mbackslash{}h.  (HypSubst'  (-1)  h
                                                                            THEN  RepUR  ``absval``  h
                                                                            THEN  Complete  (Auto')))
                            ))
  THEN  (Using  [`n',\mkleeneopen{}|x  *  y|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto))

---

Home Index