---

Step * 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 ∈ ℕ+
⊢ (r(x1)/r(x2)) = (r(c1)/r(c))
BY
{ (BLemma `req-int-fractions` THEN Auto) }

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

---

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{}  (r(x1)/r(x2))  =  (r(c1)/r(c))


By

---

Latex:
(BLemma  `req-int-fractions`  THEN  Auto)

---

Home Index