---

Step * of Lemma proportional-round_wf

∀[r:ℚ]. ∀[k:ℤ]. ∀[l:ℤ-o].  (proportional-round(r;k;l) ∈ ℤ)
BY
{ (Auto
   THEN (D 1 THENA Auto)
   THEN MoveToConcl (-3)
   THEN GenConclTerms Auto [⌜r⌝;⌜r1⌝]⋅
   THEN All Thin
   THEN Auto
   THEN Unfold `qeq` (-1)
   THEN RepeatFor 2 ((CallByValueReduce (-1) THENA Auto))
   THEN Unfold `proportional-round` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN All D_rational_form
   THEN Auto
   THEN (RWO "eqtt_to_assert" (-1) THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)) }

1
1. k : ℤ
2. l : ℤ-o
3. a3 : ℤ
4. a4 : ℤ-o
5. a1 : ℤ
6. a3 = (a1 * a4) ∈ ℤ
⊢ ((a3 * k) ÷ a4 * l) = ((a1 * k) ÷ l) ∈ ℤ

2
1. k : ℤ
2. l : ℤ-o
3. a4 : ℤ
4. a2 : ℤ
5. a3 : ℤ-o
6. (a4 * a3) = a2 ∈ ℤ
⊢ ((a4 * k) ÷ l) = ((a2 * k) ÷ a3 * l) ∈ ℤ

3
1. k : ℤ
2. l : ℤ-o
3. a5 : ℤ
4. a6 : ℤ-o
5. a2 : ℤ
6. a3 : ℤ-o
7. (a5 * a3) = (a2 * a6) ∈ ℤ
⊢ ((a5 * k) ÷ a6 * l) = ((a2 * k) ÷ a3 * l) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[k:\mBbbZ{}].  \mforall{}[l:\mBbbZ{}\msupminus{}\msupzero{}].    (proportional-round(r;k;l)  \mmember{}  \mBbbZ{})


By

---

Latex:
(Auto
  THEN  (D  1  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto
  THEN  Unfold  `qeq`  (-1)
  THEN  RepeatFor  2  ((CallByValueReduce  (-1)  THENA  Auto))
  THEN  Unfold  `proportional-round`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  All  D\_rational\_form
  THEN  Auto
  THEN  (RWO  "eqtt\_to\_assert"  (-1)  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))

---

Home Index