---

Step * 1 of Lemma proportional-round_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index