---

Step * of Lemma gcd_p_functionality_wrt_assoced

∀a,a',b,b',y,y':ℤ.  ((a ~ a') ⇒ (b ~ b') ⇒ (y ~ y') ⇒ (GCD(a;b;y) ⇐⇒ GCD(a';b';y')))
BY
{ ((RepD THENA Auto) THEN Unfold `gcd_p` 0) }

1
1. a : ℤ
2. a' : ℤ
3. b : ℤ
4. b' : ℤ
5. y : ℤ
6. y' : ℤ
7. a ~ a'
8. b ~ b'
9. y ~ y'
⊢ (y | a) ∧ (y | b) ∧ (∀z:ℤ. (((z | a) ∧ (z | b)) ⇒ (z | y)))
⇐⇒ (y' | a') ∧ (y' | b') ∧ (∀z:ℤ. (((z | a') ∧ (z | b')) ⇒ (z | y')))

---

Latex:

---

Latex:
\mforall{}a,a',b,b',y,y':\mBbbZ{}.    ((a  \msim{}  a')  {}\mRightarrow{}  (b  \msim{}  b')  {}\mRightarrow{}  (y  \msim{}  y')  {}\mRightarrow{}  (GCD(a;b;y)  \mLeftarrow{}{}\mRightarrow{}  GCD(a';b';y')))


By

---

Latex:
((RepD  THENA  Auto)  THEN  Unfold  `gcd\_p`  0)

---

Home Index