---

Step * of Lemma gcd_exists

∀a,b:ℤ.  ∃y:ℤ. GCD(a;b;y)
BY
{ (Auto THENM (Decide ⌜0 ≤ b⌝ THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. 0 ≤ b
⊢ ∃y:ℤ. GCD(a;b;y)

2
1. a : ℤ
2. b : ℤ
3. ¬(0 ≤ b)
⊢ ∃y:ℤ. GCD(a;b;y)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    \mexists{}y:\mBbbZ{}.  GCD(a;b;y)


By

---

Latex:
(Auto  THENM  (Decide  \mkleeneopen{}0  \mleq{}  b\mkleeneclose{}  THENA  Auto))

---

Home Index