---

Step * 2 1 of Lemma qrep_wf


1. z2 : ℤ
2. z3 : ℤ-o
3. z : ℤ
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z2 = (v3 * v1) ∈ ℤ
8. z3 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z2 * v4) = (v3 * z3) ∈ ℤ
11. z2 = (z * z3) ∈ ℤ
⊢ if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  = <z, 1> ∈ (ℤ × ℕ+)
BY
{ ((Assert v1 ∈ ℤ-o BY
          ((MemTypeCD THEN Auto) THEN TACTIC:(D 0 THEN Auto) THEN HypSubst' -1 -5 THEN Complete (Auto)))
   THEN (Assert v3 = (z * v4) ∈ ℤ BY
               ((Using [`n',⌜v1⌝] (BLemma `mul_cancel_in_eq`))⋅
                THEN Auto
                THEN Assert ⌜(v3 * v1) = (z * v4 * v1) ∈ ℤ⌝⋅
                THEN Auto))
   ) }

1
1. z2 : ℤ
2. z3 : ℤ-o
3. z : ℤ
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. z2 = (v3 * v1) ∈ ℤ
8. z3 = (v4 * v1) ∈ ℤ
9. CoPrime(v3,v4)
10. (z2 * v4) = (v3 * z3) ∈ ℤ
11. z2 = (z * z3) ∈ ℤ
12. v1 ∈ ℤ-o
13. v3 = (z * v4) ∈ ℤ
⊢ if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  = <z, 1> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  z2  :  \mBbbZ{}
2.  z3  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  z  :  \mBbbZ{}
4.  v1  :  \mBbbN{}
5.  v3  :  \mBbbZ{}
6.  v4  :  \mBbbZ{}
7.  z2  =  (v3  *  v1)
8.  z3  =  (v4  *  v1)
9.  CoPrime(v3,v4)
10.  (z2  *  v4)  =  (v3  *  z3)
11.  z2  =  (z  *  z3)
\mvdash{}  if  0  \mleq{}z  v4  then  <v3,  v4>  else  <-v3,  -v4>  fi    =  <z,  1>


By

---

Latex:
((Assert  v1  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}  BY
                ((MemTypeCD  THEN  Auto)
                  THEN  TACTIC:(D  0  THEN  Auto)
                  THEN  HypSubst'  -1  -5
                  THEN  Complete  (Auto)))
  THEN  (Assert  v3  =  (z  *  v4)  BY
                          ((Using  [`n',\mkleeneopen{}v1\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_eq`))\mcdot{}
                            THEN  Auto
                            THEN  Assert  \mkleeneopen{}(v3  *  v1)  =  (z  *  v4  *  v1)\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  )

---

Home Index