---

Step * 1 1 of Lemma rounded-numerator_wf


1. k : ℕ+
2. a3 : ℤ
3. a4 : ℤ-o
4. a1 : ℤ
5. a3 = (a1 * a4) ∈ ℤ
⊢ ((a3 * k) ÷ a4) = (a1 * k) ∈ ℤ
BY
{ xxx(HypSubst' (-1) 0⋅ THEN Subst' (a1 * a4) * k ~ (a1 * k) * a4 0 THEN Auto)⋅xxx }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  a3  :  \mBbbZ{}
3.  a4  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  a1  :  \mBbbZ{}
5.  a3  =  (a1  *  a4)
\mvdash{}  ((a3  *  k)  \mdiv{}  a4)  =  (a1  *  k)


By

---

Latex:
xxx(HypSubst'  (-1)  0\mcdot{}  THEN  Subst'  (a1  *  a4)  *  k  \msim{}  (a1  *  k)  *  a4  0  THEN  Auto)\mcdot{}xxx

---

Home Index