---

Step * of Lemma ratbound_wf

∀[x:ℤ × ℕ+]. (ratbound(x) ∈ {m:ℕ+| |ratreal(x)| ≤ r(m)} )
BY
{ (Intro
   THEN Unhide
   THEN D 1
   THEN (InstLemma `div_bounds_1` [⌜|x1|⌝;⌜x2⌝]⋅ THENA Auto)
   THEN (Assert ratbound(<x1, x2>) ∈ ℕ+ BY
               ProveWfLemma)
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. x1 : ℤ
2. x2 : ℕ+
3. 0 ≤ (|x1| ÷ x2)
4. ratbound(<x1, x2>) ∈ ℕ+
⊢ |ratreal(<x1, x2>)| ≤ r(ratbound(<x1, x2>))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  (ratbound(x)  \mmember{}  \{m:\mBbbN{}\msupplus{}|  |ratreal(x)|  \mleq{}  r(m)\}  )


By

---

Latex:
(Intro
  THEN  Unhide
  THEN  D  1
  THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}|x1|\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  ratbound(<x1,  x2>)  \mmember{}  \mBbbN{}\msupplus{}  BY
                          ProveWfLemma)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index