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