---

Step * of Lemma int-rdiv_wf

No Annotations
∀[k:ℤ-o]. ∀[a:ℝ].  ((a)/k ∈ ℝ)
BY
{ (Auto
   THEN (D -1 THEN Unfold `int-rdiv` 0 THEN (CallByValueReduce 0 THENA Auto))
   THEN MemTypeCD
   THEN Auto
   THEN Try (ProveWfLemma)
   THEN ParallelLast
   THEN Reduce 0
   THEN Auto
   THEN (Decide ⌜|k| ≤ 1⌝⋅ THENA Auto)) }

1
1. k : ℤ-o
2. a : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
4. n : ℕ+
5. m : ℕ+
6. |k| ≤ 1
⊢ |(m * ((a n) ÷ k)) - n * ((a m) ÷ k)| ≤ (2 * (n + m))

2
1. k : ℤ-o
2. a : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
4. n : ℕ+
5. m : ℕ+
6. ¬(|k| ≤ 1)
⊢ |(m * ((a n) ÷ k)) - n * ((a m) ÷ k)| ≤ (2 * (n + m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[a:\mBbbR{}].    ((a)/k  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto
  THEN  (D  -1  THEN  Unfold  `int-rdiv`  0  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (ProveWfLemma)
  THEN  ParallelLast
  THEN  Reduce  0
  THEN  Auto
  THEN  (Decide  \mkleeneopen{}|k|  \mleq{}  1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index