---

Step * 2 of Lemma eqmod-eqmod-div


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) ∈ ℤ)
BY
{ (With ⌜((c3 * c2) - c3 * c1) + c⌝ (D 0)⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  m'  :  \mBbbZ{}
2.  c3  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  a  :  \mBbbZ{}
5.  a'  :  \mBbbZ{}
6.  b  :  \mBbbZ{}
7.  b'  :  \mBbbZ{}
8.  m  =  (m'  *  c3)
9.  c2  :  \mBbbZ{}
10.  (a  -  a')  =  (m'  *  c3  *  c2)
11.  c1  :  \mBbbZ{}
12.  (b  -  b')  =  (m'  *  c3  *  c1)
13.  c  :  \mBbbZ{}
14.  (a'  -  b')  =  (m'  *  c)
\mvdash{}  \mexists{}c:\mBbbZ{}.  ((a  -  b)  =  (m'  *  c))


By

---

Latex:
(With  \mkleeneopen{}((c3  *  c2)  -  c3  *  c1)  +  c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index