---

Step * of Lemma eqmod-eqmod-div

∀m,m',a,a',b,b':ℤ.  ((m' | m) ⇒ (a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ (a ≡ b mod m' ⇐⇒ a' ≡ b' mod m'))
BY
{ (Auto
   THEN All (Unfold `eqmod`)
   THEN All (Unfold `divides`)
   THEN ExRepD
   THEN Eliminate ⌜m⌝⋅
   THEN (All (RWO "mul_assoc<") THENA Auto)) }

1
1. m' : ℤ
2. c3 : ℤ
3. m : ℤ
4. a : ℤ
5. a' : ℤ
6. b : ℤ
7. b' : ℤ
8. m = (m' * c3) ∈ ℤ
9. c2 : ℤ
10. (a - a') = (m' * c3 * c2) ∈ ℤ
11. c1 : ℤ
12. (b - b') = (m' * c3 * c1) ∈ ℤ
13. c : ℤ
14. (a - b) = (m' * c) ∈ ℤ
⊢ ∃c:ℤ. ((a' - b') = (m' * c) ∈ ℤ)

2
1. m' : ℤ
2. c3 : ℤ
3. m : ℤ
4. a : ℤ
5. a' : ℤ
6. b : ℤ
7. b' : ℤ
8. m = (m' * c3) ∈ ℤ
9. c2 : ℤ
10. (a - a') = (m' * c3 * c2) ∈ ℤ
11. c1 : ℤ
12. (b - b') = (m' * c3 * c1) ∈ ℤ
13. c : ℤ
14. (a' - b') = (m' * c) ∈ ℤ
⊢ ∃c:ℤ. ((a - b) = (m' * c) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}m,m',a,a',b,b':\mBbbZ{}.
    ((m'  |  m)  {}\mRightarrow{}  (a  \mequiv{}  a'  mod  m)  {}\mRightarrow{}  (b  \mequiv{}  b'  mod  m)  {}\mRightarrow{}  (a  \mequiv{}  b  mod  m'  \mLeftarrow{}{}\mRightarrow{}  a'  \mequiv{}  b'  mod  m'))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `eqmod`)
  THEN  All  (Unfold  `divides`)
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}m\mkleeneclose{}\mcdot{}
  THEN  (All  (RWO  "mul\_assoc<")  THENA  Auto))

---

Home Index