---

Step * 4 1 1 2 of Lemma qrep_wf

.....aux..... 
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. ¬(z3 = 0 ∈ ℤ)
⊢ (v7 * v4) = (v3 * v8) ∈ ℤ
BY
{ ((Using [`n',⌜z3 * z2⌝] (BLemma `mul_cancel_in_eq`))⋅ THEN Auto) }

1
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. ¬(z3 = 0 ∈ ℤ)
⊢ ((z3 * z2) * v7 * v4) = ((z3 * z2) * v3 * v8) ∈ ℤ

---

Latex:

---

Latex:
.....aux..... 
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.  \mneg{}(z3  =  0)
\mvdash{}  (v7  *  v4)  =  (v3  *  v8)


By

---

Latex:
((Using  [`n',\mkleeneopen{}z3  *  z2\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_eq`))\mcdot{}  THEN  Auto)

---

Home Index