---

Step * 1 1 1 of Lemma gcd_assoc


1. a : ℤ
2. b : ℤ
3. c : ℤ
4. w : ℤ
5. GCD(a;b;w)
6. x : ℤ
7. y : ℤ
8. GCD(w;c;y)
9. z : ℤ
10. GCD(c;b;x)
11. GCD(x;a;z)
⊢ y ~ z
BY
{ ((Sel (-1) (FLemma `gcd_of_triple` [5;8]) THENA Auto)
   THEN (Sel (-1) (FLemma `gcd_of_triple` [10;11]) THENA Auto)
   THEN RepD
   THEN Unfold `assoced` 0
   THEN HypBackchain
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  w  :  \mBbbZ{}
5.  GCD(a;b;w)
6.  x  :  \mBbbZ{}
7.  y  :  \mBbbZ{}
8.  GCD(w;c;y)
9.  z  :  \mBbbZ{}
10.  GCD(c;b;x)
11.  GCD(x;a;z)
\mvdash{}  y  \msim{}  z


By

---

Latex:
((Sel  (-1)  (FLemma  `gcd\_of\_triple`  [5;8])  THENA  Auto)
  THEN  (Sel  (-1)  (FLemma  `gcd\_of\_triple`  [10;11])  THENA  Auto)
  THEN  RepD
  THEN  Unfold  `assoced`  0
  THEN  HypBackchain
  THEN  Auto)

---

Home Index