---

Step * 2 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
{ (Auto
   THEN (Unfold `lcm` 0
         THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
         THEN RepeatFor 2 ((Try (AutoSplit) THEN Try ((HypSubst' (-1) 0 THEN Auto')))))⋅
   ) }

1
1. x : ℤ
2. x ≠ 0
3. y : ℤ
4. a : ℤ
5. b : ℤ
6. CoPrime(a,b)
7. x = (gcd(x;y) * a) ∈ ℤ
8. y = (gcd(x;y) * b) ∈ ℤ
9. ¬(gcd(x;y) = 0 ∈ ℤ)
10. CoPrime(a,b)
11. y = 0 ∈ ℤ
⊢ (x * b) = 0 ∈ ℤ

2
1. x : ℤ
2. x ≠ 0
3. y : ℤ
4. y ≠ 0
5. a : ℤ
6. b : ℤ
7. CoPrime(a,b)
8. x = (gcd(x;y) * a) ∈ ℤ
9. y = (gcd(x;y) * b) ∈ ℤ
10. ¬(gcd(x;y) = 0 ∈ ℤ)
11. CoPrime(a,b)
⊢ (x * b) = eval g = gcd(x;y) in (x * y) ÷ g ∈ ℤ

3
1. x : ℤ
2. y : ℤ
3. a : ℤ
4. b : ℤ
5. CoPrime(a,b)
6. x = (gcd(x;y) * a) ∈ ℤ
7. y = (gcd(x;y) * b) ∈ ℤ
8. ¬(gcd(x;y) = 0 ∈ ℤ)
9. CoPrime(a,b)
10. (x * b) = lcm(x;y) ∈ ℤ
11. x = 0 ∈ ℤ
⊢ (y * a) = 0 ∈ ℤ

4
1. x : ℤ
2. x ≠ 0
3. y : ℤ
4. y ≠ 0
5. a : ℤ
6. b : ℤ
7. CoPrime(a,b)
8. x = (gcd(x;y) * a) ∈ ℤ
9. y = (gcd(x;y) * b) ∈ ℤ
10. ¬(gcd(x;y) = 0 ∈ ℤ)
11. CoPrime(a,b)
12. (x * b) = lcm(x;y) ∈ ℤ
⊢ (y * a) = eval g = gcd(x;y) in (x * y) ÷ g ∈ ℤ

---

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.  \mneg{}(gcd(x;y)  =  0)
\mvdash{}  CoPrime(a,b)  \mwedge{}  ((x  *  b)  =  lcm(x;y))  \mwedge{}  ((y  *  a)  =  lcm(x;y))


By

---

Latex:
(Auto
  THEN  (Unfold  `lcm`  0
              THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
              THEN  RepeatFor  2  ((Try  (AutoSplit)  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto')))))\mcdot{}
  )

---

Home Index