---

Step * 1 2 1 1 2 1 1 of Lemma residue-mul-inverse


1. z : ℤ
2. c2 : ℤ
3. c1 : ℤ
4. n : {2...}
5. a : ℕ
6. CoPrime(z * c1,a)
7. 1 ∈ residue(z * c1)
8. b : ℤ
9. (((z * c2) * a) mod (z * c1)) = 1 ∈ ℤ
10. c : ℤ
11. (((z * c2) * a) - 1) = ((z * c1) * c) ∈ ℤ
12. 1 | (z * c2)
13. n = (z * c1) ∈ ℤ
14. b = (z * c2) ∈ ℤ
⊢ z | 1
BY
{ (With ⌜(c2 * a) - c1 * c⌝ (D 0)⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  z  :  \mBbbZ{}
2.  c2  :  \mBbbZ{}
3.  c1  :  \mBbbZ{}
4.  n  :  \{2...\}
5.  a  :  \mBbbN{}
6.  CoPrime(z  *  c1,a)
7.  1  \mmember{}  residue(z  *  c1)
8.  b  :  \mBbbZ{}
9.  (((z  *  c2)  *  a)  mod  (z  *  c1))  =  1
10.  c  :  \mBbbZ{}
11.  (((z  *  c2)  *  a)  -  1)  =  ((z  *  c1)  *  c)
12.  1  |  (z  *  c2)
13.  n  =  (z  *  c1)
14.  b  =  (z  *  c2)
\mvdash{}  z  |  1


By

---

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

---

Home Index