---

Step * 1 of Lemma gcd_properties


1. a : ℤ@i
2. b : ℤ@i
⊢ (gcd(a;b) | a) ∧ (gcd(a;b) | b)
BY
{ (Auto THEN Try ((BLemma `gcd_is_divisor_1` THEN Auto)) THEN Try ((BLemma `gcd_is_divisor_2` THEN Auto))) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
\mvdash{}  (gcd(a;b)  |  a)  \mwedge{}  (gcd(a;b)  |  b)


By

---

Latex:
(Auto
  THEN  Try  ((BLemma  `gcd\_is\_divisor\_1`  THEN  Auto))
  THEN  Try  ((BLemma  `gcd\_is\_divisor\_2`  THEN  Auto)))

---

Home Index