---

Step * 1 2 of Lemma sbdecode-code


1. m : ℕ
2. ∀m:ℕm. ∀[n:ℕ]. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
3. n : ℕ
4. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
5. 0 < m
6. 0 < n
7. m < n
8. 0 < gcd(m;n)
⊢ <m ÷ gcd(m;n), (m ÷ gcd(m;n)) + ((n - m) ÷ gcd(m;n))> ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>
BY
{ xxx(EqCD THEN Try (Trivial))xxx }

1
1. m : ℕ
2. ∀m:ℕm. ∀[n:ℕ]. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
3. n : ℕ
4. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
5. 0 < m
6. 0 < n
7. m < n
8. 0 < gcd(m;n)
⊢ (m ÷ gcd(m;n)) + ((n - m) ÷ gcd(m;n)) ~ n ÷ gcd(m;n)

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  \mforall{}m:\mBbbN{}m.  \mforall{}[n:\mBbbN{}].  (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>))
3.  n  :  \mBbbN{}
4.  \mforall{}n:\mBbbN{}n.  (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>))
5.  0  <  m
6.  0  <  n
7.  m  <  n
8.  0  <  gcd(m;n)
\mvdash{}  <m  \mdiv{}  gcd(m;n),  (m  \mdiv{}  gcd(m;n))  +  ((n  -  m)  \mdiv{}  gcd(m;n))>  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>


By

---

Latex:
xxx(EqCD  THEN  Try  (Trivial))xxx

---

Home Index