---

Step * 1 1 1 of Lemma sbdecode_wf_gcd


1. L : ℕ2 List
2. v1 : ℕ+
3. v2 : ℕ+
4. (v1 ÷ gcd(v1;v2)) = v1 ∈ ℕ+
5. (v2 ÷ gcd(v1;v2)) = v2 ∈ ℕ+
6. L = sbcode(v1;v2) ∈ (ℕ2 List)
7. 0 < gcd(v1;v2)
8. v1 = (((v1 ÷ gcd(v1;v2)) * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ∈ ℤ
⊢ gcd(v1;v2) = 1 ∈ ℤ
BY
{ xxx(HypSubst' 4 (-1) THEN InstLemma `rem_bounds_1` [⌜v1⌝;⌜gcd(v1;v2)⌝]⋅ THEN Auto')xxx }

1
1. L : ℕ2 List
2. v1 : ℕ+
3. v2 : ℕ+
4. (v1 ÷ gcd(v1;v2)) = v1 ∈ ℕ+
5. (v2 ÷ gcd(v1;v2)) = v2 ∈ ℕ+
6. L = sbcode(v1;v2) ∈ (ℕ2 List)
7. 0 < gcd(v1;v2)
8. v1 = ((v1 * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ∈ ℤ
9. 0 ≤ (v1 rem gcd(v1;v2))
10. v1 rem gcd(v1;v2) < gcd(v1;v2)
⊢ gcd(v1;v2) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  L  :  \mBbbN{}2  List
2.  v1  :  \mBbbN{}\msupplus{}
3.  v2  :  \mBbbN{}\msupplus{}
4.  (v1  \mdiv{}  gcd(v1;v2))  =  v1
5.  (v2  \mdiv{}  gcd(v1;v2))  =  v2
6.  L  =  sbcode(v1;v2)
7.  0  <  gcd(v1;v2)
8.  v1  =  (((v1  \mdiv{}  gcd(v1;v2))  *  gcd(v1;v2))  +  (v1  rem  gcd(v1;v2)))
\mvdash{}  gcd(v1;v2)  =  1


By

---

Latex:
xxx(HypSubst'  4  (-1)  THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}gcd(v1;v2)\mkleeneclose{}]\mcdot{}  THEN  Auto')xxx

---

Home Index