---

Step * of Lemma gcd_properties

∀a,b:ℤ.  (((gcd(a;b) | a) ∧ (gcd(a;b) | b)) ∧ (∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | gcd(a;b)))))
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. a : ℤ@i
2. b : ℤ@i
⊢ (gcd(a;b) | a) ∧ (gcd(a;b) | b)

2
1. a : ℤ@i
2. b : ℤ@i
⊢ ∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | gcd(a;b)))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (((gcd(a;b)  |  a)  \mwedge{}  (gcd(a;b)  |  b))  \mwedge{}  (\mforall{}c:\mBbbZ{}.  ((c  |  a)  {}\mRightarrow{}  (c  |  b)  {}\mRightarrow{}  (c  |  gcd(a;b)))))


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index