---

Step * 1 2 1 1 1 2 of Lemma assert-is-qrep


1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. gcd_reduce(p1;p2) = <v1, v3, v4> ∈ (ℕ × ℤ × ℤ)
8. p1 = (v3 * v1) ∈ ℤ
9. p2 = (v4 * v1) ∈ ℤ
10. CoPrime(v3,v4)
11. (p1 * v4) = (v3 * p2) ∈ ℤ
12. (v1 = 1 ∈ ℤ) ∨ (v1 = (-1) ∈ ℤ)
⊢ if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  = <p1, p2> ∈ (ℤ × ℕ+)
BY
{ (D (-1) THEN (HypSubst' (-1) 0 THEN HypSubst' (-1) (-5)) THEN HypSubst' (-1) (-4) THEN AutoSplit) }

1
1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. gcd_reduce(p1;p2) = <v1, v3, v4> ∈ (ℕ × ℤ × ℤ)
8. p1 = (v3 * 1) ∈ ℤ
9. p2 = (v4 * 1) ∈ ℤ
10. CoPrime(v3,v4)
11. (p1 * v4) = (v3 * p2) ∈ ℤ
12. v1 = 1 ∈ ℤ
13. 0 ≤ v4
⊢ <v3, v4> = <p1, p2> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  p1  :  \mBbbZ{}
2.  p2  :  \mBbbN{}\msupplus{}
3.  (gcd(p1;p2)  =  1)  \mvee{}  (gcd(p1;p2)  =  (-1))
4.  v1  :  \mBbbN{}
5.  v3  :  \mBbbZ{}
6.  v4  :  \mBbbZ{}
7.  gcd\_reduce(p1;p2)  =  <v1,  v3,  v4>
8.  p1  =  (v3  *  v1)
9.  p2  =  (v4  *  v1)
10.  CoPrime(v3,v4)
11.  (p1  *  v4)  =  (v3  *  p2)
12.  (v1  =  1)  \mvee{}  (v1  =  (-1))
\mvdash{}  if  0  \mleq{}z  v4  then  <v3,  v4>  else  <-v3,  -v4>  fi    =  <p1,  p2>


By

---

Latex:
(D  (-1)  THEN  (HypSubst'  (-1)  0  THEN  HypSubst'  (-1)  (-5))  THEN  HypSubst'  (-1)  (-4)  THEN  AutoSplit)

---

Home Index