---

Step * 1 2 of Lemma rounded-numerator_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index