---

Step * of Lemma real-ratio-bound-cases

No Annotations
∀M:ℕ+. ∀x,y:ℝ.
  ∀[a,b:{r:ℝ| r0 < r} ].
    ((x < y) ∧ (real-ratio-bound(M;x;y;a;b) = (a/y - x))) ∨ ((y < x) ∧ (real-ratio-bound(M;x;y;a;b) = (b/x - y))) 
    supposing (r(2)/r(M)) ≤ |x - y|
BY
{ (Auto
   THEN Unfold `real-ratio-bound` 0
   THEN (GenConclTerm ⌜rclose-or-sep(M;x;y)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (Assert ((v = 1 ∈ ℤ) ⇒ ((r1/r(M)) < (y - x)))
               ∧ ((v = 2 ∈ ℤ) ⇒ ((r1/r(M)) < (x - y)))
               ∧ ((v = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(M)))) BY
               (Unhide THEN Auto))
   THEN Thin (-2)
   THEN IntSegCases (-2)
   THEN ExRepD
   THEN ThinTrivial
   THEN Reduce 0) }

1
1. M : ℕ+
2. x : ℝ
3. y : ℝ
4. [a] : {r:ℝ| r0 < r} 
5. [b] : {r:ℝ| r0 < r} 
6. (r(2)/r(M)) ≤ |x - y|
7. v : ℤ
8. (v = 1 ∈ ℤ) ⇒ ((r1/r(M)) < (y - x))
9. (v = 2 ∈ ℤ) ⇒ ((r1/r(M)) < (x - y))
10. v = 0 ∈ ℤ
11. |x - y| < (r(2)/r(M))
⊢ ((x < y) ∧ (((r(M)/r(2)) * rmin(a;b)) = (a/y - x))) ∨ ((y < x) ∧ (((r(M)/r(2)) * rmin(a;b)) = (b/x - y)))

2
1. M : ℕ+
2. x : ℝ
3. y : ℝ
4. [a] : {r:ℝ| r0 < r} 
5. [b] : {r:ℝ| r0 < r} 
6. (r(2)/r(M)) ≤ |x - y|
7. v : ℤ
8. (v = 2 ∈ ℤ) ⇒ ((r1/r(M)) < (x - y))
9. (v = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(M)))
10. v = 1 ∈ ℤ
11. (r1/r(M)) < (y - x)
⊢ ((x < y) ∧ ((a/y - x) = (a/y - x))) ∨ ((y < x) ∧ ((a/y - x) = (b/x - y)))

3
1. M : ℕ+
2. x : ℝ
3. y : ℝ
4. [a] : {r:ℝ| r0 < r} 
5. [b] : {r:ℝ| r0 < r} 
6. (r(2)/r(M)) ≤ |x - y|
7. v : ℤ
8. (v = 1 ∈ ℤ) ⇒ ((r1/r(M)) < (y - x))
9. (v = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(M)))
10. v = 2 ∈ ℤ
11. (r1/r(M)) < (x - y)
⊢ ((x < y) ∧ ((b/x - y) = (a/y - x))) ∨ ((y < x) ∧ ((b/x - y) = (b/x - y)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}M:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbR{}.
    \mforall{}[a,b:\{r:\mBbbR{}|  r0  <  r\}  ].
        ((x  <  y)  \mwedge{}  (real-ratio-bound(M;x;y;a;b)  =  (a/y  -  x)))
        \mvee{}  ((y  <  x)  \mwedge{}  (real-ratio-bound(M;x;y;a;b)  =  (b/x  -  y))) 
        supposing  (r(2)/r(M))  \mleq{}  |x  -  y|


By

---

Latex:
(Auto
  THEN  Unfold  `real-ratio-bound`  0
  THEN  (GenConclTerm  \mkleeneopen{}rclose-or-sep(M;x;y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (Assert  ((v  =  1)  {}\mRightarrow{}  ((r1/r(M))  <  (y  -  x)))
                          \mwedge{}  ((v  =  2)  {}\mRightarrow{}  ((r1/r(M))  <  (x  -  y)))
                          \mwedge{}  ((v  =  0)  {}\mRightarrow{}  (|x  -  y|  <  (r(2)/r(M))))  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  IntSegCases  (-2)
  THEN  ExRepD
  THEN  ThinTrivial
  THEN  Reduce  0)

---

Home Index