---

Step * of Lemma lcm-property

No Annotations
∀x,y:ℤ.  ∃a,b:ℤ. (CoPrime(a,b) ∧ ((x * b) = lcm(x;y) ∈ ℤ) ∧ ((y * a) = lcm(x;y) ∈ ℤ))
BY
{ (InstLemma `gcd-property` [] THEN RepeatFor 4 (ParallelLast') THEN (Decide gcd(x;y) = 0 ∈ ℤ THENA Auto)) }

1
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) ∈ ℤ)

2
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) ∈ ℤ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x,y:\mBbbZ{}.    \mexists{}a,b:\mBbbZ{}.  (CoPrime(a,b)  \mwedge{}  ((x  *  b)  =  lcm(x;y))  \mwedge{}  ((y  *  a)  =  lcm(x;y)))


By

---

Latex:
(InstLemma  `gcd-property`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  (Decide  gcd(x;y)  =  0  THENA  Auto))

---

Home Index