---

Step * 4 1 1 3 1 of Lemma qrep_wf

.....assertion..... 
1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
20. v8 ∈ ℤ-o
21. v4 ∈ ℤ-o
22. (v7 * v4) = (v3 * v8) ∈ ℤ
⊢ CoPrime(-v3,-v4)
BY
{ (RepeatFor 3 (TACTIC:ParallelOp 17) THEN Auto THEN BackThruSomeHyp THEN EAuto 1) }

---

Latex:

---

Latex:
.....assertion..... 
1.  z3  :  \mBbbZ{}
2.  z4  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  z1  :  \mBbbZ{}
4.  z2  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  v1  :  \mBbbN{}
6.  v3  :  \mBbbZ{}
7.  v4  :  \mBbbZ{}
8.  v5  :  \mBbbN{}
9.  v7  :  \mBbbZ{}
10.  v8  :  \mBbbZ{}
11.  z3  =  (v7  *  v5)
12.  z4  =  (v8  *  v5)
13.  CoPrime(v7,v8)
14.  (z3  *  v8)  =  (v7  *  z4)
15.  z1  =  (v3  *  v1)
16.  z2  =  (v4  *  v1)
17.  CoPrime(v3,v4)
18.  (z1  *  v4)  =  (v3  *  z2)
19.  (z3  *  z2)  =  (z1  *  z4)
20.  v8  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
21.  v4  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
22.  (v7  *  v4)  =  (v3  *  v8)
\mvdash{}  CoPrime(-v3,-v4)


By

---

Latex:
(RepeatFor  3  (TACTIC:ParallelOp  17)  THEN  Auto  THEN  BackThruSomeHyp  THEN  EAuto  1)

---

Home Index