---

Step * 1 of Lemma gcd_assoc


1. a : ℤ
2. b : ℤ
3. c : ℤ
⊢ gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))
BY
{ ((((FunElim ⌜gcd(a;b) = w ∈ ℤ⌝ THENM FunElim ⌜gcd(b;c) = x ∈ ℤ⌝) THENM FunElim ⌜gcd(w;c) = y ∈ ℤ⌝)
   THENM FunElim ⌜gcd(a;x) = z ∈ ℤ⌝
   )
   THENA Auto
   ) }

1
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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
\mvdash{}  gcd(gcd(a;b);c)  \msim{}  gcd(a;gcd(b;c))


By

---

Latex:
((((FunElim  \mkleeneopen{}gcd(a;b)  =  w\mkleeneclose{}  THENM  FunElim  \mkleeneopen{}gcd(b;c)  =  x\mkleeneclose{})  THENM  FunElim  \mkleeneopen{}gcd(w;c)  =  y\mkleeneclose{})
  THENM  FunElim  \mkleeneopen{}gcd(a;x)  =  z\mkleeneclose{}
  )
  THENA  Auto
  )

---

Home Index