---

Step * of Lemma real-ratio-bound_wf

No Annotations
∀[M:ℕ+]. ∀[x,y:ℝ]. ∀[a,b:{r:ℝ| r0 < r} ].
  (real-ratio-bound(M;x;y;a;b) ∈ {r:ℝ| ((x < y) ⇒ (r ≤ (a/y - x))) ∧ ((y < x) ⇒ (r ≤ (b/x - y))) ∧ (r0 < r)} )
BY
{ (Intros
   THEN Unhide
   THEN (Assert r0 < (r1/r(M)) BY
               Auto)
   THEN Unfold `real-ratio-bound` 0
   THEN GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN D -1
   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. r0 < (r1/r(M))
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))
⊢ (r(M)/r(2)) * rmin(a;b) ∈ {r:ℝ| ((x < y) ⇒ (r ≤ (a/y - x))) ∧ ((y < x) ⇒ (r ≤ (b/x - y))) ∧ (r0 < r)} 

2
1. M : ℕ+
2. x : ℝ
3. y : ℝ
4. a : {r:ℝ| r0 < r} 
5. b : {r:ℝ| r0 < r} 
6. r0 < (r1/r(M))
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)
⊢ (a/y - x) ∈ {r:ℝ| ((x < y) ⇒ (r ≤ (a/y - x))) ∧ ((y < x) ⇒ (r ≤ (b/x - y))) ∧ (r0 < r)} 

3
1. M : ℕ+
2. x : ℝ
3. y : ℝ
4. a : {r:ℝ| r0 < r} 
5. b : {r:ℝ| r0 < r} 
6. r0 < (r1/r(M))
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)
⊢ (b/x - y) ∈ {r:ℝ| ((x < y) ⇒ (r ≤ (a/y - x))) ∧ ((y < x) ⇒ (r ≤ (b/x - y))) ∧ (r0 < r)} 

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  r0  <  (r1/r(M))  BY
                          Auto)
  THEN  Unfold  `real-ratio-bound`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  IntSegCases  (-2)
  THEN  ExRepD
  THEN  ThinTrivial
  THEN  Reduce  0)

---

Home Index