---

Step * of Lemma coprime_functionality_wrt_eqmod

∀a,a',m:ℤ.  ((a' ≡ a mod m) ⇒ (CoPrime(a',m) ⇐⇒ CoPrime(a,m)))
BY
{ (Auto
   THEN D -2
   THEN D -1
   THEN D 0
   THEN Auto
   THEN Try ((BLemma `one_divs_any` THEN Auto))
   THEN BackThruSomeHyp
   THEN Auto) }

1
1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. c : ℤ@i
5. (a' - a) = (m * c) ∈ ℤ@i
6. 1 | a'@i
7. 1 | m@i
8. ∀z:ℤ. (((z | a') ∧ (z | m)) ⇒ (z | 1))@i
9. 1 | m
10. z : ℤ@i
11. z | a@i
12. z | m@i
⊢ z | a'

2
1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. c : ℤ@i
5. (a' - a) = (m * c) ∈ ℤ@i
6. 1 | a@i
7. 1 | m@i
8. ∀z:ℤ. (((z | a) ∧ (z | m)) ⇒ (z | 1))@i
9. 1 | m
10. z : ℤ@i
11. z | a'@i
12. z | m@i
⊢ z | a

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  D  0
  THEN  Auto
  THEN  Try  ((BLemma  `one\_divs\_any`  THEN  Auto))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index