---

Step * 1 of Lemma divisibility-lattice_wf

.....wf..... 
1. ∀[a,b:ℕ].  (gcd(a;b) = gcd(b;a) ∈ ℕ)
2. ∀[a,b:ℕ].  (lcm(a;b) = lcm(b;a) ∈ ℕ)
3. a : ℕ
4. b : ℕ
5. c : ℕ
⊢ gcd(a;gcd(b;c)) ∈ ℕ
BY
{ (MemTypeCD THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  \mforall{}[a,b:\mBbbN{}].    (gcd(a;b)  =  gcd(b;a))
2.  \mforall{}[a,b:\mBbbN{}].    (lcm(a;b)  =  lcm(b;a))
3.  a  :  \mBbbN{}
4.  b  :  \mBbbN{}
5.  c  :  \mBbbN{}
\mvdash{}  gcd(a;gcd(b;c))  \mmember{}  \mBbbN{}


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index