---

Step * 3 1 1 1 2 2 of Lemma qrep_wf


1. z : ℤ
2. z1 : ℤ
3. z2 : ℤ-o
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z1 = (v3 * v1) ∈ ℤ
8. z2 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z1 * v4) = (v3 * z2) ∈ ℤ
11. (z * z2) = z1 ∈ ℤ
12. v1 ∈ ℤ-o
13. v3 = (z * v4) ∈ ℤ
14. v4 ≠ 0
15. CoPrime(z,1)
16. v4 < 0
17. CoPrime(-v3,-v4)
⊢ <z, 1> = <-v3, -v4> ∈ (ℤ × ℕ+)
BY
{ (FLemma `coprime-equiv-unique-pair` [-3;-1] THEN Auto')⋅ }

1
1. z : ℤ
2. z1 : ℤ
3. z2 : ℤ-o
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z1 = (v3 * v1) ∈ ℤ
8. z2 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z1 * v4) = (v3 * z2) ∈ ℤ
11. (z * z2) = z1 ∈ ℤ
12. v1 ∈ ℤ-o
13. v3 = (z * v4) ∈ ℤ
14. v4 ≠ 0
15. CoPrime(z,1)
16. v4 < 0
17. CoPrime(-v3,-v4)
18. z < 0
⊢ -v3 < 0

2
1. z : ℤ
2. z1 : ℤ
3. z2 : ℤ-o
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z1 = (v3 * v1) ∈ ℤ
8. z2 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z1 * v4) = (v3 * z2) ∈ ℤ
11. (z * z2) = z1 ∈ ℤ
12. v1 ∈ ℤ-o
13. v3 = (z * v4) ∈ ℤ
14. v4 ≠ 0
15. CoPrime(z,1)
16. v4 < 0
17. CoPrime(-v3,-v4)
18. -v3 < 0
⊢ z < 0

3
1. z : ℤ
2. z1 : ℤ
3. z2 : ℤ-o
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z1 = (v3 * v1) ∈ ℤ
8. z2 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z1 * v4) = (v3 * z2) ∈ ℤ
11. (z * z2) = z1 ∈ ℤ
12. v1 ∈ ℤ-o
13. v3 = (z * v4) ∈ ℤ
14. v4 ≠ 0
15. CoPrime(z,1)
16. v4 < 0
17. CoPrime(-v3,-v4)
18. <z, 1> = <-v3, -v4> ∈ (ℤ × ℤ-o)
⊢ <z, 1> = <-v3, -v4> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  z  :  \mBbbZ{}
2.  z1  :  \mBbbZ{}
3.  z2  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  v1  :  \mBbbN{}
5.  v3  :  \mBbbZ{}
6.  v4  :  \mBbbZ{}
7.  z1  =  (v3  *  v1)
8.  z2  =  (v4  *  v1)
9.  CoPrime(v3,v4)
10.  (z1  *  v4)  =  (v3  *  z2)
11.  (z  *  z2)  =  z1
12.  v1  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
13.  v3  =  (z  *  v4)
14.  v4  \mneq{}  0
15.  CoPrime(z,1)
16.  v4  <  0
17.  CoPrime(-v3,-v4)
\mvdash{}  <z,  1>  =  <-v3,  -v4>


By

---

Latex:
(FLemma  `coprime-equiv-unique-pair`  [-3;-1]  THEN  Auto')\mcdot{}

---

Home Index