---

Step * of Lemma gcd_functionality_wrt_eqmod

∀a,a',m:ℤ.  ((a' ≡ a mod m) ⇒ (gcd(a';m) ~ gcd(a;m)))
BY
{ (Auto
   THEN D -1
   THEN (InstLemma `gcd_elim` [⌜a'⌝;⌜m⌝]⋅ THENA Auto)
   THEN (InstLemma `gcd_elim` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN ((HypSubst (-4) 0 THENA Auto) THEN Thin (-4))
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN Thin (-1)
   THEN D -3
   THEN D -1
   THEN ExRepD
   THEN D 0
   THEN BackThruSomeHyp
   THEN Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}a,a',m:\mBbbZ{}.    ((a'  \mequiv{}  a  mod  m)  {}\mRightarrow{}  (gcd(a';m)  \msim{}  gcd(a;m)))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (InstLemma  `gcd\_elim`  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `gcd\_elim`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  ((HypSubst  (-4)  0  THENA  Auto)  THEN  Thin  (-4))
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -3
  THEN  D  -1
  THEN  ExRepD
  THEN  D  0
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index