---

Step * 1 of Lemma implies-equal-div


1. a : ℤ
2. c : ℤ
3. b : ℤ-o
4. d : ℤ-o
5. (d * a) = (b * c) ∈ ℤ
6. a = (((a ÷ b) * b) + (a rem b)) ∈ ℤ
7. (d * a) = (d * (((a ÷ b) * b) + (a rem b))) ∈ ℤ
8. c = (((c ÷ d) * d) + (c rem d)) ∈ ℤ
9. (b * c) = (b * (((c ÷ d) * d) + (c rem d))) ∈ ℤ
⊢ ((b * d) * (a ÷ b)) = ((b * d) * (c ÷ d)) ∈ ℤ
BY
{ (Assert ((c rem d) * b) = ((a rem b) * d) ∈ ℤ BY
         ((RWO "rem-mul<" 0 THENA Auto) THEN EqCDA THEN Auto)) }

1
1. a : ℤ
2. c : ℤ
3. b : ℤ-o
4. d : ℤ-o
5. (d * a) = (b * c) ∈ ℤ
6. a = (((a ÷ b) * b) + (a rem b)) ∈ ℤ
7. (d * a) = (d * (((a ÷ b) * b) + (a rem b))) ∈ ℤ
8. c = (((c ÷ d) * d) + (c rem d)) ∈ ℤ
9. (b * c) = (b * (((c ÷ d) * d) + (c rem d))) ∈ ℤ
10. ((c rem d) * b) = ((a rem b) * d) ∈ ℤ
⊢ ((b * d) * (a ÷ b)) = ((b * d) * (c ÷ d)) ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  c  :  \mBbbZ{}
3.  b  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  d  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  (d  *  a)  =  (b  *  c)
6.  a  =  (((a  \mdiv{}  b)  *  b)  +  (a  rem  b))
7.  (d  *  a)  =  (d  *  (((a  \mdiv{}  b)  *  b)  +  (a  rem  b)))
8.  c  =  (((c  \mdiv{}  d)  *  d)  +  (c  rem  d))
9.  (b  *  c)  =  (b  *  (((c  \mdiv{}  d)  *  d)  +  (c  rem  d)))
\mvdash{}  ((b  *  d)  *  (a  \mdiv{}  b))  =  ((b  *  d)  *  (c  \mdiv{}  d))


By

---

Latex:
(Assert  ((c  rem  d)  *  b)  =  ((a  rem  b)  *  d)  BY
              ((RWO  "rem-mul<"  0  THENA  Auto)  THEN  EqCDA  THEN  Auto))

---

Home Index