---

Step * 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 ∈ ℕ+
⊢ <c1, c> ∈ {y:ℤ × ℕ+| ratreal(<x1, x2>) = ratreal(y)} 
BY
{ ((MemTypeCD THEN Auto) THEN RWO "ratreal-req" 0 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 ∈ ℕ+
⊢ (r(x1)/r(x2)) = (r(c1)/r(c))

---

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{}  <c1,  c>  \mmember{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(<x1,  x2>)  =  ratreal(y)\} 


By

---

Latex:
((MemTypeCD  THEN  Auto)  THEN  RWO  "ratreal-req"  0  THEN  Auto)

---

Home Index