---

Step * 1 1 1 of Lemma ratreduce_wf


1. x1 : ℤ
2. x2 : ℕ+
3. g : ℤ
4. gcd(x1;x2) = g ∈ ℤ
5. 0 < |g|
6. c1 : ℤ
7. x1 = (|g| * c1) ∈ ℤ
8. c : ℤ
9. x2 = (|g| * c) ∈ ℤ
10. c ∈ ℕ+
⊢ (x1 * c) = (c1 * x2) ∈ ℤ
BY
{ ((Eliminate ⌜x1⌝⋅ THEN Eliminate ⌜x2⌝⋅) THEN Auto) }

---

Latex:

---

Latex:

1.  x1  :  \mBbbZ{}
2.  x2  :  \mBbbN{}\msupplus{}
3.  g  :  \mBbbZ{}
4.  gcd(x1;x2)  =  g
5.  0  <  |g|
6.  c1  :  \mBbbZ{}
7.  x1  =  (|g|  *  c1)
8.  c  :  \mBbbZ{}
9.  x2  =  (|g|  *  c)
10.  c  \mmember{}  \mBbbN{}\msupplus{}
\mvdash{}  (x1  *  c)  =  (c1  *  x2)


By

---

Latex:
((Eliminate  \mkleeneopen{}x1\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}x2\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index