---

Step * of Lemma gcd-mod

∀x:ℕ+. ∀y:ℕ.  (gcd(x;y mod x) = gcd(x;y) ∈ ℤ)
BY
{ (Auto THEN CaseNat 0 `y') }

1
1. x : ℕ+
2. y : ℕ
3. y = 0 ∈ ℤ
⊢ gcd(x;0 mod x) = gcd(x;0) ∈ ℤ

2
1. x : ℕ+
2. y : ℕ
3. ¬(y = 0 ∈ ℤ)
⊢ gcd(x;y mod x) = gcd(x;y) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}\msupplus{}.  \mforall{}y:\mBbbN{}.    (gcd(x;y  mod  x)  =  gcd(x;y))


By

---

Latex:
(Auto  THEN  CaseNat  0  `y')

---

Home Index