---

Step * 1 1 of Lemma gcd_assoc


1. a : ℤ
2. b : ℤ
3. c : ℤ
4. w : ℤ
5. GCD(a;b;w)
6. x : ℤ
7. GCD(b;c;x)
8. y : ℤ
9. GCD(w;c;y)
10. z : ℤ
11. GCD(a;x;z)
⊢ y ~ z
BY
{ (((FLemma `gcd_p_sym` [7] THENM FLemma `gcd_p_sym` [11]) THENM OnHyps [11;7] Thin) THENA Auto) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
(((FLemma  `gcd\_p\_sym`  [7]  THENM  FLemma  `gcd\_p\_sym`  [11])  THENM  OnHyps  [11;7]  Thin)  THENA  Auto)

---

Home Index