---

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


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

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((D  (-2)  THEN  (Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}  THENA  Auto))  THEN  D  (-1)  THEN  (Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index