---

Step * of Lemma gcd-unique-nat

∀n,m,g:ℕ.  ((((g | n) ∧ (g | m)) ∧ (∀v:ℤ. ((v | n) ⇒ (v | m) ⇒ (v | g)))) ⇒ (g = gcd(n;m) ∈ ℤ))
BY
{ ((Auto THEN BLemma `assoced_nelim` THEN Auto) THEN (InstLemma `gcd_unique` [⌜n⌝;⌜m⌝]⋅ THENM BHyp -1 ) THEN Auto) }

1
1. n : ℕ@i
2. m : ℕ@i
3. g : ℕ@i
4. g | n@i
5. g | m@i
6. ∀v:ℤ. ((v | n) ⇒ (v | m) ⇒ (v | g))@i
7. ∀y1,y2:ℤ.  (GCD(n;m;y1) ⇒ GCD(n;m;y2) ⇒ (y1 ~ y2))
⊢ GCD(n;m;g)

---

Latex:

---

Latex:
\mforall{}n,m,g:\mBbbN{}.    ((((g  |  n)  \mwedge{}  (g  |  m))  \mwedge{}  (\mforall{}v:\mBbbZ{}.  ((v  |  n)  {}\mRightarrow{}  (v  |  m)  {}\mRightarrow{}  (v  |  g))))  {}\mRightarrow{}  (g  =  gcd(n;m)))


By

---

Latex:
((Auto  THEN  BLemma  `assoced\_nelim`  THEN  Auto)
  THEN  (InstLemma  `gcd\_unique`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENM  BHyp  -1  )
  THEN  Auto)

---

Home Index