---

Step * 1 of Lemma lcm-property


1. x : ℤ
2. y : ℤ
3. a : ℤ
4. b : ℤ
5. CoPrime(a,b) ∧ (x = (gcd(x;y) * a) ∈ ℤ) ∧ (y = (gcd(x;y) * b) ∈ ℤ)
6. gcd(x;y) = 0 ∈ ℤ
⊢ CoPrime(a,b) ∧ ((x * b) = lcm(x;y) ∈ ℤ) ∧ ((y * a) = lcm(x;y) ∈ ℤ)
BY
{ (Unfold `lcm` 0
   THEN Eliminate ⌜gcd(x;y)⌝⋅
   THEN SplitAndHyps
   THEN Eliminate x⋅
   THEN Eliminate y⋅
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  a  :  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  CoPrime(a,b)  \mwedge{}  (x  =  (gcd(x;y)  *  a))  \mwedge{}  (y  =  (gcd(x;y)  *  b))
6.  gcd(x;y)  =  0
\mvdash{}  CoPrime(a,b)  \mwedge{}  ((x  *  b)  =  lcm(x;y))  \mwedge{}  ((y  *  a)  =  lcm(x;y))


By

---

Latex:
(Unfold  `lcm`  0
  THEN  Eliminate  \mkleeneopen{}gcd(x;y)\mkleeneclose{}\mcdot{}
  THEN  SplitAndHyps
  THEN  Eliminate  x\mcdot{}
  THEN  Eliminate  y\mcdot{}
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  AutoSplit)

---

Home Index