---

Step * 2 of Lemma proportional-round_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index